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

The Quest for Efficient Boolean Satisfiability SolversLintao Zhang, Sharad MalikDepartment of Electrical Engineering, Princeton University, Princeton, NJ 08544{lintaoz,sharad}@ee.Princeton.eduAbstract. The classical NP-complete problem of Boolean Satisfiability (SAT)has seen much interest in not just the theoretical computer science community,but also in areas where practical solutions to this problem enable significantpractical applications. Since the first development of the basic search basedalgorithm proposed by Davis, Putnam, Logemann and Loveland (DPLL) aboutforty years ago, this area has seen active research effort with many interestingcontributions that have culminated in state-of-the-art SAT solvers today beingable to handle problem instances with thousands, and in same cases evenmillions, of variables.

In this paper we examine some of the main ideas alongthis passage that have led to our current capabilities. Given the depth of theliterature in this field, it is impossible to do this in any comprehensive way;rather we focus on techniques with consistent demonstrated efficiency inavailable solvers. For the most part, we focus on techniques within the basicDPLL search framework, but also briefly describe other approaches and look atsome possible future research directions.1. IntroductionGiven a propositional formula, determining whether there exists a variable assignmentsuch that the formula evaluates to true is called the Boolean Satisfiability Problem,commonly abbreviated as SAT.

SAT has seen much theoretical interest as thecanonical NP-complete problem [1]. Given its NP-Completeness, it is very unlikelythat there exists any polynomial algorithm for SAT. However, NP-Completeness doesnot exclude the possibility of finding algorithms that are efficient enough for solvingmany interesting SAT instances.

These instances arise from many diverse areas many practical problems in AI planning [2], circuit testing [3], software verification[4] can be formulated as SAT instances. This has motivated the research in practicallyefficient SAT solvers.This research has resulted in the development of several SAT algorithms that haveseen practical success. These algorithms are based on various principles such asresolution [5], search [6], local search and random walk [7], Binary DecisionDiagrams [8], Stälmarck’s algorithm [9], and others.

Gu et al. [10] provide anexcellent review of many of the algorithms developed thus far. Some of thesealgorithms are complete, while others are stochastic methods. For a given SATinstance, complete SAT solvers can either find a solution (i.e. a satisfying variableassignment) or prove that no solution exists. Stochastic methods, on the other hand,cannot prove the instance to be unsatisfiable even though they may be able to find asolution for certain kinds of satisfiable instances quickly. Stochastic methods haveapplications in domains such as AI planning [2] and FPGA routing [11], whereinstances are likely to be satisfiable and proving unsatisfiability is not required.However, for many other domains (especially verification problems e.g.

[4, 12]), theprimary task is to prove unsatisfiability of the instances. For these, complete SATsolvers are a requirement.In recent years search-based algorithms based on the well-known DavisLogemann-Loveland algorithm [6] (sometimes called the DPLL algorithm forhistorical reasons) are emerging as some of the most efficient methods for completeSAT solvers.

Researchers have been working on DPLL-based SAT solvers for aboutforty years. In the last ten years we have seen significant growth and success in SATsolver research based on the DPLL framework. Earlier SAT solvers based on DPLLinclude Tableau (NTAB) [13], POSIT [14], 2cl [15] and CSAT [16] among others.They are still appearing occasionally in the literature for performance comparisonreasons. In the mid 1990’s, Silva and Sakallah [17], and Bayardo and Schrag [18]proposed to augment the original DPLL algorithm with non-chronologicalbacktracking and conflict-driven learning. These techniques greatly improved theefficiency of the DPLL algorithm for structured (in contrast to randomly generated)SAT instances. Many practical applications emerged (e.g.

[4, 11, 12]), which pushedthese solvers to their limits and provided strong motivation for finding even moreefficient algorithms. This led to a new generation of solvers such as SATO [19],Chaff [20], and BerkMin [21] which pay a lot of attention to optimizing variousaspects of the DPLL algorithm. The results are some very efficient SAT solvers thatcan often solve SAT instances generated from industrial applications with tens ofthousands or even millions of variables.

On another front, solvers such as satz [22]and cnfs [23] keep pushing the ability to tackle hard random 3-SAT instances. Thesesolvers, though very efficient on random instances, are typically not competitive onstructured instances generated from real applications.A DPLL-based SAT solver is a relatively small piece of software.

Many of thesolvers mentioned above have only a few thousand lines of code (these solvers aremostly written in C or C++, for efficiency reasons). However, the algorithms involvedare quite complex and a lot of attention is focused on various aspects of the solversuch as coding, data structures, choosing algorithms and heuristics, and parametertuning. Even though the overall framework is well understood and people have beenworking on it for years, it may appear that we have reached a plateau in terms of whatcan be achieved in practice – however we feel that many open questions still exist andpresent many research opportunities.In this paper we chart the journey from the original basic DPLL frameworkthrough the introduction of efficient techniques within this framework culminating atcurrent state-of-the-art solvers.

Given the depth of literature in this field, it isimpossible to do this in any comprehensive way; rather, we focus on techniques withconsistent demonstrated efficiency in available solvers. While for the most part, wefocus on techniques within the basic DPLL search framework, we will also brieflydescribe other approaches and look at some possible future research directions.2. The Basic DPLL FrameworkEven though there were many developments pre-dating them, the original algorithmfor solving SAT is often attributed to Davis and Putnam for proposing a resolutionbased algorithm for Boolean SAT in 1960 [5].

The original algorithm proposedsuffers from the problem of memory explosion. Therefore, Davis, Logemann andLoveland [6] proposed a modified version that used search instead of resolution tolimit the memory required for the solver. This algorithm is often referred to as theDPLL algorithm. It can be argued that intrinsically these two algorithms are tightlyrelated because search (i.e.

branching on variables) can be regarded as a special typeof resolution. However, in the future discussion we will regard search-basedalgorithms as their own class and distinguish them from explicit resolutionalgorithms.For the efficiency of the solver, the propositional formula instance is usuallypresented in a Product of Sum form, usually called a Conjunctive Normal Form(CNF). It is not a limitation to require the instance to be presented in CNF. Thereexist polynomial algorithms (e.g. [24]) to transform any propositional formula into aCNF formula that has the same satisfiability as the original one.

In the discussionsthat follow, we will assume that the problem is presented in CNF. A SAT instance inCNF is a logical and of one or more clauses, where each clause is a logical or of oneor more literals. A literal is either the positive or the negative occurrence of avariable.A propositional formula in CNF has some nice properties that can help prune thesearch space and speed up the search process.