DualSAT is a performant new SAT-solver that is optimized to find and output all solutions to an input CNF usable by further processing steps that can follow. Solutions are stored as a number of disjoint solution classes that happen to be in Decomposable Negation Normal Form (DNNF).
The solver implements new features like unentangled literal detection and backtracking with stack redo. Unentangled literal detection detects the remaining CNF to be in DNNF while a stack redo saves valuable work on conflict directed backjumps because much of the solver's stack content remains preserved. A combination of conflict dependent and independent heuristics ensures good results for known as well as novel and random CNFs. The dual data structures of DualSAT may also prove beneficial for new techniques with enhanced reasoning.
Table of Contents
1 Introduction
1.1 The Idea about DualSat
2 SAT-Solver Technology
2.1 Preliminaries
2.1.1 Encoding a Problem as SAT
2.1.2 Resolution, Preprocessing
2.2 DPLL Solvers
2.2.1 DPLL with Chronological Backtracking
2.2.2 Clause Learning
2.2.3 DPLL with Conflict Directed Backjumping
2.2.4 DPLL with Stack Redo
2.2.4.1 Practical Examples for the Stack Redo
2.3 DNNF, Extended Solution Classes and Other Known Algorithms for SAT-Solving
2.4 Efficient Data Structures for SAT-Solvers
2.4.1 Literal Counting
2.4.2 Watched Literals and Lazy Data Structures
2.4.3 The Data Structures of DualSat
2.5 DualSat
2.5.1 Unentangled Literal Detection
2.5.2 The Variable Selection Heuristic of DualSat
2.5.3 Some Other Implementation Details of DualSat
2.5.4 Wide Integer Implementation for DualSat
2.6 Interesting #SAT solvers
2.6.1 Clasp and Nogoods in DualSat
2.6.2 sharpSAT and Component Caching
3 Conclusion and Outlook
4 Benchmarks
4.1 rutgers.edu DualSat
4.2 rutgers.edu Clasp
4.3 rutgers.edu sharpSAT
4.4 rutgers.edu one solution DualSat
4.5 rutgers.edu one solution Clasp
4.6 rutgers.edu one solution ZChaff
4.7 DQMR DualSat
Epilogue
5 List of References
Acknowledgements
Many thanks to Univ. Prof. Dr. Martin Gebser who has guided and supported me at my work and who has given me valuable feedback.
1 Introduction
It was within a single decade that the practice of implementing programs for testing satisfiability of propositional formulas has made significant progress. While the first SAT-solvers were a practical curiosity, nowadays many real world and industrial scale problems can be solved with SAT-solvers. These programs are used in verification of hardware as well as software, in automatic test generation, in logical synthesis, in the analyzer of the Alloy software modeling language and in Artificial Intelligence for planning and automatic theorem proving [GuMi05], [MMZZ01]. Common SAT-solvers focus on finding just one possible solution to a propositional formula or by giving a refutation proof if such a solution should not exist. It may be sufficient to find that a given instance is unsatisfiable in order to prove the absence of bugs in a software or hardware design. There exists however a related problem, called #SAT (pronounce: ‘sharpSAT’) which goes for propositional model counting. A solution of a logical formula is called a model and thus the name model counting. It turned out that model counting is a particularly hard problem even for some polynomial-time solvable problems like 2-SAT which restricts a given conjunctive normal form (CNF) to clauses of length two. Model counting is used for bounded-length adversarial and contingency planning, probabilistic reasoning and Bayesian inference [BHMW08], [SBB04]. For some hard combinatorial problems the number of solutions provides further insights into the problem. While finding one solution can already be a challenge counting the number of solutions is even harder.
The problem of SAT-solving is NP-hard. That is you can test in polynomial time O(nx) where x is constant whether a given solution (here: to a logical expression) evaluates to true (here: in a fact in O(n) steps) but you need non-polynomial time to find such a solution. Given that you have n variables testing for all possible solutions has a worst case complexity of O(2n) for SAT or generally O(bn). This is in deed a very hard problem complexity class since you need twice the time to solve a problem with just one more variable. So if you have a computer that works eight times faster, you can only solve a problem with three more variables. Where commonly available instances of satisfiability problems have up to 10,000 variables (rutgers.edu/ssa6288-047.cnf [Ru00]), industrial scale problems being even larger, it would not be possible to get a solution here by simple truth value testing. 210000 is a number with 3011 digits. Even so current SAT-solvers apply a number of techniques to make satisfiability testing of real world problems more tractable, the basic problem remains that any decision on a variable, where both branches need to be explored exhaustively, does effectively double the execution time. That is why there are always a number of solvable problems but still also a number of unsolvable problems for SAT. One problem known to be hard is the verification of binary integer multiplication, because every digit is multiplied with each other digit before the sub-results can be added together. While integer adding involves just O(n) steps, multiplication requires O(n2) different operations which will all need to be verified [By86]. While the rutgers.edu/par16* instances are still solvable, instances like rutgers.edu/par32* have turned out to be unsolvable by the SAT-solvers we could test in this work.
There has been considerable work on the formal analysis of NP-hard problems even before the first practically usable SAT-solvers have emerged [Ng13], [So08]. There are a number of NP- hard problems like the vertex cover problem, the n-clique problem, the independent set problem, the hamilton cycle problem, the k-coloring problem, the traveling salesman problem, the knapsack problem and the bin packing problem. When the fact that every problem in NP can be reduced to SAT in polynomial time was widely regarded to be of theoretical interest before, the emergence of efficient SAT-solvers makes it now possible to solve many of such problem instances as well. The programs which convert a given problem into SAT are usually called encoders. Sometimes also preprocessors are used to make the encoding more efficient and to reduce the complexity in writing such domain specific encoders [EeBi05]. Some problems however cannot be solved by simple SAT-solvers alone. That encompasses verification and proofs with recursive structures that are not bound to a depth limit [DvPt60] or problems like answer set enumeration which require an extension of plain SAT solvers [GKAS07].
1.1 The Idea about DualSat
The initial idea about DualSat was to write a solver that returns not just one but all solutions to a given problem. This is different from plain SAT solvers which only return the first solution they can find and actually different from merely counting solutions. This may be important if a problem cannot be expressed solely by SAT as a CNF but if you have a coherent optimization problem on the number of satisfiable instances. That is why DualSat aims to return solution classes that are as compact as possible. One solution class encompasses many solutions on which a postprocessor may f.i. execute a non-linear optimization problem later on. There are plenty of NP- hard problems in computer science and some are linked to not just return any solution but to find the best possible solution of a host of solutions.
A simple solution class defines a zero or one value for a number of variables and leaves some other variables unassigned. You may write such a solution class as 01xx1 which means xi=0, x2=1, x5=1. In deed the very first solvers like CDP did already return such simple solution classes [BHMW08]. However the old style literal counting scheme of this implementation has some time been replaced with lazy data structures and watched literals. These require that all variables become assigned before a solution is detected [LyMS05].
Now look at a solution class with t assigned variables. It amounts for 2n-t solutions when you have n variables. In a worst case the basic SAT instance of our optimization problem can be a tautology and this would require then 2n-t = 2n steps to enumerate all solutions. That may last longer than the age of the universe given that you have enough variables and that you enumerate solutions one by one.
The idea about DualSat was now to combine old style literal counting for detecting that all clauses are already satisfied and that the remaining variables can take arbitrary values with the new lazy data structures which are only used for learned clauses. Learned clauses help in pruning the search space of parts that are already known not to contain a solution. They just help to get out of these parts of the search space more quickly. However learned clauses are additional sentences that can be omitted when merely testing for the satisfiability of a given solution. That is why DualSat employs old style data structures for the core problem given as input and new lazy data structures for learned clauses. It has shown that the runtime penalty for this is manageable as most clauses in a modern SAT-solver are in deed learned clauses.
Even better the benchmark results of DualSat have shown that it is still competitive with solvers like ZChaff and Clasp when only finding one solution, a case DualSat has not prevalently been optimized for. ZChaff solved one more instances and Clasp two more instances of the benchmark set from rutgers.edu than DualSat in 60 seconds (16 unsolvale, 242 instances). For counting solutions DualSat was considerably better than Clasp. For problems like the optimization problem mentioned before DualSat may be the only option since Clasp returns results one-by-one, ZChaff focuses on a singleton solution and sharpSAT only returns a solution count.
As far about simple solution classes. With extended solution classes DualSat terminates for a given solution class not just as soon as all clauses are satisfied but even before when a given solution class is in so called DNNF (Decomposable Negation Normal Form) [DwDN01]. That is the case if the variables of all remaining clauses are unentangled. It means that each variable shows up in at most one remaining unsatisfied clause. The corresponding solution class can then be written like 11x(-2)(-2)(+2)x(+3)(-3). A solution class like 10(-2)(2)(-2) can be decomposed into 100xx, 10x1x and 10xx0. We show on how to count such a class in chapter 2.3.
Besides this DualSat realizes a couple of other new ideas which may prove beneficial for future SAT-solvers. At first it does not merely rely on a conflict based heuristic like VSIDS [BFS15]. When there are little conflicts like in randomly generated SAT problems or the instance collection of Cachet, DualSat employs a refined version of BOHM’s and the Jeroslow-Wang heuristic [MqSv99]. That way DualSat can solve about 40% of the model count problems from Cachet DQMR while Clasp could not solve any of them.
Another milestone of DualSat is its stack redoing feature. Current SAT-solvers employ nonchronological backtracking. That is if a conflict is encountered and a learned conflict clause is generated then the solver jumps back up to the assertion level where the new learned conflict clause becomes unit and can en-queue the sole unassigned non-false literal as derived fact. However by doing so the solver loses already made assignments and needs to begin starting from the assertion level from scratch. There is already early work which has been aware of this problem [PiDw07]. What DualSat does is to first go back to the assertion level to add the assertion literal but then to push all decision literals above again on the stack until the currently pushed decision literal leads to a conflict. When doing so it can also keep all inferenced literals that previously have been on that level. It only needs to add new literals and detect conflicts. We will call this process stack redo. Employing a stack redo DualSat can almost restart from where it had to break off due to a conflict.
The nogood handling of DualSat is also different from that of previous #SAT-solvers. Instead of recording nogoods for already visited solutions it creates nogoods on backtracking. Evidence has shown that shorter backtrack-nogoods do even speed up the solution process as they can prevent the solver from re-entering already explored parts of the search space. There is also a mechanism to get rid of nogoods as soon as possible. That is on variable complementation which appear due to search progress. Nogood deletion is also executed after a stack redo taking place directly after nogood creation when the nogood proves to have become implicitly true by all forthcoming literal assignments.
DualSat also performs restarts before the first solution has been reached. Restarting from scratch has proven to be beneficial as otherwise the solver can get stuck in a part of the search space which is hard to explore but does not contain any solution. Most modern solvers employ restarting and for #SAT this technique is especially beneficial on unsatisfiable instances. That way the solver learns as much as possible about the whole search space before it starts to enumerate solutions. Finally DualSat randomizes the initial assignment value between zero and one for problem instances where always trying zero first may be detrimental. It does so by a literal activity counter. BerkMin claimed this method to be slightly better than random initialization. Clause database reduction has been implemented very much the way as it is in BerkMin and that has proven to go well in practice [GoNk07]. If the solver would not forget old learned clauses that mostly contain information about already visited parts of the search space, the solver would work considerably slower.
Overall DualSat is a state of the art solver ready for use, which can unlock new problem types for SAT-solving. There are still a whole lot of things that could be improved about DualSat and continuing its development is likely to prove very worthwhile. However there are problems which DualSat cannot solve. Problems consisting of multiple contingency components are an example. Nonetheless such components can be detected very easily by adding all connected variables to a bitset, something which is f.i. doable by a preprocessor. Pipatsrisawat has tested for this use case by simply replicating the same problem four times. Even a common one-solution solver had been orders of magnitude slower on the compound problem [PiDw07]. This is due to the same problem having to be solved over and over again for each assignment the solver tries with the first contingency component of the compound problem. Current #SAT solvers like first Relsat know that checking for contingency components can pay off also after every step when it comes to the harder task of model counting. Each smaller individual subproblem only needs to be solved once. Additionally, as soon as a component is discovered unsatisfiable the whole problem is. Elaborate solvers specifically optimized for #SAT like Cachet or sharpSAT do also employ a technique called component caching as the same component may be rediscovered once the solution graph falls apart by assigning new variables. In that graph variables in the same disjunctive clause need to be connected with edges while variables become vertices [BHMW08] .
2 SAT-Solver Technology
2.1 Preliminaries
2.1.1 Encoding a Problem as SAT
A propositional formula is an expression made up of logical and, logical or and the unary not as well as propositional variables that can take the truth value one and zero or true and false respectively. The constants true and false can be evaluated against the and- and the or-operator due to the neutral element (0 for V, 1 for A) and the dominant element (0 for A, 1 for V). Such a constant should thus only be necessary in an expression in case of a tautology (always true) or a contradiction (always false). If we want to normalize an expression we can push the not-operator - from bracketed expressions up to the leaves posed by variables or constants. The logical axiomon that implements this is called De Morgan ( -(aVb) « -aA-b, -(a Ab) « -aV-b ). It can be easily remembered as a rule to replace a repeat-until loop by a while loop: Fetch water until a and b are true or as long as a or b are not satisfied. The next important axiomon of a boolean algebra which we can apply is distributivity. Or is distributive against and. And is distributive against or. For multiplication and addition it is only the multiplication that is distributive against addition. So we have a V (bAc) « (aVb) A (aVc) and a A (bVc) « (aAb) V (aAc). If we now apply either of these rules exhaustively we get a propositional formula that is in Conjunctive Normal Form (CNF) or in a Disjunctive Normal Form (DNF). As can be seen easily a problem in disjunctive normal form simply enumerates all solutions with or. That is if we succeed to bring a logical formula into DNF we have already won. However consider the cost of applying and-distributivity exhaustively. For the first two-variable-bracket the number of subexpression doubles and so on for any subsequent bracket resolution.
Unfortunately a problem is typically given in CNF. We have a set of expressions which need to be fulfilled (i.e. be true) all together. Let us look on how to encode an implication like aAb^c into a CNF. First ‘ex falso quodlibet’ so either aAb can be false (-aV-b) or otherwise our conclusion needs to be true to maintain a true implication. That is -aV-bVc. If we have multiple clauses or axiomons we connect them with ‘A’. Consider the CNF (-aV-bVc) A (-cVa). It can be written as a set of sets, that is { {-a,-b,c}, {-c,a} }. This is the way modern SAT solvers store their input CNF. The symbols a, b, c are thereby replaced by integer numbers, i.e. { {-1,-2,+3}, {3,+1} }. There have only been a very few solvers which do not accept their propositional input system as CNF. That were HeerHugo and Stâlmark’s algorithm which do also operate on the logical equivalence operator and on subexpressions. The whole CNF denoted by a set of sets is a propositional sentence while each individual subset joined by logical disjunction is called a clause. Each member of one of these subsets is called a literal. A literal can be a variable or its negation. The whole expression is called satisfiable if it has at least one solution. Otherwise it is unsatisfiable.
The whole problem of solving a CNF is logically isomorph to finding a set of literals where no clause is a subset (C) of these literals and no superset of this set can have a clause as its subset. For a full assignment it boils down to simple subset checking. A clause a Vb Vc can also be written as -(-aA-bA-c) and that is where the name nogood stems from. We use it here as a synonym for clause, although the subset test must be taken against the negation of the literals of a clause-set. In DualSat the term nogood is used for learned clauses that must not be forgotten in order to prevent non-disjoint or repeated solutions, which is necessary for solution counting. Two sets are disjoint if anb = 0.
Another common property is subsumption that is a clause is subsumed by a subset-clause and can then be left out, i.e. aVb aVbVc. The input CNF can and especially for DualSat should be an axiomon set without derived sentences that can be implied by the axiomons. We have already mentioned in the introduction that operations for input clauses are more expensive to DualSat than operations on learned clauses. Before DualSat was developed, subsumption checking has already been one of many operations that can be performed by a preprocessor [EeBi05].
2.1.2 Resolution, Preprocessing
A common operation applied to clauses is resolution: F « (aVbVc) A (-aVdVe) ^ bVcVdVe. Intuitively variable a can be true or false. If it is true then dVe need to be valid, otherwise bVc needs to be valid. Formally tautology « (aV-a) ^(F) F|a V F|—a « (dVe) V (bVc) whereby FAp ^ F|p. F|p is pronounced F under p and means F where all occurrences of p are replaced by true and all occurrences of -p are replaced by false. (bVcVdVe) is called the resolvant. Learned clauses are obtained from the clause that caused a conflict (contradiction with the actual assignment) by resolving it against the ‘cause’ of other contained literals. Such a cause is another clause with one of its literals negated. We will clarify later on how it works.
Clause learning is not the only application of resolution. The Davis Putnam algorithm is an algorithm that fully relies on resolution [BHMW08]. It eliminates each variable one by one. If more than two clauses with a and -a appear, then each clause containing a needs to be joined with each clause containing -a, while the original clauses that contained an a-literal can be forgotten.
This step is refutation complete. It means if F « (AVp) A (BV-p) A R has at least one solution then also (AV B) A R needs to have at least one solution. If F is inconsistent then it needs to be false whether p amounts to false or true. In the first case F reduces AAR, and in the second case to BAR. So F is inconsistent if and only if AAR as well as BAR are both inconsistent. That is exactly the case if (A A R) V (BA R) is inconsistent. The or-operator only yields false when both of its operands yield false. Now we know that (AAR) V (BAR) « (AVB) A R is inconsistent [DvPt60]. A and B can both be a conjunction of subclauses. If they are resolved distributively against each other then this does exactly what the Davis Putnam algorithm does: Combine each clause with an a with each other clause that contains a -a.
The final solution is obtained by going back each step in reverse order. Up to then all variables except p are already known. By substituting the known variables you get a logical expression solely containing p. Simplify it. Then set p true or false respectively. The final expression can also resolve to a tautology not containing p. Then p may take any value.
It can be shown that the Davis Putnam algorithm does not just find any solution but it can be used to find all solutions. (AVp) A (BV-p) « (AAB) V (AA-p) V (BAp). A solution for AAB logically also holds in AVB, i.e. AAB AVB (The latter could have even more.). A solution for
(AA-p) V (BAp) logically also holds in (AVB). So no solution is lost by the transformation. We have shown before that the other direction, that each solution for (AVB) A R is also a solution for F, works in deed as well through back-substitution.
Today the Davis Putnam algorithm is no more applied in practice. It has high space requirements since an expression containing all solutions needs to be kept at once in memory till the end. The effectivity of Davis Putnam very much depends on the variable selection order. However there is only one order for the whole algorithm and not one independent order for each explored branch like in the Davis Putnam Loveland Longman (DPLL) algorithm which has nowadays become the dominant way for solving SAT. Obviously this is less flexible.
Nonetheless the method of the Davis Putnam algorithm is still widely used in preprocessing. That is before the DPLL algorithm is applied. The NiVER preprocessor only eliminates a variable when the number of literals in the resulting clause is reduced by the elimination [SuPr04]. It was reported to lead to a 74% decrease in the number of variables, a 58% decrease in the number of clauses and a 46% decrease in the literal count. More elaborate preprocessors can detect definitions like the definition of an and-gate x^aAb. This means that every occurrence of -x can be replaced by -aV-b (aAb^x, reverse implication) and that every occurrence of x needs to be duplicated, once for a and once for b (x^aNb) . This amounts to only compute resolvents with the member clauses of the gate definition. All other resolvents are logically implied by these primary resolvents [EeBi05]. We have already mentioned subsumption checking in chapter 2.1 which is another step taken by preprocessors. Sometimes one part of a gate definition needs to be completed f.i. -aV-b by -aV-b Vx to make the preprocessor detect the definition.
Preprocessing is already known to be of advantage for one-solution SAT-solvers. The benefit for DualSat would even be higher because of its dual data structures which require a well reduced set of core clauses. Unfortunately we did not have any preprocessor at hand to test DualSat with. We would expect considerable runtime gains since watched literals are known to be eight times faster than the literal counters still used for the core clauses [GuMi05].
2.2 DPLL Solvers
We have already mentioned that today's solvers are widely based on the Davis Putnam Loveland Longman (DPLL) algorithm. It tries the other value for a variable if it did not already have success with the initially assigned value. That is like a depth first search so that there is no need to keep expressions for all possible solutions in memory. In its simplest form the DPLL algorithm employs chronological backtracking. Most modern solvers use conflict directed backjumping and clause learning. We will also discuss the strategy of DualSat. Stack redos can be seen as a new development based on conflict directed backjumping, overcoming the issue of lost assignments. We will also see how the basic DPLL algorithm can be modified in order to return all possible solutions instead of just one.
2.2.1 DPLL with Chronological Backtracking
We have already said that making a choice on a variable comes with a worst case performance penalty of doubling the execution time. One way to avoid unnecessary choices is unit propagation or Boolean Constraint Propagation (BCP). If all but one literals of a clause are false and the remaining literal is yet unassigned then make this literal true. If it would take the value false then the whole CNF would become unsatisfiable so we need to avoid this. The new literal assignment may now cause other clauses to become unit and propagate their sole unassigned literal as true. This is exactly the case if the newly assigned literal appears in another clause in negated form.
Abbildung in dieser Leseprobe nicht enthalten
Fig 1: recursive DPLL with chronological backtracking
Fig. 1 shows a recursive formulation of DPLL with chronological backtracking. The pure literal rule is only allowed if we want to find one solution. It says that if a literal does not appear in negated form in any clause, then we are allowed to make it true. However this does not mean that there would not also exist solutions with -p. Most current solvers do not implement the pure literal rule since checking for pure literals would be too costly.
Abbildung in dieser Leseprobe nicht enthalten
Fig 2: recursive DPLL returning all solutions with chronological backtracking
Chronological backtracking is only the most simple form to implement DPLL. In order to refine our algorithm further we need to formulate it iteratively.
Abbildung in dieser Leseprobe nicht enthalten
Fig 3: iterative DPLL returning all solutions, chronological backtracking
It would have been possible to formulate DPLL in fig. 3 iteratively without goto. However we believe it to be more clear with goto since that saves us from double checking whether a is conflicting or all clauses are satisfied. We will extend this algorithm further in the section about conflict directed backjumping and in the section about stack redos. The complexity of the code will increase and so will the quest for accurate flow control.
The code in next_assignment does nothing more than to explicitly take control of the assignment stack. Each level starts with a decision literal p, that is a literal which has explicitly been selected by extend_assignment as opposed to literals inferenced by unit propagation. What DPLL in fig. 2 does on return, is to pop the current activation record from the runtime stack. If p had not been complemented yet another call DPLL( a-p ) follows. Otherwise the procedure returns and another activation record is popped off the stack.
Level zero is special in this regard as it contains no decision literal. It contains atomic facts made up of input clauses of length one. If a decision literal is searched for on level zero in next_assignment then the only remaining level gets popped, the while loop is left and the control returns from the DPLL procedure.
2.2.2 Clause Learning
Every literal assigned through unit propagation has a reason. That is the clause that had become unit in order to yield the literal. Now if a conflict is detected the conflict clause is of the form {-p,-q,C} where p and q are two literals assigned at the conflict level and C takes the place of all other literals in the conflict clause. There need to be at least two literals assigned at the conflict level because otherwise the clause would have become unit or conflicting before. Now the conflict clause can be resolved against the reasons of literals p and q. The resulting clause contains neither variable p nor variable q but some other literals which had been false before p and q were assigned. These literals can also be resolved. Current SAT-solvers go back in the assignment stack a until there remains only one literal assigned at the conflict level. This point is called the 1-UIP. Such a point is guaranteed to exist since the solver can go back up to the decision literal.
The whole dependency can be viewed as a graph. A unique implication point is a point that dominates all paths between the decision literal of the current level and the conflicting clause. Variable assignments are vertices. For each reason and each false literal of the reason an edge goes from the false literal to the yielded unit assignment. The side with the decision literals is called the decision side and the side with the conflict clause is called the conflict side. Each specific resolution step corresponds to a cut in the graph. The desired cut for the 1-UIP cuts through all edges that originate there. Each step back replaces the edges originating in the resolved variable with those that end there. Examples of implication graphs can be viewed in [BHMW08] and [ZMM01].
The procedure for conflict analysis takes the conflict clause as input and iterates over all literals of the current clause. Yet unseen literals of lower levels are added immediately to the output clause while a counter is incremented for literals of the current level. Then it goes back in the assignments of the current level and takes the reason for the current assignment, makes the reason the current clause and decrements the counter of seen literals of the current level. Finally when the counter reaches zero the only literal of the current level is written into the output clause. An implementation of this procedure as well as other important procedures for solvers with lazy data structures can be seen in the article about Minisat [EeS03].
Why do almost all solvers focus on the 1-UIP? First of all the 1-UIP tends to have fewer literals than the 2-UIP as for each newly resolved clause literals of lower levels may be added. Second we want a clause with exactly one literal of the conflict level. This literal is called the asserting literal. Then most current SAT-solvers jump back directly to the lowest level where the newly learned clause becomes unit. This level is called the assertion level. It is the second highest level of all literals in the clause. The highest level is the conflict level from which the assertion literal stems from.
It can be regarded as ideal if the 1-UIP clause happens to locate on half way between the decision literal and the conflict. If it is too far away from the conflict it may be arbitrarily different showing little similarity with the conflict. Besides this a learned clause that is far away from its origin may not be useful because it is simply too long. The more literals that need to become false before the clause yields a unit literal, the less probable is that unit propagation executes on it. If it is too near to the conflict on the other hand it will be too similar and thus have little power to prevent further conflicts. That is why Jin and Somenzi suggest to generate an additional learned clause when the 1-UIP seems to be far away from what is needed [JiSo06]. Such a clause is only generated if there are multiple conflicts on the same clause and when the length of the new clause is appealing. The additional learned clause does not need to be asserting. This means it may contain multiple literals of the conflict level. So one clause is needed for backjumping and another clause for a better pruning of yet-to-be-visited swaths of the search space.
2.2.3 DPLL with Conflict Directed Backjumping
We have described in the previous chapter on how to create a 1-UIP learned clause. This clause is asserting as it only contains one literal of the conflict level. The second highest level of literals in this clause is the assertion level. Current solvers do now perform a backjump to the assertion level and en-queue the asserting literal there from the conflict level. After propagation of unit constraints the search continues from this level, selecting new literals possibly different from what has been selected before.
Abbildung in dieser Leseprobe nicht enthalten
Fig 4: DPLL with conflict directed backjumping
Fig. 4 shows pseudo code for that algorithm. The major advantage of this implementation is that it gets out of the conflict space quickly. With chronological backtracking it would only go back to the next previous uncomplemented level, the next level where both variable choices have not yet been explored. However this level may turn out to produce the same conflict in a similar subtree and the whole process starts over and over again. By non-chronological backtracking we can be sure that the solver gets out of the conflicting space by a singleton backjump. This saves valuable time.
We have added a code line to avoid returning duplicate solutions. For any non disjoint solution subtract that solution from the newly found solution. Remember that each partial assignment corresponds to a set of solutions where the unassigned variables can take any value. While we have written setminus as an operation on sets the algorithm will need to operate on partial assignments. Before s is subtracted from a, we test whether the intersection of both sets is empty. This is the case if there is a conflicting assignment xVxs. Whenever that happens there is nothing to subtract. The second case to consider is when aCs. This can be detected for each assignment to be either the same in a and s or not present in s. If so no new solution has been found. The final case to consider is when the set difference yields a smaller set for a’ than a was initially. It is computed by assimilating all assignments from s which are not yet present in a in complemented form.
2.2.4 DPLL with Stack Redo
Conflict directed backjumping jumps back to the level where the assertion literal can be enqueued. In case of a stack redo it also starts like this. However then it tries to reestablish the previous assignment stack level by level. This may succeed for some decision literals and their levels but produce a conflict somewhere in between the backtrack level and the conflict level. It does not need to start from scratch for every level but it can put everything that was previously known to be on that level in the assignment queue before starting unit propagation.
Reinitializing the assignment queue for each level that is redone has the purpose that new literals can be inferenced out of the assertion literal on each level above the assertion level in addition to the old stack content. A stack redo combines the efficiency of conflict directed backjumping with the sequential search order of chronological backtracking. Since no swath of the search space is visited again stack redoing is even more efficient than simple conflict directed backjumping. The sequential search order guarantees that no duplicate solutions can be returned.
What the stack redo does is in deed a combination of chronological backtracking, conflict directed backjumping and a re-establishment of the previous stack content. At first it starts with chronological backtracking. If the assertion level is at least as high as the backtrack level for backjumping it already ends here. The difference is that the top literal is already complemented and the assertion literal can thus no more be enqueued. Already flipping the literal brings the search faster forward than a backjump search which needed to explore the unflipped state first. In case that there was no conflict but search simply continues to find the next solution after a previous solution has been yielded, it also ends here.
However in the majority of the cases the assertion level lies far deeper in the stack. Chronological backtracking would now continue from the current level and likely re-explore the same conflict in a newly built search-subtree. It would do so for one level after the other until it gets out of the conflict area. This can be very time consuming. Instead of searching for the first nonconflicting level from the top down as chronological backtracking does a stack redo jumps down to the assertion level and searches from the bottom up till the last level where no conflict is discovered. All levels above the first conflicting level are now known to be also conflicting and can thus be skipped for chronological backtracking. What the stack redo does on the first conflicting level (called the hook level) is to continue chronological backtracking from there.
In detail there are two possible cases to be considered when the stack is reestablished. The first case is that a new conflict is discovered at the unit propagation of the current level when it tries to inference additional literals. If a new conflict is detected the whole procedure restarts from the very beginning, now with the new conflict instead of the old one. Another case to consider is that some literal in the old stack content now already appears in complemented form on a lower level. This is clearly a contradiction and it means that the current level can not be redone. However now we do not have a classical conflict but simply two contradictory literals. As it is always legal to continue with chronological backtracking instead of conflict analysis this is right what we do then.
Some additional conditions need to be checked for when doing a stack redo, namely checking for duplicate literals in addition to contradictory literals. Duplicate literals can appear somewhere in the middle of the inferenced literals of the current level and are then simply deleted in place maintaining the order of the other literals for conflict analysis. If a decision literal happens to be a duplicate literal then the whole level can be cropped as all its literals have already been inferenced by unit propagation on a lower level. The last condition to check for is that a decision literal can become a duplicate literal after it has been flipped by a continuation of chronological backtracking. In this case the current level is also cropped and the search can continue selecting a new decision literal.
Abbildung in dieser Leseprobe nicht enthalten
Fig 5: DPLL with stack redo
The main difference between a literal being in the queue and in the trail a is that it has not yet been unit propagated as long as it is in the queue. The assignment queue is then de-queued literal by literal propagating each literal and finally placing it in the trail a. Unit propagation needs to be re-executed because the new literal on the assertion level may yield new propagation results.
The major advantage of stack redos is that they save previous work where the literals between the backtrack level and the redo level do only need to be supplemented by new literals. It does not need to re-explore that whole search space.
To make the implementation more efficient DualSat does not shuffle the data from the trail into the queue and then back into the trail but it virtually adds the literals that have been on the current redoing level previously into the queue. This means the de-queue operation first looks for previous literals on the current level and then on what really is in the queue.
The implementation becomes a bit tricky when the solver detects a conflict while it is redoing the virtual queue. It will need to jump back to conflict analysis thereafter but this code section and especially the conflict analysis there will expect everything that has been redone successfully in the trail and the literal that caused the conflict at the front of the queue. All other trail literals that pertain to the virtual queue must be deleted then. Their level and reason is unset in order to leave clean data structures. Unsetting the reason is important for unlocking clauses. As long as a clause remains the reason for a unit propagation implication, it must not be deleted when tidying up old clauses because it could be needed for conflict analysis. You can see this procedure in fig. 5 at “if new_conflict”.
Special precautions must be taken if a literal should be redone that has now already been inferenced on a lower level. Such a literal is deleted from the virtual queue. For a possible later conflict analysis the order of the literals must be maintained thereby. When the literal to be deleted happens to be a decision literal then the whole level needs to be removed, all the levels on top of it moving down one level.
Another case appears when for any literal which should be put into the virtual queue there happens to be already the same literal in negated form on a lower level. In this case we do not have a new conflict but the old stack content is simply conflicting with the newly derived literals. The current level cannot be redone in this case and the redo level will remain one level below. We say the current level becomes the hook level.
DualSat can now simply continue with new variable assignments falling through to the label extend_assignment. However it would be better if it did not make a choice on any variable next but on the same variable as before. If it does it can either complement this variable if it has not been complemented yet or go to next_assignment to search for any uncomplemented variable down the stack. The effect is the same as if it would have done chronological backtracking until no more conflict appears.
Chronological backtracking goes down the stack until it finds an uncomplemented variable. If the current level is still conflicting it can continue this process until it arrives at a level without conflict. This is exactly what DPLL with stack redo does in effect. It searches the last level where there is no conflict from the bottom up and on the level above it applies next_assignment to flip the next variable down from there. The code needs a case distinction if the level above happens to be the level where chronological backtracking has ended before to already complement the decision variable. This variable then needs to be uncomplemented temporarily because next_assignment wants to complement it again. The final effect may be the same as for chronological backtracking but what a stack redo does is much faster in effect.
Let us look once more on what the stack redoing code section really does. At first it applies chronological backtracking. Then, if there has been no conflict or if it already has undone the stack till the assertion level (btlevel) it has finished and goes over to propagate. If the assertion level lies lower it continues to do the same as on a conflict directed backjump. However it does not forget the stack when backjumping but keeps everything in place for the following stack redo. We have already described how the stack redo works in detail. The stack redo can break with a new conflict in which case the whole procedure loops starting at chronological backtracking first. If the old stack content does simply not fit the new one, it continues with chronological backtracking. However all the levels in between the redo level and the conflict level can be skipped as they are already known to conflict with the new assignment inserted down below at the assertion level.
There is a little extra condition we need to take account of in case of continuing chronological backtracking: If it is the decision variable that appears in complemented form on a lower level then this decision variable which is on the so called hook level must not be simply complemented. Since its non-complemented form was conflicting its complemented form would be the same as down below in the stack. Now instead of establishing a duplicate decision variable, we simply continue with extend_assignment selecting a new decision variable and this perfectly matches a continuation in sequential search.
One last note about the case in which no backjump appears because initial chronological backtracking was already successful. As the topmost literal is now complemented, we are not allowed to enqueue the assertion literal though we would be on the right level to do so. The new learned clause could only fire if the topmost literal was still in an unflipped state.
If we do chronological backtracking only, we do not need any nogoods as the whole solution space is searched through in sequential order. However initially DualSat did not continue with chronological backtracking but it was selecting new variables after stack redo on from the level where the redo was no more successful. If you do this you still lose some part of the execution or search state. Then it is possible that the same solution is visited again. This was initially solved by adding nogoods. That are learned clauses which explicitly prevent the solver from entering the same search space again.
2.2.4.1 Practical Examples for the Stack Redo
In this section we want to present examples for the stack redo algorithm described in the previous section.
Abbildung in dieser Leseprobe nicht enthalten
Fig 6: full stack redo starting with chronological backtracking
Fig. 6 shows an arbitrary stack content at the left. Decision literals which have already been complemented are shown underlined. The middle column shows the same stack content after chronological backtracking. Since h and g have already been complemented, they are popped from the trail and the decision literal which is then found at the top is complemented thereupon (here: f).
Now a stack redo continues analyzing the conflict that has caused backtracking. If we resolve the last two clauses in ‘rules on the conflict level’ then we receive (-k,-n,-b). The -n literal does however not become part of the learned clause because it is a level zero literal. Level zero literals are atomic facts that will always hold true for any solution. Note that the 1-UIP can be found at k which means that the conflict directed backjump does not need to insert -h on a level below. If the rule were (-h,-c,k) instead of (-h,k) that would be level two rather than level one.
The assertion literal is -k. The second highest level in the learned clause is the level of -b. Going to this level (the assertion level) we enqueue -k. The additional rules we have listed do now cause x, y and z to become inserted on the remaining redo levels. In this example a full stack redo does succeed keeping the complemented literal -f at the top. The execution thread now falls through to the label extend_assignment.
Abbildung in dieser Leseprobe nicht enthalten
Fig 7: when the old stack content conflicts with the new one
Unfortunately in practice it is rather an exception if a stack redo succeeds to reestablish all previous levels. It is more likely that one of the newly established literals either conflicts with the previous stack content or that it causes a completely new conflict on an intermediate level. The former is the case in fig. 7. When literal e should be reestablished that causes a conflict. This means that the redo level remains at level one and level two becomes the hook level. As described in the previous section the literal on the hook level is complemented starting chronological backtracking from there.
The algorithm behaves slightly different if it is not the old stack content that is conflicting with the new one, but if an additional conflict is raised and discovered as a consequence of enqueueing the assertion literal. A valid example for this would be caused by (-y,q) and (-y,-q) for level 2 as shown in fig. 6 if (k,-e) is missing. This will invoke another conflict resolution. It would discover that the fact y is atomically true and enqueue it on level zero. As the conflict level also happens to be level two, chronological backtracking would likewise be started from there also complementing c.
Abbildung in dieser Leseprobe nicht enthalten
Fig 8: removal of duplicate literals and levels
Now we want to show how duplicate literals that have newly been inferenced on a lower level become deleted. The first such literal in fig. 8 is c. Since it is a decision literal the whole level can be cropped. Literal x on the contrary only causes itself and the dependent literal i to be removed on that level which now falls down from altitude three down to two. Finally the whole redo succeeds with -g at level 3.
Abbildung in dieser Leseprobe nicht enthalten
Fig 9: stack redo: same literal on lower level
Finally we show a conflicting decision literal in fig. 9. Normally we would establish -c on level two by complementing the existing decision literal c. As -c does already appear on level one, it must not be reestablished as decision literal on level two. Instead the code jumps to extend_assignment selecting a new decision literal w.
[...]
-
-
-
-
¡Carge sus propios textos! Gane dinero y un iPhone X. -
-
¡Carge sus propios textos! Gane dinero y un iPhone X. -
-
¡Carge sus propios textos! Gane dinero y un iPhone X. -
-
¡Carge sus propios textos! Gane dinero y un iPhone X. -
-
¡Carge sus propios textos! Gane dinero y un iPhone X. -
-
¡Carge sus propios textos! Gane dinero y un iPhone X. -
-
¡Carge sus propios textos! Gane dinero y un iPhone X. -
-
¡Carge sus propios textos! Gane dinero y un iPhone X. -
-
¡Carge sus propios textos! Gane dinero y un iPhone X. -
-
¡Carge sus propios textos! Gane dinero y un iPhone X. -
-
¡Carge sus propios textos! Gane dinero y un iPhone X. -
-
¡Carge sus propios textos! Gane dinero y un iPhone X. -
-
¡Carge sus propios textos! Gane dinero y un iPhone X. -
-
¡Carge sus propios textos! Gane dinero y un iPhone X.