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

GRASP—A New Search Algorithm for SatisfiabilityJoão P. Marques SilvaCadence European LaboratoriesIST/INESC1000 Lisboa, PortugalAbstractThis paper introduces GRASP (Generic seaRch Algorithmfor the Satisfiability Problem), an integrated algorithmic framework for SAT that unifies several previously proposed searchpruning techniques and facilitates identification of additionalones. GRASP is premised on the inevitability of conflicts duringsearch and its most distinguishing feature is the augmentation ofbasic backtracking search with a powerful conflict analysis procedure.

Analyzing conflicts to determine their causes enablesGRASP to backtrack non-chronologically to earlier levels in thesearch tree, potentially pruning large portions of the search space.In addition, by “recording” the causes of conflicts, GRASP canrecognize and preempt the occurrence of similar conflicts later onin the search. Finally, straightforward bookkeeping of the causality chains leading up to conflicts allows GRASP to identifyassignments that are necessary for a solution to be found.

Experimental results obtained from a large number of benchmarks,including many from the field of test pattern generation, indicate that application of the proposed conflict analysis techniquesto SAT algorithms can be extremely effective for a large numberof representative classes of SAT instances.1 IntroductionThe Boolean satisfiability problem (SAT) appears inmany contexts in the field of computer-aided design of integrated circuits including automatic test pattern generation(ATPG), timing analysis, delay fault testing, and logic verification, to name just a few. Though well-researched andwidely investigated, it remains the focus of continuing interest because efficient techniques for its solution can have greatimpact.

SAT belongs to the class of NP-complete problemswhose algorithmic solutions are currently believed to haveexponential worst case complexity [6]. Over the years, manyalgorithmic solutions have been proposed for SAT, the mostwell known being the different variations of the Davis-Putnam procedure [3]. The best known version of this procedure is based on a backtracking search algorithm that, ateach node in the search tree, elects an assignment and prunessubsequent search by iteratively applying the unit clause andthe pure literal rules [18]. Iterated application of the unitclause rule is commonly referred to as Boolean ConstraintPropagation (BCP) or as derivation of implications in the electronic CAD literature [1].Most of the recently proposed improvements to thebasic Davis-Putnam procedure [5, 10, 17, 18] can be distinguished based on their decision making heuristics or theirThi dKarem A.

SakallahDepartment of EECSUniversity of MichiganAnn Arbor, Michigan 48109-2122use of preprocessing or relaxation techniques. Common toall these approaches, however, is the chronological nature ofbacktracking. Nevertheless, non-chronological backtrackingtechniques have been extensively studied and applied to different areas of Artificial Intelligence, particularly TruthMaintenance Systems (TMS), Constraint Satisfaction Problems (CSP) and Automated Deduction, in some cases withvery promising experimental results. (Bibliographic references to the work in these areas can be found in [15].)Interest in the direct application of SAT algorithms toelectronic design automation (EDA) problems has been onthe rise recently [2, 10, 17].

In addition, improvements tothe traditional structural (path sensitization) algorithms forsome EDA problems, such as ATPG, include search-pruningtechniques that are also applicable to SAT algorithms in general [8, 9, 13]. The main purpose of this paper is to introduce a procedure for the analysis of conflicts in searchalgorithms for SAT. Even though the conflict analysis procedure is described in the context of SAT, it can be naturallyextended to EDA-specific algorithms, thus complementingother well-known search-pruning techniques [2, 9].The proposed conflict analysis procedure has beenincorporated in GRASP (Generic seaRch Algorithm for theSatisfiability Problem), an integrated algorithmic frameworkfor SAT. Several features distinguish the conflict analysis procedure in GRASP from others used in TMSs and CSPs.First, conflict analysis in GRASP is tightly coupled with BCPand the causes of conflicts need not necessarily correspond todecision assignments.

Second, clauses can be added to theoriginal set of clauses, and the number and size of addedclauses is user-controlled. This is in explicit contrast withnogood recording techniques developed for TMSs and CSPs.Third, GRASP employs techniques to prune the search byanalyzing the implication structure generated by BCP.Exploiting the “anatomy” of conflicts in this manner has noequivalent in other areas.Some of the proposed techniques have also been appliedin several structural ATPG algorithms [8, 16], among others.The GRASP framework, however, permits a unified representation of all known search-pruning methods and potentiates the identification of additional ones.

The basic SATalgorithm in GRASP is also customizable to take advantageof application-specific characteristics to achieve additionalefficiencies [13]. Finally, the framework is organized to alloweasy adaptation of other algorithmic techniques, such asd ihFM k404those in [2, 9], whose operation is orthogonal to thosedescribed here.The remainder of this paper is organized in four sections. In Section 2, we introduce the basics of backtrackingsearch, particularly our implementation of BCP, and describethe overall architecture of GRASP.

This is followed, in Section 3, by a detailed discussion of the procedures for conflictanalysis and how they are implemented. Extensive experimental results on a wide range of benchmarks, includingmany from the field of ATPG, are presented and analyzed inSection 4.

In particular, GRASP is shown to outperform tworecent state-of-the-art SAT algorithms [5, 17] on most, butnot all, benchmarks. The paper concludes in Section 5 withsome suggestions for further research.2 Definitions2.1 Basic Definitions and NotationA conjunctive normal form (CNF) formula ϕ on nbinary variables x 1, …, x n is the conjunction (AND) of mclauses ω 1, …, ω m each of which is the disjunction (OR) ofone or more literals, where a literal is the occurrence of avariable or its complement. A formula ϕ denotes a uniquen-variable Boolean function f ( x 1, …, x n ) and each of itsclauses corresponds to an implicate of f.

Clearly, a function fcan be represented by many equivalent CNF formulas. A formula is complete if it consists of the entire set of primeimplicates for the corresponding function. In general, a complete formula will have an exponential number of clauses.We will refer to a CNF formula as a clause database and use“formula,” “CNF formula,” and “clause database” interchangeably. The satisfiability problem (SAT) is concernedwith finding an assignment to the arguments off ( x 1, …, x n ) that makes the function equal to 1 or provingthat the function is equal to the constant 0.A backtracking search algorithm for SAT is implemented by a search process that implicitly traverses the spacenof 2 possible binary assignments to the problem variables.During the search, a variable whose binary value has alreadybeen determined is considered to be assigned; otherwise it isunassigned with an implicit value of X ≡ { 0, 1 } .

A truthassignment for a formula ϕ is a set of assigned variables andtheir corresponding binary values. It will be convenient torepresent such assignments as sets of variable/value pairs; forexample A = { ( x 1, 0 ) , ( x 7, 1 ) , ( x 13, 0 ) } . Alternatively,assignmentscanbedenotedasA = { x 1 = 0, x 7 = 1, x 13 = 0 } . Sometimes it is convenient to indicate that a variable x is assigned without specifying its actual value.

In such cases, we will use the notationν ( x ) to denote the binary value assigned to x. An assignment A is complete if A = n ; otherwise it is partial. Evaluating a formula ϕ for a given truth assignment A yields threepossible outcomes: ϕ A = 1 and we say that ϕ is satisfiedand refer to A as a satisfying assignment; ϕ A = 0 in whichcase ϕ is unsatisfied and A is referred to as an unsatisfyingassignment; and ϕ A = X indicating that the value of ϕcannot be resolved by the assignment.

This last case can onlyhappen when A is a partial assignment. An assignment partitions the clauses of ϕ into three sets: satisfied clauses (evaluating to 1); unsatisfied clauses (evaluating to 0); andunresolved clauses (evaluating to X). The unassigned literalsof a clause are referred to as its free literals. A clause is said tobe unit if the number of its free literals is one.2.2 Formula SatisfiabilityFormula satisfiability is concerned with determining if agiven formula ϕ is satisfiable and with identifying a satisfying assignment for it. Starting from an empty truth assignment, a backtrack search algorithm traverses the space oftruth assignments implicitly and organizes the search for asatisfying assignment by maintaining a decision tree. Eachnode in the decision tree specifies an elective assignment toan unassigned variable; such assignments are referred to asdecision assignments.

A decision level is associated with eachdecision assignment to denote its depth in the decision tree;the first decision assignment at the root of the tree is at decision level 1. The search process iterates through the steps of:1. Extending the current assignment by making a decisionassignment to an unassigned variable. This decision processis the basic mechanism for exploring new regions of thesearch space. The search terminates successfully if allclauses become satisfied; it terminates unsuccessfully ifsome clauses remain unsatisfied and all possibleassignments have been exhausted.2.