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

Extending the current assignment by following the logicalconsequences of the assignments made thus far. Theadditional assignments derived by this deduction processare referred to as implication assignments or, more simply,implications. The deduction process may also lead to theidentification of one or more unsatisfied clauses implyingthat the current assignment is not a satisfying assignment.Such an occurrence is referred to as a conflict and theassociated unsatisfying assignments, called conflictingassignments.3. Undoing the current assignment, if it is conflicting, so thatanother assignment can be tried.

This backtracking processis the basic mechanism for retreating from regions of thesearch space that do not correspond to satisfyingassignments.The decision level at which a given variable x is either electively assigned or forcibly implied will be denoted by δ ( x ) .When relevant to the context, the assignment notation introduced earlier may be extended to indicate the decision levelat which the assignment occurred. Thus, x = v @d would beread as “x becomes equal to v at decision level d.”The average complexity of the above search processdepends on how decisions, deductions, and backtracking aremade. It also depends on the formula itself. The implicationsthat can derived from a given partial assignment depend onthe set of available clauses. In general, a formula consisting ofmore clauses will enable more implications to be derived andwill reduce the number of backtracks due to conflicts.

Thelimiting case is the complete formula that contains all primeimplicates. For such a formula no conflicts can arise since alllogical implications for a partial assignment can be derived.This, however, may not lead to shorter execution times sincethe size of such a formula may be exponential.2.3 Function SatisfiabilityGiven an initial formula ϕ many search systemsattempt to augment it with additional implicates to increasethe deductive power during the search process.

This is usually referred to as “learning” [12] and can be performedeither as a preprocessing step (static learning) or during thesearch (dynamic learning). Even though learning as definedin [10, 12] only yields implicates of size 2 (i.e. non-localimplications), the concept can be readily extended to implicates of arbitrary size.Our approach can be classified as a dynamic learningsearch mechanism based on diagnosing the causes of conflicts. It considers the occurrence of a conflict, which isunavoidable for an unsatisfiable instance unless the formulais complete, as an opportunity to “learn from the mistakethat led to the conflict” and introduces additional implicatesto the clause database only when it stumbles.

Conflict diagnosis produces three distinct pieces of information that canhelp speed up the search:1. New implicates that did not exist in the clause databaseand that can be identified with the occurrence of theconflict. These clauses may be added to the clause databaseto avert future occurrence of the same conflict andrepresent a form of conflict-based equivalence (CBE).2. An indication of whether the conflict was ultimately dueto the most recent decision assignment or to an earlierdecision assignment.a. If that assignment was the most recent (i.e. at thecurrent decision level), the opposite assignment (if ithas not been tried) is immediately implied as anecessary consequence of the conflict; we refer to thisas a failure-driven assertion (FDA).b.

If the conflict resulted from an earlier decisionassignment (at a lower decision level), the search canbacktrack to the corresponding level in the decisiontree since the subtree rooted at that level corresponds toassignments that will yield the same conflict. Theability to identify a backtracking level that is muchearlier than the current decision level is a form of nonchronological backtracking that we refer to as conflictdirected backtracking (CDB), and has the potential ofsignificantly reducing the amount of search.These conflict diagnosis techniques are discussed further inSection 3.2.4 Structure of the Search ProcessThe basic mechanism for deriving implications from agiven clause database is Boolean constraint propagation(BCP) [5, 18]. Consider a formula ϕ containing the clauseω = ( x + ¬y ) and assume y = 1 .

For any satisfyingassignment to ϕ , ω requires that x be equal to 1, and we saythat y = 1 implies x = 1 due to ω . In general, given aunit clause ( l 1 + … + l k ) of ϕ with free literal l j , consistency requires l j = 1 since this represents the only possibility for the clause to be satisfied. If l j = x , then theassignment x = 1 is required; if l j = ¬x then x = 0 isrequired. Such assignments are referred to as logical implications (implications, for short) and correspond to the application of the unit clause rule proposed by M. Davis and H.Putnam [3].

BCP refers to the iterated application of thisrule to a clause database until the set of unit clauses becomesempty or one or more clauses become unsatisfied.Let the assignment of a variable x be implied due to aclause ω = ( l 1 + … + l k ) . The antecedent assignment of x,denoted as A ( x ) , is defined as the set of assignments to variables other than x with literals in ω . Intuitively, A ( x ) designates those variable assignments that are directly responsiblefor implying the assignment of x due to ω . For example, theantecedent assignments of x, y and z due to the clauseω = ( x + y + ¬z )are,respectively,A ( x ) = { y = 0, z = 1 } , A ( y ) = { x = 0, z = 1 } , andA ( z ) = { x = 0, y = 0 } . Note that the antecedent assignment of a decision variable is empty.The sequence of implications generated by BCP is captured by a directed implication graph I defined as follows(see Figure 1):1.

Each vertex in I corresponds to a variable assignmentx = ν ( x) .2. The predecessors of vertex x = ν ( x ) in I are theantecedent assignments A ( x ) corresponding to the unitclause ω that led to the implication of x. The directededges from the vertices in A ( x ) to vertex x = ν ( x ) areall labeled with ω . Vertices that have no predecessorscorrespond to decision assignments.3. Special conflict vertices are added to I to indicate theoccurrence of conflicts. The predecessors of a conflictvertex κ correspond to variable assignments that force aclause ω to become unsatisfied and are viewed as theantecedent assignment A ( κ ) .

The directed edges fromthe vertices in A ( κ ) to κ are all labeled with ω .The decision level of an implied variable x is related to thoseof its antecedent variables according to:δ(x) = max { δ(y) ( y, ν ( y ) ) ∈ A(x) }(1)2.5 Search Algorithm TemplateThe general structure of the GRASP search algorithm isCurrent Assignment:{ x 9 = 0 @1, x 10 = 0 @3, x 11 = 0 @3, x 12 = 1 @2, x 13 = 1 @2 }Decision Assignment:{ x 1 = 1 @6 }ω 1 = ( ¬x 1 + x 2 )ω 2 = ( ¬x 1 + x 3 + x 9 )x 10 = 0 @3ω 3 = ( ¬x 2 + ¬x 3 + x 4 )x 2 = 1 @6ω 4 = ( ¬x 4 + x 5 + x 10 )ω1ω 5 = ( ¬x 4 + x 6 + x 11 )x 1 = 1 @6ω 6 = ( ¬x 5 + ¬x 6 )ω 7 = ( x 1 + x 7 + ¬x 12 )ω8 = ( x1 + x8)ω2ω2x 9 = 0 @1ω3ω3x 3 = 1 @6ω4ω4x 5 = 1 @6ω6x 4 = 1 @6ω5ω5κω6x 6 = 1 @6x 11 = 0 @3ω 9 = ( ¬x 7 + ¬x 8 + ¬x 13 )Clause DatabaseImplication GraphFigure 1: Clause database and partial implication graphshown in Figure 2. We assume that an initial clause databaseϕ and an initial assignment A, at decision level 0, are given.This initial assignment, which may be empty, may be viewedas an additional problem constraint and causes the search tobe restricted to a subcube of the n-dimensional Booleanspace.

As the search proceeds, both ϕ and A are modified.The recursive search procedure consists of four major operations:1. Decide(), which chooses a decision assignment at eachstage of the search process. Decision procedures arecommonly based on heuristic knowledge. For the resultsgiven in Section 4, the following greedy heuristic is used:At each node in the decision tree evaluate the numberof clauses directly satisfied by each assignment to eachvariable. Choose the variable and the assignment thatdirectly satisfies the largest number of clauses.Other decision making procedures have been incorporatedin GRASP, as described in [15].2. Deduce(), which implements BCP and (implicitly)maintains the resulting implication graph. (See [15] forthe details of Deduce().)3.

Diagnose(), which identifies the causes of conflictsand can augment the clause database with additionalimplicates. Realization of different conflict diagnosisprocedures is the subject of Section 3.4. Erase(), which deletes the assignments at the currentdecision level.We refer to Decide(), Deduce() and Diagnose() as the Decision, Deduction and Diagnosis engines,// Global variables:Clause database ϕ//Variable assignment A// Return value:FAILURE or SUCCESS// Auxiliary variables: Backtracking level β//GRASP(){return (Search (0, β ) != SUCCESS) ?FAILURE : SUCCESS;}// Input argument:Current decision level// Output argument:Backtracking level β// Return value:CONFLICT or SUCCESS//Search (d, & β ){if (Decide (d) == SUCCESS)return SUCCESS;while (TRUE) {if (Deduce (d) != CONFLICT) {if (Search (d + 1, β ) == SUCCESS)return SUCCESS;else if ( β != d) {Erase(); return CONFLICT;}}if (Diagnose (d, β ) == CONFLICT) {Ease(); return CONFLICT;}Erase();}}dDiagnose (d, & β ){ω C ( κ ) = Conflict_Induced_Clause(); // From (4)Update_Clause_Database ( ω C ( κ ) );β = Compute_Max_Level();// From (7)if ( β != d) {add new conflict vertex κ to I;record A ( κ ) ;return CONFLICT;}return SUCCESS;}Figure 2: Description of GRASPrespectively.

Different realizations of these engines lead todifferent SAT algorithms. For example, the Davis-Putnamprocedure can be emulated with the above algorithm bydefining a decision engine, requiring the deduction engine toimplement BCP and the pure literal rule, and organizing thediagnosis engine to implement chronological backtracking.3 Conflict Analysis ProceduresWhen a conflict arises during BCP, the structure of theimplication sequence converging on a conflict vertex κ isanalyzed to determine those (unsatisfying) variable assignments that are directly responsible for the conflict. The conjunction of these conflicting assignments is an implicant thatrepresents a sufficient condition for the conflict to arise.Negation of this implicant, therefore, yields an implicate ofthe Boolean function f (whose satisfiability we seek) thatdoes not exist in the clause database ϕ .