CSU 670 Fall 2006 Project Description =========================================================================== Which team builds the best designed and fastest CSP Solver? The DICHOTOMY CSP Project =========================================================================== version 1.1, Nov. 16, 2006 The project is about applying, refining and testing your software development skills to the design of your own CSP solvers (of which SAT solvers are a special case). The importance of SAT and CSP solvers is documented by several websites and conferences, e.g., http://www.satlive.org/ and http://cpai.ucc.ie/05/CallForSolvers.html Application domains are: program verification, electronic design automation, optimal planning, Bayesian network inference, computational biology and chemistry, etc. In the homeworks you have already implemented important parts of a CSP solver; you build on that experience in the project. ------------------------------------------ Here is a short version of the requirements document: Implement a CSP Solver which takes input according to class dictionary In and produces output according to class dictionary Out. To formulate the constraints any subset of the 256 relations of rank 3 over the Boolean domain may be used. An In-object consists of a set of constraints, each constraint of the form 22(5 6 7) where 22 is the name of one of the 256 relations and 5, 6 and 7 are literals. Your task is to find an assignment that satisfies all constraints. An Out-object consists either of an assignment of Boolean values to the variables that satisfies all constraints (this means the CSP instance is satisfiable) or of a sequence of transition steps (also called proof steps) that result in a FailState (this means the CSP instance is unsatisfiable). The details of the syntax is for you to decide and we will standardize on a syntax later. Because you write structure-shy software it will be easy for you to adapt to a new structure later. You need to use the value ordering software described below which is outsourced. The transition system you need to implement yourself. ------------------------------------------ The project is in the domain of Artifical Intelligence but it has a firm algorithmic foundation. The project is designed in such a way that we can prove: If we could do in polynomial time better than a trillionth (in terms of the fraction of the satisfied constraints wrt all constraints) then we would earn a million dollars from the Clay Foundation: http://www.claymath.org/millennium/ for solving the famous P=NP problems. The goal of the project is to create a modular, well-designed CSP solver that is correct and that implements non-chronological backtracking and value ordering based on outsourced software for computing an optimal coin flipping probability. There will be a competition among the teams for the CSP solver that can solve the largest instance in a benchmark of CSP problems. (Note: I talked with a software development manager in industry, Hilda Wong-Doo a vice-president at Fidelity Investments, and she found it important that you learn about software development in a global economy where working with geographically distributed teams is important.) The behavior of a large class of SAT solvers can be explained in terms of state transition systems. You have seen simple forms of state transition systems in your Theory of Computation class: Automata are a simple form of a state transition system. See: http://en.wikipedia.org/wiki/Labelled_transition_system The transition rules below describe at a high level the basic capabilities that your algorithms must have but it is left to you 1. how to implement those basic capabilities 2. how to sequence those basic capabilities. View this document as a requirements document written by a user who wants to influence at a high level of abstraction the algorithms that are used. In principle, the requirement document could just say: Implement a CSP Solver which takes input according to class dictionary In and produces output according to class dictionary Out. But Ahmed and I have certain algorithmic ideas in mind how to implement CSP solvers. This requirements document explains the requirements in terms of SAT solvers but you are expected to translate (generalize) those requirements to CSP solvers for the domain D = {0,1} and all relations of rank 3 or smaller. If you want to receive significant extra credit, you implement MaxCSP solvers for the domain D = {0,1} and all relations of rank 3 or smaller. Before you do this, talk to the professor and get permission to complete this more challenging task. The first algorithmic idea we want you to implement is non-chronological backtracking, a technique that your professor invented more than 30 years ago and which has been re-invented and has become a feature of all state-of-the-art SAT solvers. Non-chronological backtracking is explained by using a transition system consisting of states and transitions. A state is either the state FailState or a pair of the form M || F, where F is a CNF formula and M is essentially a partial assignment. Read sections 2.1 and 2.2 and 2.3 in Solving SAT and SAT Modulo Theories: http://www.ccs.neu.edu/home/lieber/courses/csg260/f06/materials/papers/sat/JACM2006revision.pdf taken from: http://www.lsi.upc.es/~roberto/papers/JACM2006revision.pdf The above paper is long and not published yet. You need to read only very little of it to do your project. A published predecessor is: @proceedings{LPAR:2005/sat, editor = {Roberto Nieuwenhuis and Albert Oliveras}, title = {Decision procedures for SAT, SAT Modulo Theories and Beyond - The BarcelogicTools}, booktitle = {LPAR 2005 invited talk}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, year = {2005} } http://www.ccs.neu.edu/home/lieber/courses/csg260/f06/materials/papers/sat/lpar05.pdf Abbreviations used: d* decision literal + or {} empty set , and UnitPropagate(literal k is forced): M||F,C + k => M k|| F,C + k if (C is not satisfied by M) and (k undef in M) Informal: (from the above JACM2006revision.pdf paper) To satisfy a CNF formula, all its clauses have to be true. Hence, if a clause of F contains a literal k whose truth value is not defined by the current assignment M while all the remaining literals of the clause are false, then M must be extended to make k true. Example: (from the above JACM2006revision.pdf paper) 1* || !1+!2, 2+3, !1+!3+4, 2+!3+!4, 1+4 => UnitPropagate 1* !2 || !1+!2, 2+3, !1+!3+4, 2+!3+!4, 1+4 => UnitPropagate 1* !2 3 || !1+!2, 2+3, !1+!3+4, 2+!3+!4, 1+4 => UnitPropagate 1* !2 3 4 || !1+!2, 2+3, !1+!3+4, 2+!3+!4, 1+4 Decide: M||F => M k*||F if (k and !k occur in a clause of F) and (k is undefined in M) Informal: (from the above JACM2006revision.pdf paper) This rule represents a case split. An undefined literal k is chosen from F, and added to M. The literal is annotated as a decision literal, to denote that if M k cannot be extended to a model of F then the alternative extension M !k must still be considered. This is done by means of the Backtrack rule or Semi-Superresolution rule. The Decide rule has to choose a value ordering. If k is positive then some variable v = k is first set to true and later to false, if (M v) cannot be extended to a model. If k is negative then some variable v = !k is first set to false and later to true, if (M !v) cannot be extended to a model. There are many options for value ordering and we will choose an interesting one below. Example: (from the above JACM2006revision.pdf paper) {} || !1+!2, 2+3, !1+!3+4, 2+!3+!4, 1+4 => Decide 1* || !1+!2, 2+3, !1+!3+4, 2+!3+!4, 1+4 Fail: M||F,C => FailState if M satisfies !C and M contains no decision literals This rule indicates that a CNF is unsatisfiable. It is interesting to note that the rules UnitPropagate, Decide, Fail and the following Backtrack rule already form a complete system to model SAT solvers. However, we are not going to use the following Backtrack rule in our solver; instead we will use a more sophisticated Semi-Superresolution rule. Backtrack: M l* N || F, C => M !l || F,C if (M l* N implies !C) and (N contains no decision literals). Informal: This rule models the backtracking you implemented in hw 5. Semi-Superresolution: I || F => I || F, {The negation of all decision literals in I} if Contradiction (I, F). We call {all negated decision literals in I} a semi-superresolvent. Informal: Semi-Superresolution computes the forced consequences of I (by UnitPropagate). If this leads to an unsatisfied clause in F, we learn a clause which prevents the same "mistake" in the future. Here is where non-chronological backtracking comes in: once we have added the semi-superresolvent, we will not explore the same node in the search space again and we are free to restart the search. Contradiction(I, F) returns the set of forced literals by I. The partial assignment I Contradiction(I, F) leaves at least one clause in F unsatisfied. When Semi-Superresolution is applied, the necessary UnitPropagate steps are already done. Why the name? Semi-Superresolution is one half of Superresolution. Example: 1* || !1+!2, 2+3, !1+!3+4, 2+!3+!4, 1+4 => Semi-Superresolution 1* || !1+!2, 2+3, !1+!3+4, 2+!3+!4, 1+4, !1 because by UnitPropagation: !2 3 4 are forced which makes 2+!3+!4 unsatisfied. 1* is the only decision variable; therefore we learn the semi-superresolvent !1. Superresolution: M||F => M||F,{all negated decision literals in M} if exists v* not in M: Contradiction ((M v), F) and Contradiction((M !v), F) We all {all negated decision literals in M} a superresolvent. Informal: Superresolution is Semi-Superresolution applied twice: First application: Semi-Superresolution with v: M v* || F => M v* || F, {all negated decision literals in (M v*)} Second application: Semi-Superresolution with !v: M !v* || F => M !v* || F, {all negated decision literals in (M !v*)} When we apply resolution to {all negated decision literals in (M v*)} and {all negated decision literals in (M !v*)} we get: {all negated decision literals in M} Example: Formula: 1+2,3+4,5+6,!1+!3,!1+!5,!3+!5,!2+!4,!2+!6,!4+!6 With Semi-Superresolution(1) we learn !1 With Semi-Superresolution(!1) we learn 1 The superresolvent is the empty clause, which means that the above formula has no satisfying assignment. 1,!1 leads to the FailState (see the Fail rule below) {} || 1,!1 UnitPropagate 1 || 1,!1 Fail FailState ---- Contradiction(M, k, F) = M k implies a contradiction in F by UnitPropagate more precisely: There is a sequence of transitions from the state M k || F using UnitPropagate leading to a state M k R || F where a clause in F is unsatisfied by M k R. Contradiction returns R if there is a contradiction (true) and {} otherwise (false). Fail: M||F,C => FailState if M satisfies !C and M contains no decision literals Learn: M||F => M||F,C if each atom of C occurs in F and F implies C Informal: Learn is a generalization of superresolution. If M||F => M||F,C by Superresolution then M||F => M||F,C by Learn Learn is also a generalization of Semi-Superresolution. If I||F => I||F,C by Semi-Superresolution then I||F => I||F,C by Learn Backtrack: M k* N || F,C => M !k || F,C if M k* N satisfies !C and N contains no decision literals Restart: M || F => {} || F Informal: With restart we can forget the partial assignment we have tried and start from scratch. This works if we use Semi-Superresolution to learn clauses that remember what we already have tried. Non-chronological backtracking is modeled by Restart and Semi-Superresolution. Resolution: M || F, v+C1, !v+C2 => M || F, C1+C2 if C1+C2 does not contain X and !X for some literal X. Informal: A famous proof rule introduced for the predicate calculus in 1965. A CNF is unsatisfiable iff we can derive the empty clause by Resolution. Decide by coin flipping: M||F => M k*||F if (k and !k occur in a clause of F) and (k is undefined in M) and (the decision between k = v* and k = !v* is made by flipping a coin that turns head with probability p. p is chosen so that the expected number of satisfied clauses is maximized for 0<=p<=1. The computation of the optimal coin bias is outsourced. The manager who is responsible for coordinating with the outsourcing team is Ahmed Abdel Mohsen. To educate yourself about the outsourcing project, read: http://www.ccs.neu.edu/home/lieber/p-optimal/partial-sat-II/Partial-SAT2.pdf (the first 6 pages are sufficient) (explains formula to polynomial construction for outsourcing project) http://www.ccs.neu.edu/home/lieber/p-optimal/max-mean.html (explains coin flipping connection) http://www.ccs.neu.edu/research/demeter/biblio/maxmean.html (original paper on formula to polynomial construction) http://www.ccs.neu.edu/home/lieber/p-optimal/README.html (more context on P-optimal approximation) To educate yourself about Superresolution: http://www.ccs.neu.edu/research/demeter/biblio/clause-learning.html Coordination with the outsourcing team is a high priority item so that the software development can proceed in parallel. You need to clearly define the interface that the outsourcing software needs to satisfy. What are the preconditions and what are the postconditions? You should be aware that you need to show professional behavior and creativity in your work with the outsourcing team. You really need to justify that you as US employees are paid 4 to 5 times as much as your outsourcing colleagues. Furthermore, your outsourcing colleagues are the cream of the cream and are likely to be very bright. I have informed your outsourcing colleagues about this collaboration and they will propose an interface themselves. But you need to come up with your own interface to make sure you get an interface that suits your needs. In this class, the outsourcing team is simulated by my graduate class on Advanced Software Development CSG 260. You may listen to their internal discussions at: https://lists.ccs.neu.edu/pipermail/csg260/ One member of the outsourcing team has written the following summary that is useful reading but still being refined: http://www.ccs.neu.edu/home/guaraldi/csg260/ (please choose the latest version) And you may study their "background" by looking at the homeworks they have done: http://www.ccs.neu.edu/home/lieber/courses/csg260/f06/hw/ (Note: I talked with a software development manager in industry and she found it important that you learn about software development in a global economy where working with geographically distributed teams is important.) Here is a first suggestion for the interface with the outsourcing team: The input is given by an object of class InputValueOrder and the result by an object of class OutputValueOrder. InputValueOrder = List(RelationFractionPair). RelationFractionPair = "relation" RelationNumber "fraction" RelationFraction. RelationNumber = int. RelationFraction = float. List(S) ~ {S}. OutputValueOrder = "max" "bias" CoinBias "polynomial" Polynomial. CoinBias = float. Polynomial = List(Coefficient). // We need only polynomials of rank 3 (four coefficients) // because our relations are of at most rank 3 Coefficient = float. InputUpdate = "polynomial" "before" Polynomial "added" List(RelationFractionPair) "subtracted" List(RelationFractionPair). // when a variable gets set we get a reduced formula // (see your homeworks) where new relations are added (plus) // and some relations are removed (minus). OutputUpdate = OutputValueOrder. // polynomial will be added to "previous" polynomial. We only consider relations of at most rank 3. The relation number of a relation is the result column viewed as a decimal number. For example consider the following relation that we have studied before: result 000 0 001 1 010 1 011 0 100 1 101 0 110 0 111 0 This relation has name 22 which is also called the OneInThree relation. The input consists of a list of pairs (relationName,fraction). For example, consider the CSP problem CSP1: 22 1 2 3 22 1 2 4 22 1 3 4 22 2 3 4 Here, the list relationFractions has only one pair: (22, 1.0) because CSP1 uses only one relation. The maximal coin bias is 1/3 and the corresponding polynomial that will be in the output is: 3*x(1-x)**2 = 3*x(1-2*x+x**2) = 3*x - 6*x**2 + 3*x**3 Your outsourcing colleagues are very good at math and they know the basics of calculus and discrete math. Note that when you maximize the above polynomial, you get a maximum for x = 1/3 and the value of the polynomial at 1/3 is 4/9. To debug the CSP solver, have the outsourcing team develop a debugging aspect using AspectJ. When you compile your solver with the debugging aspect, you will get a lot of feedback about how your solver behaves. Inspection of this output might lead to further improvements to your solver. The debugging aspect must produce the following: 1. A drawing of the polynomials in the OutputValueOrder objects including the probability for which the polynomial is maximum in the interval (0,1). You must write the software that draws the polynomials. It must be possible to show up to 255 polynomials in one graph. The graph may be crowded: http://www.ccs.neu.edu/home/lieber/courses/csu670/f06/project/256Polynomials.BMP shows 255 polynomials in one graph (0.0 = 1 and 1.0 = 11) . Those are the graphs of 255 of the 256 relations used in the outsourcing project. Ahmed has used Excel to plot the polynomials. The outsourced aspect will reach into your solver and call your drawing software at the right time. 2. Statistics about the solver: how often was each transition rule activated? This document will be amended as the course progresses. Please keep the same groups you had during the homeworks. If you absolutely need a change, please inform me. Deliverables: All deliverables involving software must be complete with adequate test cases. The implementation language is Java and you may use any tools you like. You don't have to use DemeterJ or DJ or you may use them only for a part of the project. For example, for efficiency reasons, you may want to use a non-DemeterJ generated data structure to represent CSP problems. You are encouraged to use version control software such as CVS. If you want to use CVS on college machines, please let Ahmed know. The project starts on Oct. 17. Deadline: Start date plus 7 days: Road map Document your road map to the final stage. This is a 1-2 page document, listing requirements, clarifying issues left open or left contradictory in this document and enumerating the steps you intend to follow. Explicitly list what components will be developed, their use and where they fit in the whole scheme of things. Also include a proposal for the interface with the outsourcing team and the test cases that you want to use: provide both inputs and expected outputs. You may want to develop the test cases in collaboration with the outsourcing team. Keep in mind that your success depends on how well the outsourcing team does its job. This step of the project is very important. At the end of the project you will compare your road map with the actual path of your project. Deadline: Start date plus 14 days: Phase 1 UnitPropagate for CSP. Input: A CSP problem. Output: A sequence of state transitions applying UnitPropagate terminating in a state where UnitPropagate can no longer be applied. Receive software from outsourcing team and test and review it. Use the debugging aspect to visualize the polynomials. You should also independently verify that they give you the correct maximum by doing a loop for k=0 to n and determining the k for which p(k/n) is maximum. The k[max] you get this way should be equal to n*x[max] rounded to the nearest integer. x[max] is returned by the outsourced software. Deadline: Startdate plus 21 days: Phase 2 Add Decide, FailState, Restart and Semi-Superresolution. Input: A CSP problem. Output: A sequence of state transitions leading to a target state that is either a FailState (formula is unsatisfiable) or a state where a model is found satisfying all constraints. Request changes from outsourcing team, if needed. Deadline: Startdate plus 28 days: Phase 3 Add Decide by coin flipping. This is a special kind of value ordering. Input: A CSP problem. Output: A sequence of state transitions leading to a target state that is either a FailState (formula is unsatisfiable) or a state where a model is found satisfying all constraints. When a decision needs to be made (you are no longer allowed to use the general Decide rule), you call the outsourced software to determine whether it is better to set a chosen variable x first to true and then to false or vice-versa. Deadline: Startdate plus 35 days: Phase 4 Add Variable Ordering (this is not a rule defined above) Input: A CSP problem. Output: A sequence of state transitions leading to a target state that is either a FailState (formula is unsatisfiable) or a state where a model is found satisfying all constraints. If there is a choice of variables to decide, choose the variable first for which the outsourced software produces the largest value. Report behavior of your software on provided benchmark. Deadline: Startdate plus 42 days: Phase 5 Performance Optimization. Get ready for the big CSP solver competition! Can you make the semi-superresolvents shorter by analyzing the reasons for a constraint to become unsatisfied. This will spead up your solver. Turn in your complete project with documentation but without your final report. Deadline: Startdate plus 49 days: Phase 6 Final report. Include original road map, and how you changed it. Also reflect on your project experience: what could you have done better? Grading: Your project will be graded based on 1. How well it works (how well can it solve CSP problems) 2. The quality of your code 3. Code reviews Not all deliverables will be graded. You will get a grade for the final project. All team members will be asked to report on the others how well they contributed to the project. See http://www.ccs.neu.edu/home/lieber/courses/csu670/f06/project/hitchhikers-couch-potatoes (Note the deadline) For later: Undecide (proposed by Ahmed): M k* R||F => M k R||F if by UnitPropagate we can derive k from M R in F i.e., there is a sequence of transitions from state M R||F using UnitPropagate to state M R k||F