1================ CHANGES TO THE ORIGINAL CODE ================================== 2 3The only CVC4 connections passed to minisat are the proxy (defined in sat.h) and 4the context. The context is obtained from the SmtEngine, and the proxy is an 5intermediary class that has all-access to the SatSolver so as to simplify the 6interface to (possible) other sat solvers. These two are passed to minisat at 7construction time and some additional flags are set. We use the SimpSolver 8solver with simplifications. 9 10To compare with original minisat code in SVN you can compare to revision 6 on 11the trunk. 12 13The PropEngine then uses the following 14 15// Create the sat solver (this is the proxy, which will create minisat) 16d_satSolver = new SatSolver(this, d_theoryEngine, d_context); 17// Add some clauses 18d_cnfStream->convertAndAssert(node); 19// Check for satisfiabilty 20bool result = d_satSolver->solve(); 21 22* Adding theory literals: 23 24The newVar method has been changed from 25 Var Solver::newVar(bool sign, bool dvar) 26to 27 Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) 28in order to mark the variables as theory literals. For that purpose there is a 29new boolean array called "theory" that is true or false if the variables is for 30a theory literal. 31 32* Backtracking/Pushing 33 34Backtracking in minisat is performed through the cancelUntil() method, which is 35now modified to pop the context the appropriate number of times. 36 37Minisat pushes the scope in the newDecisionLevel() method where we appropriately 38also push the CVC4 context. 39 40* Phase caching 41 42In order to implement phase-caching (RSAT paper) we 43(1) flag minisat to use the user-provided polarities first by setting the 44minisat::SimpSolver::polarity_user flag when initializing the solver (in sat.h) 45(2) when a variable is set (in uncheckedEnqueue()) we remember the value in the 46"polarity" table. 47 48* Asserting the theory literals 49 50In the uncheckedEnqueue() method, if the literal is a theory literal (looking 51in the "theory" table), it is passed to the prop engine thorough the proxy. 52 53* Theory propagation (checking) 54 55The BCP propagation method was changed from propagate to propagateBool and 56another method propagateTheory is defined to do the theory propagation. The 57propagate method now looks like 58 59Clause* Solver::propagate() 60{ 61 Clause* confl = NULL; 62 63 while(qhead < trail.size()) { 64 confl = propagateBool(); 65 if (confl != NULL) break; 66 confl = propagateTheory(); 67 if (confl != NULL) break; 68 } 69 70 return confl; 71} 72 73The propagateBool method will perform the BCP on the newly assigned variables 74in the trail, and if a conflict is found it will break. Otherwise, the theory 75propagation is given a chance to check for satisfiability and maybe enqueue some 76additional propagated literals. 77 78* Conflict resolution 79 80If a conflict is detected during theory propagation we can rely on the minisat 81conflict resolution with a twist. Since a theory can return a conflict where 82all literals are assigned at a level lower than the current level, we must 83backtrack to the highest level of any literal in the conflict. This is done 84already in the propagateTheory(). 85 86* Clause simplification 87 88Minisat performs some simplifications on the clause database: 89(1) variable elimination 90(2) subsumtion 91 92Subsumtion is complete even with theory reasoning, but eliminating theory 93literals by resolution might be incomplete: 94 95(x = 0 \vee x = 1) \wedge (x != 1 \vee y = 1) \wedge x = y 96 ^^^^^ ^^^^^^ 97 v ~v 98 99would, after eliminating v, simplify to 100(x = 0) wedge (y = 1) wedge (x = y) which is unsatisfiable 101 102while x = 1, y = 1 is a satisfying assignment for the above. 103 104Minisat does not perform variable elimination on the variables that are marked 105as frozen (in the "frozen", SimSolver.h) table. We put all the theory literals 106in the frozen table, which solves the incompleteness problem. 107 108================ NOTES ========================================================= 109 110* Accessing the internals of the SAT solver 111 112The non-public parts of the SAT solver are accessed via the static methods in 113the SatSolver class. SatSolverProxy is declared as a friend of the 114SatSolver and has all-privileges access to the internals -- use with care!!! 115 116* Clause Database and CNF 117 118The clause database consists of two parts: 119 120 vec<Clause*> clauses; // List of problem clauses. 121 vec<Clause*> learnts; // List of learnt clauses. 122 123Clauses is the original problem clauses, and learnts are the clauses learned 124during the search. I have disabled removal of satisfied problem clauses by 125setting the remove_satisfied flag to false. 126 127The learnt clauses get removed every once in a while by removing the half of 128clauses with the low activity (reduceDB()) 129 130Since the clause database backtracks with the SMT solver, the CNF cache should 131be context dependent and everything will be in sync. 132 133* Adding a Clause 134 135The only method in the interface that allows addition of clauses in MiniSAT is 136 137 bool Solver::addClause(vec<Lit>& ps), 138 139but it only adds the problem clauses. 140 141In order to add the clauses to the removable database the interface is now 142 143 bool Solver::addClause(vec<Lit>& ps, bool removable). 144 145Clauses added with removable=true might get removed by the SAT solver when 146compacting the database. 147 148The question is whether to add the propagation/conflict lemmas as removable or 149not? 150 151* Literal Activities 152 153We do not backtrack literal activities. This does not semantically change the 154equivalence of the context, but does change solve times if the same problem is 155run several times. 156 157* Do we need to assign literals that only appear in satisfied clauses? 158