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

Note that one of theinput clauses to resolve() is a conflicting clause (i.e. all literals evaluate to 0),and the other is the antecedent of the variable var (i.e. all but one literal evaluate to 0).Therefore, the resulting clause will have all literals evaluating to 0, i.e. it will still bea conflicting clause.analyze_conflict(){cl = find_conflicting_clause();while (!stop_criterion_met(cl)) {lit = choose_literal(cl);var = variable_of_literal( lit );ante = antecedent( var );cl = resolve(cl, ante, var);}add_clause_to_database(cl);back_dl = clause_asserting_level(cl);return back_dl;}Fig.

4. Generating Learned Clause by ResolutionThe clause generation process will stop when some predefined stop criterion ismet. In modern SAT solvers, the stop criterion is that the resulting clause be anasserting clause. A clause is asserting if the clause contains all value 0 literals; andamong them only one is assigned at current decision level.

After backtracking, thisclause will become a unit clause and force the literal to assume another value (i.e.evaluate to 1), thus bringing the search to a new space. We will call the decision levelof the literal with the second highest decision level in an asserting clause theasserting level of that clause. The asserting clause is a unit clause at its assertingdecision level.In addition to the above asserting clause requirement, different learning schemesmay have some additional requirements. Different learning schemes differ in theirstop criterion and the way to choose literals. Notice the stop criterion can always bemet if function choose_literal() always chooses the literal that is assigned lastin the clause.

If that is the case, the resolution process will always resolve theconflicting clause with the antecedent of the variable that is assigned last in theclause. After a certain number of calls to resolve(), there will always be a timewhen the variable that is assigned last in the clause is the decision variable of thecurrent decision level. At this time, the resulting clause is guaranteed to be anasserting clause. The SAT solver rel_sat [18] actually uses this stop criterion, i.e.

itrequires that the variable that has the highest decision level in the resulting clause be adecision variable. The literal corresponding to this variable will be a unit literal afterbacktracking, resulting in essentially flipping the decision variable.In [39], the authors discussed a scheme called the FirstUIP scheme. The FirstUIPscheme is quite similar to the rel_sat scheme but the stop criterion is that it will stopwhen the first asserting clause is encountered. In [17], the authors of GRASP use asimilar scheme as the FirstUIP, but add extra clauses other than the asserting clauseinto the database. If function choose_literal() does not choose literals inreversed chronological order, then extra mechanisms are needed to guarantee that thestop criterion can be met.

Some of the schemes discussed in [39] may need functionchoose_literal() to choose literals that are not in the current decision level.Different learning schemes affect the SAT solver’s efficiency greatly. Experimentsin [39] show that among all the discussed schemes, FirstUIP seems to be the best onthe benchmarks tested. Therefore, recent SAT solvers (e.g. Chaff [20]) often employthis scheme as the default conflict-driven learning scheme.Conflict-driven learning will add clauses to the clause database during the searchprocess.

Because added clauses are redundant, deleting some or all of them will notaffect the correctness of the algorithm. In fact, the added clauses will slow down thededuction engine, and keeping all added clauses may need more memory for storagethan the available memory. Therefore, it is often required for the solver to delete someof the less useful learned clauses and learned clauses that have too many literals.There are many heuristics to measure the usefulness of a learned clause.

For example,rel_sat [18] proposes to use relevance to measure a clause’s usefulness, whileBerkMin [21] use the number of conflicts that involve this clause in the history tomeasure a clause’s usefulness. These measures seem to work reasonably well.3.4 Data Structure for Storing Clause DatabaseCurrent state-of-the-art SAT solvers often need to solve instances that are quite largein size. Some instances generated from circuit verification problems may containmillions of variables and several million clauses. Moreover, during the SAT solvingprocess, learned clauses are generated for each conflict encountered and may furtherincrease the dataset size. Therefore, efficient data structures for storing the clauses areneeded.Most commonly, clauses are stored in a linear way (sometimes called sparsematrix representation), i.e.

each clause occupies its own space and no overlap existsbetween clauses. Therefore, the dataset size is linear in the number of literals in theclause database. Early SAT solvers (e.g. GRASP [25], rel_sat [18]) use pointer heavydata structures such as linked lists and array of pointers pointing to structures to storethe clause database. Pointer heavy data structures, though convenient formanipulating the clause database (i.e. adding/deleting clauses), are not memoryefficient and usually cause a lot of cache misses during the solving process because oflack of access locality. Chaff [20] uses a data structure that stores clause data in alarge array. Because arrays are not as flexible as linked lists, some additional garbagecollection code is needed when clauses are deleted.

The advantage of the array datastructure is that it is very efficient in memory utilization. Moreover, because an arrayoccupies contiguous memory space, access locality is increased. Experiments showsthat the array data structure has a big advantage compared with linked lists in terms ofcache misses that translates to substantial speed-up in the solving process.Researchers have proposed schemes other than sparse matrix representation forstoring clauses. In [41], the authors of the solver SATO proposed the use of a datastructure called trie to store clauses. A trie is a ternary tree.

Each internal node in thetrie structure is a variable index, and its three children edges are labeled Pos, Neg, andDC, for positive, negative, and don't care, respectively. A leaf node in a trie is eitherTrue or False. Each path from root of the trie to a True leaf represents a clause. A trieis said to be ordered if for every internal node V, Parent(V) has a smaller variableindex than the index of variable V. The ordered trie structure has the nice property ofbeing able to detect duplicate and tail subsumed clauses of a database quickly.

Aclause is said to be tail subsumed by another clause if its first portion of the literals (aprefix) is also a clause in the clause database. For example, (a + b + c) is tailsubsumed by (a + b). Fig. 5 shows a simple clause database represented in a triestructure.V1+DC-V2+TFV2DC+FV3+FDCTDCV3+T-FDCFFTFFig.

5. A trie data structure representing clauses (V1+V2) (V1’+V3) (V1’+V3’)(V2’+V3’)An ordered trie has obvious similarities with Binary Decision Diagrams. This hasnaturally led to the exploration of decision diagram style set representations. In [42]and [43], the authors have experimented with using Zero-suppressed Binary DecisionDiagrams (ZBDDs) [44] to represent the clause database. A ZBDD representation ofthe clause database can detect not only tail subsumption but also head subsumption.Both authors report significant compression of the clause database for certain classesof problems.Based on current experimental data it does not seem that the data compressionadvantages of the trie and ZBDD data structures are sufficient to justify the additionalmaintenance overhead of these data structures compared to the sparse matrixrepresentation.3.5 Preprocess, Restart and other techniquesPreprocess aims at simplifying the instances before the regular solving begins in orderto speed up the solving process.

Usually the preprocessor of a SAT solver is just anextra deduction mechanism applied at the beginning of the search. Because thepreprocessor will only be applied once in the solving process, it is usually possible toincorporate some deduction rules that are too expensive to be applied at every node ofthe search tree. The preprocessor can be applied on-line (within the solver) or off-line(it produces an equivalent instance to be fed to a solver). In [45], the authors give anoverview of some of the existing preprocessing techniques and find that the result ofapplying simplification techniques before the regular search is actually mixed.The time required for solving similar SAT instances often varies greatly forcomplete algorithms. Two problems that are exactly the same except for the variableorder may require totally different times to solve by a certain SAT solver (e.g.

one canbe solved in seconds while the other takes days). In [46], the authors proposed to userandom restart to cope with this phenomenon. Random restart randomly throwsaway the already searched space and starts from scratch. This technique is applied inmodern SAT solvers such as Chaff [20] and BerkMin [21]. In these cases, whenrestart is invoked, even though the current search tree is abandoned, because thesolver still keeps some of the learned clauses, the previous search effort is not totallylost.

Experiments show that random restarts can increase the robustness of certainSAT solvers.Researchers have been extending the randomization idea of random restart to otheraspects of the SAT solving process as well. For example, portfolio design [47] aims atusing different solving strategies during one solving process in order to make thesolver robust.

Some researchers [48] also propose to randomize backtracking. All inall, it seems that randomization is quite important because of the heavy tail [49]nature of SAT solving process.4. Other techniques used in SAT solversIn this section, we briefly discuss some of the other techniques used to solve SATproblems besides the basic DPLL search.The original Davis Putnam algorithm [5] was based on resolution. A well-knownproblem of the resolution-based algorithm is that the solver tends to blow up inmemory. Because of this, resolution based algorithm is seldom employed in modernSAT solvers.