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

However, they are also quite expensive compared with VSIDS.Random SAT problems are usually much harder than structured problems of the samesize. Current solvers can only attack hard random 3-SAT problems with severalhundred variables. Therefore, the instances regarded as hard for random SAT isgenerally much smaller in size than the instances considered hard for structuredproblems.

Thus, while it may be practical to apply these expensive heuristics to thesmaller random problems, their overhead tends to be unacceptable for the larger wellstructured problems.3.2 The Deduction algorithmFunction deduce() serves the purpose of pruning the search space by “look ahead”.When a branch variable is assigned a value, the entire clause database is simplified.Function deduce() needs to determine the consequences of the last decision tomake the instance satisfiable, and may return three status values. If the instance issatisfied under the current variable assignment, it will return SATISFIABLE; if theinstance contains a conflicting clause, it will return CONFLICT; otherwise, it willreturn UNKNOWN and the solver will continue to branch. There are variousmechanisms with different deduction power and run time costs for the deducefunction.

The correctness of the algorithm will not be affected as long as thededuction rules incorporated are valid (e.g. it will not return SATISFIABLE whenthe instance contains a conflicting clause under the assignment). However, differentdeduction rules, or even different implementations of the same rule, can significantlyaffect the efficiency of the solver.Over the years several different deduction mechanisms have been proposed.However, it seems that the unit clause rule [6] is the most efficient one because itrequires relatively little computational power but can prune large search spaces.

Theunit clause rule states that for a certain clause, if all but one of its literals has beenassigned the value 0, then the remaining (unassigned) literal must be assigned thevalue 1 for this clause to be satisfied, which is essential for the formula to be satisfied.Such clauses are called unit clauses, and the unassigned literal in a unit clause iscalled a unit literal. The process of assigning the value 1 to all unit literals is calledunit propagation, or sometimes called Boolean Constraint Propagation (BCP).Almost all modern SAT solvers incorporate this rule in the deduction process. In aSAT solver, BCP usually takes the most significant part of the run time.

Therefore, itsefficiency is directly related to the implementation of the BCP engine.3.2.1 BCP MechanismsIn a SAT solver, the BCP engine’s function is to detect unit clauses and conflictingclauses after a variable assignment. The BCP engine is the most important part of aSAT solver and usually dictates the data structure and organization of the solver.A simple and intuitive implementation for BCP is to keep counters for each clause.This scheme is attributed to Crawford and Auton [13] by [30]. Similar schemes aresubsequently employed in many solvers such as GRASP [25], rel_sat [18], satz [22]etc. For example, in GRASP [25], each clause keeps two counters, one for the numberof value 1 literals in the clause and the other for the number of value 0 literals in theclause.

Each variable has two lists that contain all the clauses where that variableappears as a positive and negative literal, respectively. When a variable is assigned avalue, all the clauses that contain this literal will have their counters updated. If aclause’s value 0 count becomes equal to the total number of literals in the clause, thenit is a conflicting clause.

If a clause’s value 0 count is one less than the total numberof literals in the clause and the value 1 count is 0, then the clause is a unit clause. Acounter-based BCP engine is easy to understand and implement, but this scheme isnot the most efficient one. If the instance has m clauses and n variables, and onaverage each clause has l literals, then whenever a variable gets assigned, on theaverage l m / n counters need to be updated. On backtracking from a conflict, we needto undo the counter assignments for the variables unassigned during the backtracking.Each undo for a variable assignment will also update l m / n counters on average.Modern solvers usually incorporate learning mechanisms in the search process(described in the next sections), and learned clauses often have many literals.Therefore, the average clause length l is quite large, thus making a counter-based BCPengine relatively slow.In [30], the authors of the solver SATO proposed the use of another mechanism forBCP using head/tail lists.

In this mechanism, each clause has two pointers associatedwith it, called the head and tail pointer respectively. A clause stores all its literals inan array. Initially, the head pointer points to the first literal of the clause (i.e.beginning of the array), and the tail pointer points to the last literal of the clause (i.e.end of the array). Each variable keeps four linked lists that contain pointer to clauses.The linked lists for the variable v are clause_of_pos_head(v),clause_of_neg_head(v),clause_of_pos_tail(v)andclause_of_neg_tail(v). Each of these lists contains the pointers to the clausesthat have their head/tail literal in positive/negative phases of variable v.

If v isassignedwiththevalue1,clause_of_pos_head(v)andclause_of_pos_tail(v) will be ignored. For each clause C inclause_of_neg_head(v), the solver will search for a literal that does notevaluate to 1 from the position of the head literal of C to the position of the tail literalof C. Notice the head literal of C must be a literal corresponding to v in negativephase. During the search process, four cases may occur:1) If during the search we first encounter a literal that evaluates to 1, then theclause is satisfied, we need to do nothing.2) If during the search we first encounter a literal l that is free and l is not thetail literal, then we remove C from clause_of_neg_head(v) and add Cto head list of the variable corresponding to l.

We refer to this operation asmoving the head literal, because in essence the head pointer is moved fromits original position to the position of l.3) If all literals in between these two pointers are assigned value 0, but the tailliteral is unassigned, then the clause is a unit clause, and the tail literal is theunit literal for this clause.4) If all literals in between these two pointers and the tail literal are assignedvalue 0, then the clause is a conflicting clause.Similar actions are performed for clause_of_neg_tail(v), only the search isin the reverse direction (i.e.

from tail to head).Head/tail list method is faster than the counter-based scheme because when thevariable is assigned value 1, the clauses that contain the positive literals of this clausewill not be visited at all and vice-versa. As each clause has only two pointers,whenever a variable is assigned a value, the status of only m/n clauses needs to beupdated on the average, if we assume head/tail literals are distributed evenly in eitherphase. Even though the work needed to be done for each update is different from thecounter-based mechanism, in general head/tail mechanism is still much faster.For both the counter-based algorithm and the head/tail list-based algorithm,undoing a variable’s assignment during backtrack has about the same computationalcomplexity as assigning the variable. In [20], the authors of the solver Chaff proposedanother BCP algorithm called 2-literal watching.

Similar to the head/tail listalgorithm, 2-literal watching also has two special literals for each clause calledwatched literals. Each variable has two lists containing pointers to all the watchedliterals corresponding to it in either phase. We denote the lists for variable v aspos_watched(v) and neg_watched(v).

In contrast to the head/tail listscheme in SATO, there is no imposed order on the two pointers within a clause, andeach of the pointers can move in either direction. Initially the watched literals are free.When a variable v is assigned value 1, for each literal p pointed to by a pointer in thelist of neg_watched(v) (notice p must be a literal of v with negative phase), thesolver will search for a literal l in the clause containing p that is not set to 0.

There arefour cases that may occur during the search:1) If there exists such a literal l and it is not the other watched literal, then weremove pointer to p from neg_watched(v), and add pointer to l to thewatched list of the variable corresponding to l. We refer to this operation asmoving the watched literal, because in essence one of the watched pointers ismoved from its original position to the position of l.2) If the only such l is the other watched literal and it is free, then the clause is aunit clause, with the other watched literal being the unit literal.3) If the only such l is the other watched literal and it evaluates to 1, then weneed to do nothing.4) If all literals in the clause is assigned value 0 and no such l exists, then theclause is a conflicting clause.2-literal watching has the same advantage as the head/tail list mechanism comparedwith the literal counting scheme.

Moreover, unlike the other two mechanisms,undoing a variable assignment during backtrack in the 2-literal watching scheme takesconstant time. This is because the two watched literals are the last to be assigned to 0,so as a result, any backtracking will make sure that the literals being watched areeither unassigned, or assigned to one. Thus, no action is required to update thepointers for the literals being watched. Therefore, it is significantly faster than bothcounter-based and head/tail mechanisms for BCP. In Fig. 3, we show a comparison of2-literal watching and head/tail list mechanism.In [31], the authors examined the mechanisms mentioned above and introducedsome new deduction data structures and mechanisms.