GRASP—A New Search Algorithm for Satisfiability (Презентации лекций), страница 3

This new implicate,referred to as a conflict-induced clause, provides the primarymechanism for implementing failure-driven assertions, nonchronological conflict-directed backtracking, and conflictbased equivalence (see Section 2.3). In TMS [16] and insome algorithms for CSP [11], “nogoods” provide conditionssimilar to conflict-induced clauses. Nevertheless, the basicmechanism for creating conflict-induced clauses differs.We denote the conflicting assignment associated with aconflict vertex κ by A C ( κ ) and the associated conflictinduced clause by ω C ( κ ) . The conflicting assignment isdetermined by a backward traversal of the implication graphstarting at κ .

Besides the decision assignment at the currentdecision level, only those assignments that occurred at previous decision levels are included in A C ( κ ) . This is justifiedby the fact that the decision assignment at the current decision level is directly responsible for all implied assignments atthat level. Thus, along with assignments from previous levels,the decision assignment at the current decision level is a sufficient condition for the conflict. To facilitate the computation of A C ( κ ) we partition the antecedent assignments ofκ as well as those for variables assigned at the current decision level into two sets.

Let x denote either κ or a variablethat is assigned at the current decision level. The partition ofA ( x ) is then given by:Λ(x) = { ( y, ν(y) ) ∈ A(x) δ(y) < δ(x) }Σ(x) = { ( y, ν(y) ) ∈ A(x) δ(y) = δ(x) }(2)For example, referring to the implication graph of Figure 1,Λ ( x 6 ) = { x 11 = 0 @3 } and Σ ( x 6 ) = { x 4 = 1 @6 } .Determination of the conflicting assignment A C ( κ ) cannow be computed using the following recursive definition:( x, ν ( x ) )AC ( x) = Λ ( x ) ∪if A ( x ) = ∅(3)∪( y, ν ( y ) ) ∈ Σ ( x )A C(y) otherwiseand starting with x = κ . The conflict-induced clause corresponding to A C ( κ ) is now determined according to:ωC ( κ ) =∑( x, ν ( x ) ) ∈ AxCν ( x)(4)( κ)01where, for a binary variable x, x ≡ x and x ≡ ¬x . Application of (2)-(4) to the conflict depicted in Figure 1 yields thefollowing conflicting assignment and conflict-induced clauseat decision level 6:A C ( κ ) = { x 1 = 1, x 9 = 0, x 10 = 0, x 11 = 0 }(5)ω C ( κ ) = ( ¬x 1 + x 9 + x 10 + x 11 )3.1 Standard Conflict Diagnosis EngineThe identification of a conflict-induced clause ω C ( κ )x 9 = 0 @1ω8x 10 = 0 @3ω9x 1 = 0 @6ω7x 11 = 0 @3antecedent assignment of x1 due to (5)decisionlevelx 8 = 1 @6ω7κ′ω93ω9x 13 = 1 @25x 7 = 1 @6x 12 = 1 @2x1160(a) Conflicting implication sequence(b) Decision treeFigure 3: Non-chronological backtrackingenables the derivation of further implications that helpprune the search.

Immediate implications of ω C ( κ ) includeasserting the current decision variable to its opposite valueand determining a backtracking level for the search process.Such immediate implications do not require that ω C ( κ ) beadded to the clause database. Augmenting the clause database with ω C ( κ ) , however, has the potential of identifyingfuture implications that are not derivable without ω C ( κ ) .In particular, adding ω C ( κ ) to the clause database insuresthat the search engine will not regenerate the conflictingassignment that led to the current conflict.3.1.1Failure-Driven Assertions. If ω C ( κ ) involves thecurrent decision variable, erasing the implication sequence atthe current decision level makes ω C ( κ ) a unit clause andcauses the immediate implication of the decision variable toits opposite value.

We refer to such assignments as failuredriven assertions (FDAs) to emphasize that they are implications of conflicts and not decision assignments. We note further that their derivation is automatically handled by ourBCP-based deduction engine and does not require specialprocessing. This is in contrast with most search-based SATalgorithms that treat a second branch at the current decisionlevel as another decision assignment. Using our runningexample (see Figure 1) as an illustration, we note that aftererasing the conflicting implication sequence at level 6, theconflict-induced clause ω C ( κ ) in (5) becomes a unit clausewith ¬x 1 as its free literal.

This immediately implies theassignment x 1 = 0 and x 1 is said to be asserted.3.1.2Conflict-Directed Backtracking. If all the literals inω C ( κ ) correspond to variables that were assigned at decision levels that are lower than the current decision level, wecan immediately conclude that the search process needs tobacktrack. This situation can only take place when the conflict in question is produced as a direct consequence of diagnosing a previous conflict and is illustrated in Figure 3 (a) forour working example. The implication sequence generatedafter asserting x 1 = 0 due to conflict κ leads to anotherconflict κ′ .

The conflicting assignment and conflict-inducedclause associated with this new conflict are easily determinedto beA C ( κ′ ) = { x 9 = 0, x 10 = 0, x 11 = 0, x 12 = 1, x 13 = 1 }(6)ω C ( κ′ ) = ( x 9 + x 10 + x 11 + ¬x 12 + ¬x 13 )and clearly show that the assignments that led to this secondconflict were all made prior to the current decision level.In such cases, it is easy to show that no satisfying assignments can be found until the search process backtracks to thehighest decision level at which assignments in A C ( κ′ ) weremade. Denoting this backtrack level by β , it is simply calculated according to:β = max { δ(x) ( x, ν(x) ) ∈ A C ( κ′ ) }(7)When β = d – 1 , where d is the current decision level, thesearch process backtracks chronologically to the immediatelypreceding decision level. When β < d – 1 , however, thesearch process may backtrack non-chronologically by jumping back over several levels in the decision tree.

It is worthnoting that all truth assignments that are made after decisionlevel β will force the just-identified conflict-induced clauseω C ( κ′ ) to be unsatisfied. A search engine that backtrackschronologically may, thus, waste a significant amount oftime exploring a useless region of the search space only todiscover after much effort that the region does not containany satisfying assignments. In contrast, the GRASP searchengine jumps directly from the current decision level back todecision level β .

At that point, ω C ( κ′ ) is used to eitherderive a FDA at decision level β or to calculate a new backtracking decision level.For our example, after occurrence of the second conflictthe backtrack decision level is calculated, from (7), to be 3.Backtracking to decision level 3, the deduction engine creates a conflict vertex corresponding to ω C ( κ′ ) .

Diagnosis ofthis conflict leads to a FDA of the decision variable at level 3(see Figure 3 (b)).The pseudo-code illustrating the main features of thediagnosis engine in GRASP is shown in Figure 2. Generalproofs of the soundness and completeness of GRASP can befound in [7, 14].3.2 Variations on the Standard Diagnosis EngineThe standard conflict diagnosis, described in the previous section, suffers from two drawbacks. First, conflict analysis introduces significant overhead which, for some instancesof SAT, can lead to large run times.

Second, the size of theclause database grows with the number of backtracks; in theworst case such growth can be exponential in the number ofvariables.The first drawback is inherent to the algorithmic framework we propose. Fortunately, the experimental results presented in Section 4 clearly suggest that, for specific instancesof SAT, the performance gains far outweigh the procedure’sadditional overhead.One solution to the second drawback is a simple modification to the conflict diagnosis engine that guarantees theworst case growth of the clause database to be polynomial inthe number of variables. The main idea is to be selective inthe choice of clauses to add to the clause database. Assumethat we are given an integer parameter k. Conflict-inducedclauses whose size (number of literals) is no greater than k aremarked green and handled as described earlier by the standard diagnosis engine. Conflict-induced clauses of sizegreater than k are marked red and kept around only whilethey are unit clauses.

Implementation of this scheme requiresa simple modification to procedure Erase(), which mustnow delete red clauses with more than one free literal, and tothe diagnosis engine, which must attach a color tag to eachconflict-induced clause. With this modification the worstcase growth becomes polynomial in the number of variablesas a function of the fixed integer k.Further enhancements to the conflict diagnosis engineinvolve generating stronger implicates (containing fewer literals) by more careful analysis of the structure of the implication graph. Such implicates are associated with thedominators [15] of the conflict vertex κ . These dominators,referred to as unique implication points (UIPs), can be identified in linear time with a single traversal of the implicationgraph.

Additional details of the above improvements to thestandard diagnosis engine can be found in [15].4 Experimental ResultsIn this section we present an experimental comparisonof GRASP with two state-of-the-art and publicly availableSAT programs, TEGUS [17] and POSIT [5]. TEGUS wasadapted to read CNF formulas and augmented to continuesearching when all its default options were exhausted inorder to abort fewer faults. No changes were made to POSIT.GRASP and POSIT have been implemented in C++,whereas TEGUS has been implemented in C.