The Quest for Efficient Boolean Satisfiability Solvers (Презентации лекций), страница 4

In particular, the experimentssuggest that the mechanism called Head/Tail list with Literal Sifting actuallyoutperforms the 2-literal watching mechanism for BCP. However, the experiments arecarried out in a framework implemented in Java. The authors admit that it may notrepresent the actual performance if implemented in C/C++.3.2.2 Other Deduction MechanismsBesides the unit clause rule, there are other rules that can be incorporated into adeduction engine. In this section, we briefly discuss some of them. We want to pointout that though many of the deduction mechanisms have been shown to work oncertain classes of SAT instances, unlike the unit clause rule, none of them seems towork without deteriorating the overall performance of the SAT solver for generalSAT instances.One of the most widely known rules for deduction is the pure literal rule [6]. Thepure literal rule states that if a variable only occurs in a single phase in all theunresolved clauses, then it can be assigned with a value such that the literal of thevariable in that phase evaluates to 1.

Whether a variable satisfies the pure literal ruleHead/Tail ListHAction2-Literal WatchingCommentT-V1 V4-V7 V12 V15-V1 V4-V7 V12 V15Initially Head/Tail shouldbe at the beginning/end ofthe clauses, while watchedcan point to any freeliteral-V7 V12 V15Clause will be visited onlyif the pointers need to bemoved.-V7 V12 V15Head can only move towardstail and vice versa, whilewatched can move freely.-V7 V12 V15When all but one literal isassigned value 0, the clausewill be a unit clause-V7 V12 V15When backtrack, Head/Tailneed to be undone, whilewatched need to do nothing-V7 V12 V15If a literal is assigned 1,the clause containing itwill not be visited for bothcases.-V7 V12 V15During searching for freeliteral, if a value 1literal is encountered,Head/Tail scheme will donothing, while watched willmove the watched pointerV1=1@1TH-V1 V4H-V1 V4H-V1 V4H-V1 V4-V7 V12 V15-V1 V4V7=1@2V15=0@2T-V7 V12 V15-V1 V4V4=0@3Both generatean implicationT-V7 V12 V15T-V7 V12 V15-V1 V4Suppose conflict,we backtrack todecision level 1-V1 V4V12=1@2V7=0@2H-V1 V4T-V7 V12 V15-V1 V4V4=0@1H-V1 V4T-V7 V12 V15V4Free LiteralV4Value 0 Literal-V7Value 1 LiteralV7=1@2-V1 V4HHead LiteralTTail LiteralSet V7 to be 1 at decision level 2Watched LiteralFig.

3. Comparison of Head/Tail List and 2-Literal Watchingis expensive to detect during the actual solving process, and the consensus seems tobe that incorporating the pure literal rule will generally slow down the solving processfor most of the benchmarks encountered.Another explored deduction mechanism is equivalence reasoning. In particular,eqsatz [32] incorporated equivalence reasoning into the satz [22] solver and foundthat it is effective on some particular classes of benchmarks. In that work, theequivalence reasoning is accomplished by a pattern-matching scheme for equivalenceclauses.

A related deduction mechanism was proposed in [33]. There, the authorspropose to include more patterns in the matching process for simplification purpose indeduction.The unit literal rule basically guarantees that all the unit clauses are consistent witheach other. We can also require that all the 2 literal clauses be consistent with eachother and so on.

Researchers have been exploring this idea in the deduction process inworks such as [34, 35]. In particular, these approaches maintain a transitive closure ofall the 2 literal clauses. However, the overhead of maintaining this information seemsto far outweigh any benefit gained from them on the average.Recursive Learning [36] is another reasoning technique originally proposed in thecontext of learning with a logic circuit representation of a formula.

Subsequentresearch [37] has proposed to incorporate this technique in SAT solvers and foundthat it works quite well for some benchmarks generated from combinational circuitequivalence checking problems.3.3 Conflict Analysis and LearningWhen a conflicting clause is encountered, the solver needs to backtrack and undo thedecisions. Conflict analysis is the procedure that finds the reason for a conflict andtries to resolve it.

It tells the SAT solver that there exists no solution for the problemin a certain search space, and indicates a new search space to continue the search.The original DPLL algorithm proposed the simplest conflict analysis method. Foreach decision variable, the solver keeps a flag indicating whether it has been tried inboth phases (i.e. flipped) or not. When a conflict occurs, the conflict analysisprocedure looks for the decision variable with the highest decision level that has notbeen flipped, marks it flipped, undoes all the assignments between that decision leveland current decision level, and then tries the other phase for the decision variable.This method is called chronological backtracking because it always tries to undo thelast decision that is not flipped. Chronological backtracking works well for randomgenerate SAT instances and is employed in some SAT solvers (e.g satz [22]).For structured problems (which is usually the case for problems generated fromreal world applications), chronological backtracking is generally not efficient inpruning the search space.

More advanced conflict analysis engines will analyze theconflicting clauses encountered and figure out the direct reason for the conflict. Thismethod will usually backtrack to an earlier decision level than the last unflippeddecision. Therefore, it is called non-chronological backtracking.

During the conflictanalysis process, information about the current conflict may be recorded as clausesand added to the original database. The added clauses, though redundant in the sensethat they will not change the satisfiability of the original problem, can often help toprune search space in the future. This mechanism is called conflict-directedlearning. Such learned clauses are called conflict clauses as opposed to conflictingclauses, which refer to clauses that generate conflicts.Non-chronological backtracking, sometimes referred to as conflict-directedbackjumping, was proposed first in the Constraint Satisfaction Problem (CSP)domain (e.g.

[38]). This, together with conflict-directed learning, were firstincorporated into a SAT solver by Silva and Sakallah in GRASP [25], and by Bayardoand Schrag in rel_sat [18]. These techniques are essential for efficient solving ofstructured problems.

Many solvers such as SATO [19] and Chaff [20] haveincorporated similar technique in the solving process.Previously, learning and non-chronological backtracking have been discussed byanalyzing implication graphs (e.g. [17, 39]). Here we will formulate learning as analternate but equivalent resolution process and discuss different schemes in thisframework.Researchers have adapted the conflict analysis engine to some deduction rulesother than the unit clause rule in previous work (e.g. [33, 37]).

However, because theunit clause rule is usually the only rule that is incorporated in most SAT solvers, wewill describe the learning algorithm that works with such a deduction engine. In sucha solver, when a variable is implied by a unit clause, the clause is called theantecedent of the variable. Because the unit clause rule is the only rule in thededuction engine, every implied variable will have an antecedent. Decision variables,on the other case, have no antecedents.In conflict driven learning, the learned clauses are generated by resolution.Resolution is a process to generate a clause from two clauses analogous to the processof consensus in the logic optimization domain (e.g.

[40]). Resolution is given by(x + y ) (y’ + z) ≡ (x + y ) (y’ + z)(x + z)The term (x + z) is called the resolvent of clause (x + y) and (y’ + z). Because of this,we have(x + y ) (y’ + z) → (x+z)Similar to the well-known consensus law (e.g. [40]), the resulting clause ofresolution between two clauses is redundant with respect to the original clauses.Therefore, we can always generate clauses from original clause database by resolutionand add the generated clause back to the clause database without changing thesatisfiability of the original formula.

However, randomly choosing two clauses andadding the resolvent to the clause database will not generally help the solving process.Conflict-driven learning is a way to generate learned clauses with some direction inthe resolution process.The pseudo-code for conflict analysis is shown in Fig. 4. Whenever a conflictingclause is encountered, analyze_conflict() will be called. Functionchoose_literal() will choose a literal from the clause. Functionresolve(cl1, cl2, var) will return a clause that contains all the literals incl1 and cl2 except for the literals that corresponds to variable var.