Undergraduate Thesis (roger Willis)

Satisability Solving

Roger M. Willis

A Dissertation presented for the degree of Bachelor of Science 17900 Words

Department of Computer Science University of Durham England May 2006

Abstract Satisability or SAT can easily be considered as the quintessential problem in computational complexity theory. The problem  proved to be NP-complete by Cook in 1971

[15]

 entails nding a truth-assignment for variables of a propositional

Boolean formula, such that the formula evaluates to true. SAT is fundamental to many problem solving disciplines such as; automated reasoning (AR), articial intelligence (AI) and electronic design automation (EDA), thus it is viewed as a core problem in computer science which enjoys considerable research attention. Ecient SAT-solving algorithms are of great importance in theory and practise however due to the NP-completeness of SAT it is unlikely a tractable solution to the problem exists. Until recently, research has been geared towards the theoretical aspects of SATsolving; nding eective heuristics to prune the search space of a SAT instance with the goal of rapidly converging on a solution. Less attention has been focused on the implementation issues of these proposed heuristics until recently with the development of Cha, a highly optimised solver outlining new SAT-solving methods based on engineering rather than a theoretical grounding

[4].

This paper intends to review and qualitively examine existing SAT-solving techniques through empirical analysis and make claims regarding eciency with reference to the engineering of the solvers in question. As shown with zCha, an ecient implementation can vastly speed up a solvers' overall performance. This paper hopes to present a comprehensive overview of existing SAT-solvers and make claims regarding the reasoning behind their performance and if possible suggest performance enhancements.

iii

Acknowledgements Thanks to the patient and helpful Dr. Stefan Dantchev for agreeing to supervise my dissertation. Thanks to Dr. Nick Holliman, Prof. Malcolm Munro and Mr. Brendan Hodgson for allowing me to change my dissertation topic at a late date. Lastly Thanks to Mr. M. Imran who prepared this Lyx template so I didn't have to.

iv

Contents

1

2

Abstract

iii

Acknowledgements

iv

Introduction

1

1.1

Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

1

1.1.1

Denition of SAT . . . . . . . . . . . . . . . . . . . . . . . . .

1

1.1.2

Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

3

1.1.3

Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . .

4

1.1.4

DIMACS

. . . . . . . . . . . . . . . . . . . . . . . . . . . . .

5

1.2

Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

5

1.3

Objectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

7

1.3.1

Plan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

7

1.3.2

Deliverables . . . . . . . . . . . . . . . . . . . . . . . . . . . .

7

1.3.3

Report structure . . . . . . . . . . . . . . . . . . . . . . . . .

8

Literature Survey

2.1

2.2

2.3

10

Variations of SAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.1.1

k-SAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

2.1.2

Horn-SAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

SAT instances . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.2.1

Polynomial Time Reductions . . . . . . . . . . . . . . . . . . . 12

2.2.2

Random Generation . . . . . . . . . . . . . . . . . . . . . . . 14

2.2.3

Hard Vs Easy Instances . . . . . . . . . . . . . . . . . . . . . 15

Deduction methods . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 v

Contents

2.4

3

2.3.1

Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

2.3.2

Unit resolution . . . . . . . . . . . . . . . . . . . . . . . . . . 18

2.3.3

Subsumption . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

2.3.4

Purication . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

Two Branches of Solver . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.4.1

Complete Systematic Search . . . . . . . . . . . . . . . . . . . 21

2.4.2

Incomplete Stochastic Local Search . . . . . . . . . . . . . . . 22

2.4.3

Other methods . . . . . . . . . . . . . . . . . . . . . . . . . . 23

Design

3.1

3.2

4

vi

24

Systematic Solver Design . . . . . . . . . . . . . . . . . . . . . . . . . 24 3.1.1

The Need For a New Method . . . . . . . . . . . . . . . . . . 24

3.1.2

The DPLL Algorithm . . . . . . . . . . . . . . . . . . . . . . . 25

3.1.3

Search . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28

3.1.4

Deduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

3.1.5

Conict Analysis . . . . . . . . . . . . . . . . . . . . . . . . . 34

3.1.6

Other techniques . . . . . . . . . . . . . . . . . . . . . . . . . 37

Stochastic Solver Design . . . . . . . . . . . . . . . . . . . . . . . . . 38 3.2.1

A New Powerful Method . . . . . . . . . . . . . . . . . . . . . 38

3.2.2

GSAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39

3.2.3

WalkSAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

3.2.4

Variable Selection Heuristics . . . . . . . . . . . . . . . . . . . 41

Implementation

42

4.1

Implementation Languages . . . . . . . . . . . . . . . . . . . . . . . . 42

4.2

Systematic Search . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43

4.3

4.2.1

Static and Dynamic Heuristics . . . . . . . . . . . . . . . . . . 43

4.2.2

Pointer and Counter BCP . . . . . . . . . . . . . . . . . . . . 45

4.2.3

Learning Schemes . . . . . . . . . . . . . . . . . . . . . . . . . 46

4.2.4

Other Factors . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

Local Search . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 4.3.1

Escaping Local Maxima . . . . . . . . . . . . . . . . . . . . . 48

Contents

5

4.3.2

Performance Trade O . . . . . . . . . . . . . . . . . . . . . . 49

4.3.3

Conguration . . . . . . . . . . . . . . . . . . . . . . . . . . . 49

Results and Evaluation

5.1

6

vii

51

Testing Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 5.1.1

SAT-instances Used . . . . . . . . . . . . . . . . . . . . . . . . 51

5.1.2

Solvers Tested . . . . . . . . . . . . . . . . . . . . . . . . . . . 52

5.1.3

The Testing Platform . . . . . . . . . . . . . . . . . . . . . . . 54

5.2

Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54

5.3

Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 5.3.1

Deduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56

5.3.2

Heuristics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57

5.3.3

Conict Driven Learning . . . . . . . . . . . . . . . . . . . . . 58

5.3.4

Local Search . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60

5.3.5

Other Observations . . . . . . . . . . . . . . . . . . . . . . . . 61

Conclusions

6.1

6.2

62

Achievements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 6.1.1

Importance of Decision Variables . . . . . . . . . . . . . . . . 63

6.1.2

Emphasis on Engineering . . . . . . . . . . . . . . . . . . . . . 63

6.1.3

Domain Dependent SAT-Solving . . . . . . . . . . . . . . . . . 64

Further Studies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64

Bibliography

66

Appendix

72

A Additional Information

72

A.1 Plan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 A.2 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72

List of Figures 1.1

The search space of a SAT-instance can be represented as a binary tree

5

2.1

The bipartite (2-colourable) graph G . . . . . . . . . . . . . . . . . . 14

2.2

Number of DPLL solver operations required and Probability of Satisability vs. clause to variable ratio. . . . . . . . . . . . . . . . . . . 16

2.3

A tree-like resolution refutation of φ. . . . . . . . . . . . . . . . . . . 17

3.1

Iterative dention of the DPLL algorithm . . . . . . . . . . . . . . . . 26

3.2

The adjacency relationship between variables and clauses . . . . . . . 32

3.3

Watched Literal cases for BCP. . . . . . . . . . . . . . . . . . . . . . 34

3.4

A sample Implication Graph . . . . . . . . . . . . . . . . . . . . . . . 36

3.5

The search space of local search algorithm on a 66 variable clause-set. 39

3.6

The GSAT algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

A.1 GANTT Chart . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73

viii

List of Tables 5.1

Search and conict analysis test SAT-instances . . . . . . . . . . . . . 52

5.2

Combinations of developed DPLL based SAT-solvers to test . . . . . 53

5.3

Combinations of developed Local search SAT-solvers to test . . . . . 54

A.1 lex results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 A.2 lex-learn results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 A.3 rand results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 A.4 dlcs results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 A.5 dlis results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 A.6 rdlcs results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 A.7 rdlcs-learn results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 A.8 vsids results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 A.9 gsat results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 A.10 walksat results

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76

A.11 gsat-weighted . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 A.12 gsat-tabu

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77

A.13 BCP test results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78

ix

Chapter 1 Introduction This rst chapter presents a brief overview of the motivations for writing this paper as well as outlining the subsequent chapters. Firstly, the reader  if not aquainted with basic SAT terminology  would be advised to read the following section to gain a basic understanding of SAT, including some standard notation which will used throughout this paper.

1.1

Preliminaries

An overview of essential background information including; the SAT problem definition, the complexity of SAT, examples and an insight into the SAT research community.

1.1.1 Denition of SAT This section will assume an understanding of basic propositional logic and settheoretical concepts which will be used to give a sussinct denition of SAT. Let

V = {v1 · · · vn } be an alphabet of n propositional Boolean variables. A propositional Boolean formula φ can be dened as a conjunction of m clauses such that:

φ = c1 ∧ c2 ∧ . . . ∧ cn

1

1.1. Preliminaries

2

where each ci is dened as a disjunction of literals such that:

l1 ∨ l2 ∨ . . . ∨ ln where each lj represents a literal which is either a variable, v ∈ A, or its negation

v¯. The formula φ is referred to as being in conjunctive normal form (CNF) which is widely used as the standard input to many SAT-solvers. Any arbitary propositional Boolean formula can be translated into CNF  in polynomial time  using Tseitin's Translation algorithm

[17]

which preserves equisatisability1 .

To check whether the CNF is satisable, truth values have to be assignmed for all v ∈ A. When a variable v is assigned a truth value, each literal  which is either an instance of a variable or its negation  adopts the assigned truth value. More formally, a truth assignment (TA) of a variable v can be dened as a function,

t : V → {true, f alse}, this function can be extended to a truth assignment over individual literals such that if t (v) = true then t (¯ v ) = f alse and if t (¯ v ) = true then t (v) = f alse. If dom (t) ⊂ V then the truth assignment is said to be partial, else if dom (t) = V the truth assignment is total. Note the following equivelances

φ is satisable ≡ φ is satised by a partial TA ≡ φ is satised by a total TA A partial TA can be extended to a total TA by assigning arbitary Boolean values to unassigned variables. Given any literal, it is said to be satised if and only if it is assigned the truth value true. In turn, a clause is said to be satised if and only if at least

one

literal in the clause is satised. Thus, given the nature of a logical

conjunction, a formula is said to be satised if and only if

every

clause is satised.

So given the propositional formula φ, SAT can be dened as follows; exist a truth assignment such that

φ is

satisable,

otherwise φ

φ

is satised?.

does there

If such an assignment exists then

unsatisable.

A clause can be represented as a set of literals which can be considered to be an implicit disjunction, similarly, a formula in CNF can be respresented as a set 1 Two

isable.

propositional formulas are equisatisable if either both are satisable or both are unsat-

1.1. Preliminaries

3

of clauses which can be considered to be an implicit conjunction. This method for representation using sets is benecial for inputting CNF formulae into modern SAT solvers which gives rise to the DIMACS2 CNF format, explained in

Section 1.1.4.

Clause-sets are equivlant to CNF formulas such that φ is satisable if and only if the clause-set representing φ is satisable. With reference to the representation of CNF formlea using sets, the satisability of the empty formula φ = ∅  containing no clauses  can be trivially declared as satisable (or truth functionally valid) as the notion of satisability claims that a set of clauses is satisable if there is a truth assignment for φ such that every clause evaluates to true. However, there are no clauses in ∅ that need to be true, so φ is satisable. Furthermore, the empty clause represented by  is unsatisable as for a clause to be satisable there is required to be at least one satised literal, thus a formula containing the empty clause is also unsatisable. This is the basic principle behind propositional resolution which is a powerful rule of logical inreference explained in

Chapter 2.

1.1.2 Example Consider the clause-set φ containing 5 clauses and 3 variables such that

{1 : {x, y, z¯} , 2 : {x, y¯} , 3 : {¯ y , z} , 4 : {¯ z , x} , 5 : {¯ x, y¯, z}} After a brief look it is obvious that φ is satisable as the following partial truth assignment can be dened

t (x) = true, t (z) = true assigning x to true satises clauses 1, 2 and 4, assigning z to true satises clauses 3 and 5. A random value can be assigned to y if a total truth assignment is preferred. For larger (and harder) clause-sets containing hundreds of clauses and variables it is quite evident that the simple examination of a clause-set is not sucient to 2 The

Center for Discrete Maths and Theoretical Computer Science.

1.1. Preliminaries

4

determine satisability. Various deduction techniques have been developed to solve large SAT-instances and an overview of them will be introduced in

Chapter 2.

1.1.3 Complexity Stephen Cook and Leonid Levin both independently proved the NP-completeness of SAT in 1971

[15, 18].

In computational complexity theory, some of the more

dicult problems reside in the complexity class NP3 , where NP-complete is a subset of NP that contains the hardest problems in NP, i.e. they are unlikely to reside in the complexity class P4 which contains the 'easier' problems. One property of NPcompleteness states that every other problem in NP is reducible to an NP-complete problem via a polynomial time-reduction algorithm, this implies that other problems in NP such as graph colouring, Hamiltonian Cycle and Clique can be represented as a SAT problem in CNF. Various domain specic translation algorithms allow the conversion of any problem in NP to SAT. Being NP-complete, there is no tractable algorithm for solving SAT in reasonable time, so for any CNF with n propositional variables there are 2n possible truth assignments. It is infeasible to 'brute-force' the complete search space of a SAT instance where n large, this has been the motivation for developing various heuristics to solve the problem by pruning the search space, eee

Figure 1.1

5

.

Restrictions on the type of propositional Boolean formula (explained in 2)

can give rise to specic formulations of SAT such as Horn-SAT

(where k = 2) which can be solved in polynomial time

[20].

[19]

Chapter

and k-SAT

Although complexity

and worst-case run-time of a problem is a good measue of its hardnesss, many SATsolvers can solve SAT-instances well within the bounds of the worst case O (2n ), this 3 Non-deterministic

polynomial time, implying that a non-deterministic Turing Machine can solve an NP-complete problem in polynomial time. The reader must be aware that there exists no practical implemention of a non-deterministic Turing Machine, they are meerly theoretical concepts. An alternative denition of NP states that a Deterministic Turing machine can verify the validity of a solution  such as a truth assignment for a particular clause-set to an NP-complete problem in polynomial time. 4 Deterministic polynomial time, implying that a eterministic Turing Machine can solve a problem of class P in polynomial time. 5 Taken from Lintao Zhang, Searching For Truth: Techniques for Satisability of Boolean Formulas. Phd Thesis, June 2003, Princeton University.

1.2. Motivation

5

Figure 1.1: The search space of a SAT-instance can be represented as a binary tree gives rise to the notion of the 'hard' and 'easy' distribution of SAT-instances also explained in

Chapter 2.

1.1.4 DIMACS The Center for Discrete Mathematics and Theoretical Computer Science (DIMACS) is a collaboration between Rutgers and Princeton Universities as well as a number of research rms who are committed,

to both theoretical development and practical

applications of discrete mathematics and theoretical computer science

contribution to the SAT sommunity by DIMACS was the, Satisability problems,

6

. A major

suggested format for

which denes a suggested input for todays modern SAT

solvers. Details of this format  which will be used as the input to solvers developed for this paper  can be seen in

1.2

[10].

Motivation

Researchers have been studying SAT-solving algorithms for many years  since the publication of the David-Putnam procedure  and much progress has been made 6 DIMACS,

Wikipedia.

1.2. Motivation

6

developing eective theories onto which future algorithms will be based upon. However, of equal importance to the theory behind these algorithms is the way in which they are implemented, making use of sound engineering procedures and empirical analysis which can be used to rene and optimise the eciency of these algorithms. A SAT-solving algorithm that performs well in theory is not an adequate claim for a SAT researcher to present. For the algorithm to be of practical use, a good average-case performance of the algorithm is required which can only be achieved through an extensive engineering, testing and renement lifecycle. SAT-solver engineering is mainly concerned with the implemention of the various heuristics and data-structures which form the core of modern SAT-solvers. Solvers utilising powerful algorithms  which claim to quickily solve SAT-instances  may seem impressive when presented on paper, however the true potential of the algorithm will be demonstrated if they excel in practise. Increased sophistication does not imply a more ecient algorithm and because of this researchers are trying to strike a balance between complexity, simplicity and eciency. For example, complex decisions will take longer to execute than simple decisions, however do the complex decisions deomonstrate a performance increase, or conversley, a performance loss? It can be shown that simple SAT-solving algorithms can be just as competitive as complex solvers sporting thousands of lines of source code. For example, later on in this paper a simple algorithm [23] can be presented which is capable of performance  on a certain class of SAT-instances  comparable to that of state-of-the-art SATsolvers such as Cha. As previously mentioned in Section

1.1.3,

it is not the theoretical computational

complexity of SAT that determines its hardness which is why SAT-solvers need to be comprehensively tested on a wide range of SAT-instances. This outlines the motivation for writing this paper; researchers are beginning to believe that the future of SAT research lies in the engineering aspects of algorithm implementation, though of course theoretical study is still required. This has been reected in recent research as the basic DPLL7 algorithm (explained in 7 The

Chapter 2 )

hasen't changed for

David-Putnam-Loveland-Logemann procedure which is a complete systematic search framework for solving SAT.

1.3. Objectives

7

many years, however the algorithms based on DPLL have shown signicant performance increases through a means of extensive empirical analysis of the underlying framework and as a consequence improving the overall performance of SAT-solvers.

1.3

Ob jectives

This paper aims to present a thorough analysis of modern SAT solving techniques with reference to their practical eciency. Through empirical analysis of these modern techniques, good engineering practise will be identied and explained with reference to the performance of SAT-solvers. Furthermore it will be shown that engineering, testing and renement is a powerful way of developing ecient SAT-solvers as opposed to benchmarking algorithms on worst-case complexity. Above all, this paper will present a walk-through of SATsolver development from the Davis-Putnam procedure up to state-of-the-art SATsolvers such as Cha, highlighting the solvers evolutionary progress with reference to engineering issues.

1.3.1 Plan The reader is pointed to the Appendix

A

where the original project plan and various

necessary amendments are located.

1.3.2 Deliverables The deliverables for this dissertation are split up into three sections; basic, intermediate and advanced objectives and are as follows: 1. Basic objectives (a) Implement a basic DPLL solver and test its performance on a range of SAT instances. (b) Experiment with and compare the performance of simple variable selection heuristics.

1.3. Objectives

8

(c) Compare the performance of simple data structures for the DPLL solver. 2. Intermediate objectives (a) Implement a DPLL solver using more advanced heuristics and implement a basic conict driven learning procedure. (b) Implement a basic stochastic local search solver  GSAT and WalkSAT. (c) Compare the performance of stochastic local search and complete systematic search algorithms. (d) Compare the performance of the basic and more advanced DPLL solvers. 3. Advanced objectives (a) Implement a state-of-the-art DPLL solver using advanced techniques for search, deduction and conict analysis. (b) Implement a state-of-the-art WalkSAT solver using advanced heuristical methods for variable selection. (c) Compare the performance of both solvers on a wide range of SAT instances. (d) Compare the performance of all the solvers implemented.

1.3.3 Report structure This paper is split up into 6 main chapters, including; Introduction (the current Chapter), Literature Survey, Design, Implementation, Results & Evaluation and the Conclusion. Chapter 2,

the literature survey reviews existing contributions to the SAT com-

munity and will cover topics such as deduction methods, algorithms, variations of the SAT problem, the practical 'hardness' of SAT as well as other essential SAT topics. Chapter 3

will cover in detail the algorithms which will be implemented, as well

as presenting and explaining the dierences between them.

1.3. Objectives

Chapter 4

9

covers implementation issues of the solvers such as data structure and

algorithm optimisation. Chapter 5

covers the empirical analysis of the solvers, each of the which will be

tested and their performances will be critically analyzed. Chapter 6

will present the conclusions of this paper and if possible, changes will

be suggested for existing algorithms which may enhance performance. The bibliography and appendix will follow.

Chapter 2 Literature Survey This chapter will review existing contributions to the SAT research community and explain their relevance to the objective of this paper. The main topics that will be covered include existing types of SAT algorithms and their underlying deduction methods as well as types and variations of SAT instances.

2.1

Variations of SAT

Various restrictions can be placed upon SAT-instances generating subsets  in terms of complexity  of the SAT problem such as k-SAT and Horn-SAT. For the most part of this paper randomly generated 3-SAT instances (explained below) and classic computer science problems (such as Pigeon Hole and Graph colouring reduced to a SAT problem) will be considered for testing purposes.

2.1.1 k-SAT The most common variation of SAT is k-SAT. With k-SAT, clauses are restricted to a maximum of k literals per clause, though most of the time all the clauses in most kSAT instances will contain exactly k literals. k-SAT instances can be generated from general SAT-instances by using extention variables1 or randomly generated using an algorithm. k-SAT instances where k = 3 are mainly used to benchmark SAT-solvers 1 Using

extention variables enables to transform clause-sets with arbitary width clauses into a k-SAT clause-set.

10

2.1. Variations of SAT

11

as it is easy to generate clause-sets with a desired 'hardness' whilst staying within the bounds of NP-completeness. As just stated, 3-SAT is interesting because it is NP-Complete, 2-SAT for example is not NP-complete, it is infact P-complete2 and can be solved using Aspvall's algorithm by converting the 2-SAT-instance into a graph and then proceed to search for pairs of strongly connected components (SCC) from each literal l to its negation ¯l. If there exists SSC from a literal l to its negation

¯l then the instance can be declared unsatisable, otherwise a truth assignment can be generated from the graph3 .

2.1.2 Horn-SAT4 A clause is considered to be Horn if it contains at most one positive literal. A clause is called dinitive Horn if it contains exactly one positive literal. A clause-set is called (denitive) Horn if it contains only (denitive) Horn clauses. For example

{x, y¯, z¯} is a horn clause, however {x, y¯, z} is not. The following is an example of a (denitive) Horn clause-set:

{{x, y¯} , {¯ x, y} , {x, y¯, z¯} , {¯ x, z}} As each clause may only contain up to one positive literal, the clause-set can be re-written as a series of implications

{{¯ y → x} , {¯ x → y} , {¯ y ∧ z¯ → x} , {¯ x → z}} such that the truth values of all the negative literals, implies the truth value of the singular positive literal. For example, if a clause contains no negative literals then the single positive literal must be assigned to true. If there are no positive literals present in a Horn clause-set then trivially, every variable can be assigned to

f alse, thus satisfying the clause-set. 2 The

set P-complete contains the hardest problems in P and is analogous to the set of NPcomplete problems. 3 AAI-AR lecture notes by Stefan Szeider, Durham Universirty. 4 ibid.

2.2. SAT instances

2.2

12

SAT instances

For this paper, random 3-SAT instances and various NP-hard problems (such as Pigeon hole and Graph Colouring) will be reduced to SAT for testing purposes.

2.2.1 Polynomial Time Reductions A polynomial-time reduction A ≥R B where A, B ∈ N P is an algorithm that transforms an instance of problem A into an instance of problem B , as the name of the reduction suggests, this is done in polynomial time. So, for every problem in NP it is possible to represent it as a SAT problem, this is useful for testing the ability of SAT-solvers. As many domain specic algorithms are developed to solve NP-complete problems which make good use of common structures in problem instances it is unlikely that even the most ecient SAT-solvers would be able to compete. In a sense, it is practically pointless in reducing problems to SAT in order to solve them with a SATsolver. One must also appreciate that the truth assignment of a problem reduced to SAT must be interpreted to correspond to a solution to the original problem.

Pigeon Hole clause sets can be generated in the following way5 . P Hn be the clause set that represents the

untrue

For n ∈ N, let

statement that n + 1 pigeons can

be tted into n holes such that each hole contains only

one

pigeon. The clause-set

P Hn contains the variables xi,j for 1 ≤ i ≤ n + 1 and 1 ≤ j ≤ n where xi,j is

true

if

pigeon i is in hole j . The clause-set contains two types of clauses:

• A clause {xi,1 , . . . , xi,n } for each 1 ≤ i ≤ n + 1 which represents that pigeon i is in one of the n holes.

 0 • A clause xi,j , xi0 ,j for each 1 ≤ i < i ≤ n+1 and 1 ≤ j ≤ n which represents that in each hole there is at most one pigeon. It should be observed that P Hn is unsatisable, infact it can be proved that pigeonhole clause-sets require long resolution refutations, i.e. the shortest resolution 5 Adapted

from AAI-AR lecture notes by Stefan Szeider, Durham Universirty.

2.2. SAT instances

13

refutation of a pigeonhole clause-set contains 2Ω(n) clauses [21]. Alternatively a resolution refutation can be viewed as short if the number of clauses in the refutation are polynomial in the size of the input clauses. The Pigeon Hole clause-set P H2 can be represented by the following clauses:

{x1,1 , x1,2 } {x2,1 , x2,2 } {x3,1 , x3,2 } {x1,1 , x2,1 } {x1,1 , x3,1 } {x2,1 , x3,1 } {x1,2 , x2,2 } {x1,2 , x3,2 } {x2,2 , x3,2 }

SuDoku the popular constraint satisfaction puzzle which is found in news papers worldwide can be represented as SAT. A more detailed explanation can be found in [22].

Traditional 9 × 9 grids do not prove dicult for ecient SAT solvers, however

the problem can be abstracted to much larger grids.

Graph Colouring

can be easily reduced to SAT. Given a graph G = (V, E),

where V is the set of verticies and E is the set of edges, a k-colouring of G for some

k ∈ N is a function f : G (V ) → {1, 2, ..., k} which assigns a colour to each vertex v ∈ G (V ) such that adjacent verticies do not get assigned the same colour, i.e. for every edge uv ∈ G (E), f (v) 6= f (u). If there is a k-colouring for G, then G is refered to as k-colourable. To reduce graph colouring to SAT, it would be prudent to follow the above example of Pigeon hole clause-sets in that:

• For ∀v ∈ G (V ) and ∀c ∈ {1, 2, ..., k} the variable xv,c represents, the possibility that vertex v is assigned colour c.

• A clause {{xv,c : c ∈ {1, 2, ..., k}} , v ∈ G (V )} represents that each vertex gets assigned a colour.

• A clause {{xv,c , xu,c } : c ∈ {1, 2, ..., k} , uv ∈ G (E)} represents that adjacent verticies do not get assigned the same colour. The bipartite graph G (shown in Figure

2.1 )

for example is 2-colourable, it is repre-

sented as a SAT-instance by the following clauses for which there are assignments:

two

satisfying

2.2. SAT instances

14

Figure 2.1: The bipartite (2-colourable) graph G

{x1,1 , x1,2 } {x2,1 , x2,2 } {x3,1 , x3,2 } {x4,1 , x4,2 } {x1,1 , x2,1 } {x1,2 , x2,2 } {x2,1 , x3,1 } {x2,2 , x3,2 } {x3,1 , x4,1 } {x3,2 , x4,2 } {x4,1 , x1,1 } {x4,2 , x1,2 } As can be seen by the above clause-set, reducing a k-colourability problem to SAT results in a k-SAT clause-set. To evaluate the SAT-solvers produced for this paper, other instances may be used such as

nQueens, Towers of Hanoi

and

Parity

6

.

2.2.2 Random Generation In order to test the ecieny of a SAT-solver, a reliable benchmark is needed, this entails the use of NP-hard problems reduced to SAT (above), or the creation of random k-SAT instances, specically random 3-SAT. There are a number of creation algorithms available, the simplist of which is the following: 1. Specify n variables and m clauses to create. 2. For each (3-SAT) clause randomly select a set of three variables from the pool of n variables. 3. Randomly select a truth assignment for each variable with probability 0.5. Other algorithms include

[27, 28].

The importance of knowing the 'hardness' of

the instances generated is paramount if they to be used for testing a SAT-solver as 6 http://www.intellektik.informatik.tu-darmstadt.de/SATLIB/benchm.html

2.2. SAT instances

15

there is little point in bench-marking a solver with no knowledge about the instances used.

2.2.3 Hard Vs Easy Instances As previously stated, independently of the worst-case computational complexity of SAT there exists hard and easy instances of the problem. For example, some SATinstances can be solved quickily, even with a niave algorithm

[23].

Similarly, some

instances are easy for a particular type of algorithm, i.e. local search performs very well on random 3-SAT instances

[1, 3].

The formalisation of a hard SAT-instance is hard to dene as the many dierent types of SAT-solver perform well on particular instances, also domain enhancements can increase a solvers performance on a particular instance. Researchers have turned to using SAT-instances that they can easily gauge the diculy of, this entails using randomly generated 3-SAT or instances generated from congurable algorithms. Generally, the following assumption can be made regarding a random 3-SAT clause-set with a xed number of k variables:

• Short clause-sets, that contain fewer clauses, are under-constrained and therefore have many satisfying assignments, so an assignment is likely to be found early on in the search.

• Longer clause-sets are over-constrained therefore are most likely unsatisable, so a contradiction will be found easily.

• Instances inbetween are considered much harder as they contain few satisfying assignments and to nd a contradiction many variables will be have to assigned truth values. It has been found through empirical analysis that the hardest 3-SAT instances occur when there is a ratio of 4.3 clauses to each variable. They are also harder when there is a 50% chance that the instance is satisable because the solver has to do more work to deduce a satisable or unsatisable solution (with reference to the points

2.3. Deduction methods

16

Figure 2.2: Number of DPLL solver operations required and Probability of Satisability vs. clause to variable ratio. listed above), see

Figure 2.2

7

[12, 25].

It is important to use the above ndings when chosing SAT-instances to performing empirical analysis on new SAT-solvers as it unprofessional and unproductive to (unknowingly) make claims about the average case performance of a solver on a range of easy SAT-instances. For example, taken from Selman et al.

[3]

claims

made by Goldberg (that SAT could be solved on average in polynomial time) in [30]

2.3

were shown to be false by Franco and Paull in

[31].

Deduction methods

Various deduction methods can be used and combined to solve SAT-instances. They can also be integrated with systematic search algorithms, for example the DPLL algorithm is basically a depth-rst-search with unit resolution. The following section 7 Taken

from [25].

2.3. Deduction methods

17

Figure 2.3: A tree-like resolution refutation of φ. reviews existing deduction methods for propositional clause-sets.

2.3.1 Resolution8 Resolution is a basic inreference rule in propositional logic which states that given a clause-set φ and any two clauses A, B ∈ φ, with a literal x ∈ A and x ¯ ∈ B it is possible to dervie the clause C = A − {x} ∪ B − {¯ x}, in other words:

(x ∨ y1 ∨ . . . ∨ yn ) (¯ x ∨ z1 ∨ . . . ∨ zm ) (y1 ∨ . . . ∨ yn ∨ z1 ∨ . . . ∨ zm ) It can be said that the (resolvent) clause C was derived by resolution from φ, hence if there exists a resolution derivation from φ that contains C then φ `R C . If φ `R  then φ can be declared as unsatisable. A resolution derivation that contains  is called a resolution refutation, a resolution refutation is said to be treelike if every clause in the refutation occurs exactly once, i.e. no clauses are re-used for future derivations. For example, taking the clause-set φ such that:

{{x, y} , {¯ x, y} , {x, y¯} , {¯ x, y¯}} It can be shown that φ is unsatisable through resoluion, in that φ `R  which is shown in

Figure 2.3.

8 Adapted

from AAI-AR lecture notes by Stefan Szeider, Durham Universirty.

2.3. Deduction methods

18

2.3.2 Unit resolution Often called unit propagation for reasons explained below, unit resolution can be applied to a clause-set which contains a unit clause.

Unit clauses

are clauses of cardinality 1. For the unit clause to be satisable,

the single literal within the unit clause must be satised, thus it can be assigned a truth value which must be included in a satisfying assignment.

Implied clauses

are clauses of cardinality n that contain n − 1 unsatised

literals, thus the only unassigned literal must assigned a truth value that satises the clause.

Conict clauses are clauses of cardinality n that contain n unsatised literals. If a conict clause occurs then the current truth assignment  whether partial or total  does not satisfy the clause-set. Given a clause-set φ that contains the unit clause {x} every satisfying truth assignment of φ must contain t (x) = true. Hence the clause-set φ [t] (where t is a (partial) truth assignment) can be obtained by unit resolution such that every clause containing the literal x can be removed and the literal x ¯ can be removed from all remaining clauses. It should be noted that φ is satisable if and only if φ [t] is satisable. In other words:

(x ∨ y1 ∨ . . . ∨ yn ) (y1 ∨ . . . ∨ yn )

x¯

For example the following clause-set φ can be shown to be unsatisable through unit resolution:

φ = {{x, y} , {¯ x, y} , {x, y¯} , {¯ x, y¯} , {x}} Identify the unit clause {x} and perform unit resolution on x:

φ [x = true] = {{y} , {¯ y }} Identify the either the unit clause {y} or {¯ y } and perform unit resolution on y or y¯:

2.3. Deduction methods

19

φ [x = true, y = true/f alse] = {} Unit propagation is named so because as can be seen in the above example, through one application of unit resolution the rest of the variable assignments will be propagated in a ripple eect as implied clauses are generated  forcing the truth assignment of the other variables  until no more unit clauses. This denes the unit propagation procedure which forms the theoretical basis for all DPLL type SAT-solvers.

2.3.3 Subsumption9 Given two clauses A and B and if A ⊂ B then it can be said that A subsumes

B and that B is subsumed by A. Given a propositional clause-set φ such that 0

A, B ∈ φ and A subsumes B then the clause-set φ = φ − B is satisable if and only if φ is satisable. The intuition behind subsumption is that if there is a truth assignment that satises the larger clause B then the truth assignment that satises

A is contained within the truth assignment that satuses B . Subsumption is often used to simpify clause-sets inbetween the application of resolution or unit propagation.

2.3.4 Purication Given a clause-set φ and suppose a literal l appears in some clauses of φ and the complement of l appears in no clauses of φ, then the literal l can be said to be pure and the clause-set φ [t] (where t is a (partial) truth assignment including an assignment to the pure literal) can be obtained by removing every clause from φ which contains l. The idea behind pure literal elimination is that if a literal only appears in one phase it can be assigned a truth value such that it satises all the clauses it appears in. Given the following clause-set φ such that: 9 Adapted

from AAI-AR lecture notes by Stefan Szeider, Durham Universirty.

2.4. Two Branches of Solver

20

{{x, y, z¯} , {¯ y , z, v} , {x, v, y¯} , {¯ y , z¯, v} , {z} , {¯ x, y}} which contains a pure literal v that can be assigned the truth value true thus satisfying any clause in which v appears in, hence it is possible to give a new clauseset φ [t] such that:

φ [v = true] = {{x, y, z¯} , {z} , {¯ x, y}} so φ is satisable if and only if φ [v = true] is satisable.

2.4

Two Branches of Solver

As mentioned before, soliciting a brute-force search upon the search space of a hard (or large) SAT instance with the hope of quickily obtaining a truth assignment is not possible. Any brute-force search would require an exponential number of opertations which is why SAT researchers have spent considerable time developing ecient SAT-solving methods. Research has recently split into the development of two types of solver:

• Compelete systematic deapth-rst-search  of the search space  making use of deduction inference rules such as unit resolution. They are all able to determine the satisability of satisable and unsatisable instances, thus they are known as complete.

• Stochastic local search, using techniques such as simulated annealing and greedy hill climbing. They are unable to deduce unsatisability of a clause-set, thus are known as incomplete. Both types of solver have proved eective at solving a wide range of SAT-instances and their underlying frameworks will be discussed below, along with a brief mention of less popular but eective methods.

2.4. Two Branches of Solver

21

2.4.1 Complete Systematic Search There are two basic complete frameworks for solving SAT: the Davis-Putnam (DP) procedure

[8]

and the David-Putnam-Loveland-Logemann (DPLL) procedure

The Davis-Putnam Procedure ,

[7].

given a propositional formula, tackles the

Satisability problem by attempting to apply the propositional resolution rule to each variable that appears in the clause-set. The DP procedure will iteratively perform resolution until it either encounters the empty clause, which is unsatisable or can be simplied no further but does not contain the empty clause, implying that the clause-set is satisable10 . In addition to the application of resolution, after resolving clauses, DP simplies the clause-set by performing subsumption. DP also omits tautological11 clauses. The performance of DP depends greatly on picking the right variables to perform resolution with. Various heuristics have been developed to improve the chances of picking the optimal variables but the procedures' run-time is still exponential. DP is however a great deal more ecient than the brute-force approach as each time resolution is applied, a whole sub-tree of the search space is eliminated.

The Davis-Putnam-Loveland-Logemann Procedure , unlike the DP procedure, which cannot return a satisfying assignment, DPLL does return a satisfying assignment if one exists. It is based on the unit resolution inference rule and incorporates the following three ideas:

• Search: Heuristically chose a variable to perform unit propagation with. • Deduction: Perform unit propagation and literal purication on the clause-set. • Conict analysis: If a conicting clause occurs during unit propagation, try and diagnose the reason why and prevent similar occurences from happening in the future. Backtrack up the search tree out of the sub-tree which does not contain a satisfying assignment. 10 DP

cannot actually nd a satisfying assignment, it can only show whether a clause-set is satisable or unsatisable. 11 A clause containing a literal l as well as it's negation ¯ l, which is true under all interpretations.

2.4. Two Branches of Solver

22

Various variable selection heuristics can be employed such as; selecting the variable which occurs most often or selecting the variable which induces the most unit propagations. Branching heuristics can have a tremendous impact on reducing the size of the search space. These issues will be discussed in the following two Chapters. The DPLL algorithm is usually shown as a recursive procedure which is convienient as data structures (the current variable assignment) are preserved for each recursive call of the algorithm but for the sake of ecieny and the use of more more complex methods  which are used in modern DPLL solvers  it is implemented iteratively. Recent research has seen the development of solvers such as GRASP, SATO, Cha and Berkmin

[2, 4, 14, 24]

which have made huge advances in the eld of

systematic SAT-solvering whilst still utilising the basic DPLL framework.

2.4.2 Incomplete Stochastic Local Search Stochastic local search algorithms are a completely dierent breed of SAT-solver, research have shown them to be very powerful and ecient for nding satisfying assignments; the two main local search solvers include GSAT

GSAT . As stated previously,

[3]

and WalkSAT

[1].

some of the most powerful algorithms for SAT-

solving and hill-climbing style algorithms that view SAT as an optimization problem; GSAT is one specialization of hill-climbing tailored to SAT. Consider a SAT-instance with n distinct propositional variables and m disjunctive clauses. Viewed as an optimization problem, the set of states V is the set of possible truth assignments. Viewed as a maximization problem, the objective function obj (n) ≤ m denotes the number of clauses that are satised in state v ∈ V . States are assignments of the n propositional variables to {0, 1}. A convenient representation for such an assignment is a bit string bi ∈ {0, 1}, where bi denotes the truth value of the ith propositional variable. Based on this state representation, GSAT uses the following neighborhood operation:

N (v) = {u ∈ V : HamDist (u, v) = 1}

2.4. Two Branches of Solver

23

which is the set of states that are reachable from v via exactly one bit / variable ip12 . In practise, GSAT implements the force-best-move heuristic, which forces it to accept some move, even if the best-move beyond the current state is not in fact an improvement. This approach sometimes enables the algorithm to proceed beyond local optima unlike other local search algorithms which may have to restart when reaching a local maxima.

GSAT + Walk which was inspired by Papadimitriou's random walk algorithm for 2-SAT [32], which nds a satisfying assignment in O (n2 ) bit ips for any 2-SAT formula with n variables. GSAT + Walk acts like GAST with probability p, but with probability p − 1 it ips the truth assignment of a variable in a random unsatised clause. This adds random noise to the hill climbing process, thus hopefully allowing it to avoid local maxima.

WalkSAT

is empirically the best algorithm for SAT-solving. Like GSAT +

Walk, WalkSAT ips the assignment of some variable v that appears in an unsatised clause C , doing so instantly renders C satised but also has a tendency to render previously satised clauses unsatised. The break value of a variable v at is dened as the number of clauses that are satised by the current truth assignments but break when the truth assignment of v is ipped. With probability p, WalkSAT greedily ips the truth value of a variable of minimal break value, for some unsatised clause. Otherwise, with probability p − 1 WalkSAT randomly ips the truth assignment of a variable.

2.4.3 Other methods As well as DP(LL) and stochastic local seach, many other SAT-solving methods have been proposed however for the sake of simplicity, this paper will concentrate on the two aforementioned methods. The reader should be aware that many other methods exist such as using neural networks [33], Stalmarck's Algorithm [16], using simulated annealing and genetic algorithms local search) 12 Hamming

[34],

and Hybrid algorithms (Complete

[35].

distance is a measure of the dierence between two binary strings of equal length. A hamming distance of one implies that two sequences dier by one bit.

Chapter 3 Design As the aim of this paper is to compare the ecieny of a range of SAT-solvers, naturally an implementation of them will be required so an empirical analysis can be performed. This chapter presents an architecture  which will be covered in great depth  for systematic and stochastic solvers based on DPLL and GSAT / WalkSAT respectively, although more focus will be on systematic solvers.

3.1

Systematic Solver Design

The most widely studied systematic search algorithms are the DP procedure and DPLL algorithm which will be discussed below.

3.1.1 The Need For a New Method Although the DP procedure can solve small to medium sized SAT-instances, it is unable to solve SAT-instances which require long resolution refutations  usually derived from EDA applications and various NP-hard problems. Long resolution refutations imply that an exponential number of clauses will have to be derived. Exponsential memory will be required to store the clauses, meanwhile the whole resolution process  obtaining the empty clause or exhausting the search space  takes exponential time. Furthermore, the DP procedure is usually dened recursively which implies it heavily uses the stack memory allocated to the program run-time environment, 24

3.1. Systematic Solver Design

25

creating even more memory usage problems. Resolution (if niavely implemented) also requires the manipulation  concatenation of clauses and deletion of literals within clauses  of lists which requires considerable computational time. Despide many negative points, the DP procedure is a sound and complete method for SAT-solving thus it can be used as a baseline benchmark for future developments to improve upon. The inadequacies of the DP procedure gave way for the development of the DPLL algorithm explained in the next section.

3.1.2 The DPLL Algorithm As mentioned previously, DPLL can be viewed as a systematic, backtracking, depthrst-search algorithm and due to this nature  like many tree traversal algorithms  it is often represented recursively, this allows DPLL to conserve the current (partial) truth assignment with each recursive call. However, as with the DP procedure, a recursive implementation tends to be more resource intensive, hence an iterative approach is usually prefered for serious implementations, this also allows the solver to use a more complex conict analysis procedure incorporating non-chronological backtracking (explained in

Section 3.1.5 ).

With the introduction of the GRASP solver [2], a standard framework for DPLL solvers was dened. The performance of DPLL solvers varies only due to dierent implementations of the three main functions of the algorithm; search, deduction and conict analysis.

An iterative implementation of DPLL can be seen in

Figure 3.1

1

.

DPLL is based around the manipulation of data-structures; a clause-set and a list of variables. As mentioned, DPLL is related to DP in that it still uses (unit) resolution, however the dierence with DPLL is that the clause-set is not actually manipulated, however constant sized meta data about the clause set is manipulated (usually counters or pointers) to keep track of conicting and unit clauses. The basic ow of DPLL  with reference to

Figure 3.1

 is as follows:

Firstly, a CNF clause-set is parsed to create an initial clause database and list of variables. Clauses are ususally stored in a two dimentional list; the second dimention 1 Adapted

from Propositional Satisability and Constraint Programming: A comparative survey, Microsoft, October 2005.

3.1. Systematic Solver Design

Figure 3.1: Iterative dention of the DPLL algorithm

26

3.1. Systematic Solver Design

27

storing the literals of the clauses. Variables are usually stored in an array. Additional meta data is stored about clauses and variables which is needed for the solving process. Before the solving process starts all of the variables are assigned an

undened

truth value. One feature of DPLL that this paper has neglected to mention so far is preprocessing which performs deduction upon a SAT-instance before heuristically picking a decision variable, so any deduction that takes place during preprocessing can be kept and will not cause concits in the future search process. Some easy SATinstances can be trivially declared satisable or unsatisable through pre-processing but this is very uncommon for most clause-sets. Preprocessing entails the use of any deduction methods, usually it will look for a pure literal and / or a unit clause and perform unit propagation on the implied literals. During preprocessing the variables assigned during unit propagation or literal purication will be assigned a level

decision

of 0.

If preprocess() cannot determine satisability then the main solving loop kicks in. A variable is selected from the variable list using the solvers selection heuristic;

decide_next_branch() and is assignmed a truth value accordingly. This variable is usually referred to as the decision variable, and as the search space of a SAT-instance can be viewed as a tree, each variable selection is usually assigned a decision level which represents a level of the search tree. The decision level is used to determine unsatisability and backtrack if there is a conict. Once a variable is selected then deduce() is executed which  usually using unit propagation  begins to propagate assignments for variables until no more implied clauses are generated. Variables that are assigned during unit propagation are assigned the same decision

level

as the last decision variable, again this is for the

benet of the conict analysis procedure. The unit propagation will either terminite with a conict or non-conicting status corresponding to whether a conicting clause was encountered :

• If the status is not conicting and all variables have been assigned then the solver will return satisable.

3.1. Systematic Solver Design

28

• If the status is not conicting but variables still require assignments then

decide_next_branch() will be called once again. • If a conict did occour then the analyse_conflict() procedure will be iniatied as the current assignment cannot satisfy the clause-set. The conict analysis procedure determines the reason for the conict and then uses backtrack() to un do all the previous variable truth assignments until the solver backtracks to the decision level specied. A new variable to branch on will usually be chosen by the conict analysis procedure and deduction will begin once again, this time searching a dierent sub tree of the search space which will hopefully lead to a satisfying assignment. If the solver has to backtrack to a decision level less than zero  below the root of the search tree  then it can be said that the instance is unsatisable as a conict was generated for every possible truth assignment. Complex conict analysis procedures can perform conict driven learning

[2]

which helps to speed up future conicts and

features an integral part of state-of-the-art SAT-solvers. The whole solving loop can continue indenetely until satisability is determined, however usually the solver is set to run until a time-out is triggered. The following sections will cover dierent implementation of the four main DPLL functions.

3.1.3 Search If there exist no facts to enque for unit propagation and / or there are no unit clauses present in the clause-set then the select_next_branch() procedure is invoked and it heuristically choses a variable to perform unit propagation with. This guarentees the completeness of DPLL as without search, unit propagation could not occur if no unit clauses existed which is common in many clause-sets. The search methods incorprated in to DPLL, often referred to as a branching heuristics, can signicantly alter the ecieny and eectivenes of the algorithm. Many branching heuristics have been proposed in the past and have been compared in the following papers [11, 38].

3.1. Systematic Solver Design

29

Essentially the branching heuristic procedure unions the current clause-set with a unit clause (the variable and its truth value which was heuristically selected) which is enqueued for unit propagation. For example, if the variable x was selected and assigned the truth value true the new clause-set would be:

{{x, y¯} , {¯ z , y, x¯} , {¯ y , z} , {x, z}} ∪ {{x}} In this sense it can be said that an assumption is made, if the assumption is incorrect then conicts will be generated, possibly much further down the search tree. Ideally, if the heurstic could non-deterministically choose a correct variable and truth assignment every time then no conicts would occur. The general idea of the decision heuristic is:

• If the clause-set is satisable then try to quickily nd a satisfying assignment by pruning the search space where no assignments are likely to exist, or concentrate the search where a satisfying assignment is likely to exist.

• If the clause-set is unsatisable then try to quickily nd a contradiction by forcing the occurence of conicting clauses. There are many variable selection heuristics available to use, including the following:

Randomisation

is often used in SAT-solvers, however in this case, 'heuristic',

should be used in a loose sense; a random variable is picked from the variable list and assigned a random truth value. It takes little computational time and can be eective when used with randomly created 3-SAT instances.

Dynamic Largest Combined Sum or DLCS [2] is the rst in a range of literal counting heuristics. Let pos (x) be the number of occurences of x in unresolved clauses2 and neg (x) be the number of occurances of x ¯ in unresolved clauses. A variable is chosen which maximises the equation pos (x) + neg (x). Then if pos (x) ≥

neg (x) then assign x as true, otherwise assign x as f alse.

Dynamic Largest Individual Sum

or DLIS

[2]

is similar to DLCS however

it picks a variable where either pos (x) or neg (x) is maximal. A truth assignment 2 Unresolved

clauses are neither satisable or unsatisable.

3.1. Systematic Solver Design

30

is chosen in the same manner as DLCS.

RandomDLCS

is the same heuristic as DLCS, however the truth assignment

of the variable with the best score is determined randomly

MOM's Heuristic

[2].

which stands for Maximum occurences in clauses of mini-

mum size aims to maximise the function




2k f (l) + f ¯l + f (l) · f ¯l where f (l) is the number of occurences of l in the smallest unresolved clauses. The constant k is just a tuning parameter. The output of the function gives a rough estimate of how many unit propagations would occur after assigning the variable of literal l a truth value. Other similar heuristics include the Jeroslow-Wang Heuristic Heuristic

[39]

and BOHM's

[40].

VSIDS

which stands for Variable State Independent Decaying Sum is a rela-

tively new heuristic proposed by the developers of the Cha solver [4]. It is dierent with respect the heuristics mentioned above, in that they use literal counting to heuristically select a variable, which requires a lot of computation (as all unresolved clauses need to be traversed). VSIDS, however  as the name suggests!  is variable state independent, in that the heuristic does not depend on the state of the current partial truth assignment, hence no clauses need to be traversed. This is

very

benicial in terms of eciency. The VSIDS heuristic keeps scores for each literal (l and ¯l), before solving begins the scores are set to the number of occurences of each literal in the clause-set. The key to the heuristic is that it works in conjunction with conict driven learning (explained in

Section 1.1.5 ),

so when a conict clause is added to the database, the

scores of the literals contained within the new clause are incremented by a constant factor. Over a period of time, the scores are set to decay by another constant factor, hence there is more emphasis on recently added clauses and the literals contained within them. The literal with the highest score is enqueued for unit propagation. A variation on VSIDS is the heuristic used in the solver Berkmin

[24]

which

3.1. Systematic Solver Design

31

considers only literals added within the last unresolved learnt clause, as opposed to every literal.

3.1.4 Deduction Deduction, often called binary constaint propagation (BCP) is the integral part of a DPLL solver. After a variable has been selected for deduction deduce() is called and BCP begins which entails simplifying the clause-set given the assumption made from the search procedure. Like the branching heuristic, the deduction method can be implemented in a number of dierent ways, however there is obviously a basic requirement in that the method of deduction is sound, such that it always makes a correct series of deductions that simples the clause-set. Many deduction methods have been proposed in the past, including unit propagation and pure literal elimination which were specied in the original DPLL paper [7].

Pure literal elimination, described in

Chapter 2

entails the identication of lit-

erals which only appear in one phase and as a consequence, removing all clauses containing the pure literal. This technique while powerful  it can prune many subtrees from the search space  is very resource intensive as it requires a complete linear search of the clause-set, maintaining occurence counters for each literal. An analysis of the complexity of pure literal elimination was performed in

[37]

where

the conclusion was made that it is too costly for inclusion in modern SAT-solvers. Unit propagation on the other hand, has proved to be the most ecient dedution method for DPLL type solvers and will be covered in detail for the remainder of this paper. There are a number of dierent unit propagation implementations, however the most common include counter-based and pointer-based methods.

Adjaceny Lists are used by most DPLL solvers to associate each variable with all of the clauses in which it appears (as a literal). The adjacency lists for each variable are usually split into two parts; one for each occuring phase of the literal. A representation of how adjacency lists operate can be seen in Figure 3 Taken

3.2

3

. Adjacency

from http://www.infsec.ethz.ch/education/ws0506/decproc/lec01-dpll.pdf, 20th April.

3.1. Systematic Solver Design

32

Figure 3.2: The adjacency relationship between variables and clauses lists are an essential pre-requisite for counter based BCP algorithms.

Counter-based BCP originally proposed in [42] entails the usage of adjacency lists to keep track of unresolved, implied and conicting clauses. Each clause is usually assigned 2-counters; one keeping track of satised literals and the other keeping track of unsatised literals. When a variable is assigned a truth value, all its adjacent clauses are visited and the literal counters are updated, there are three cases to consider which correspond to states of a clause:

• If the unsatised literal counter is equal to the size of the clause then the clause is conicting.

• If the unsatised literal counter is equal to one less than the clause size and the satised literal counter is zero, then the clause is implied and the clause will have to be searched for the implied literal which can be equeued for unit propagation.

• If none of the above cases occur then the clause is neither conicting nor implied, so no counters need to be updated. It must be noted that the algorithm only needs to consider the above when a variable assignment causes a literal to be unsatised. When an assignment generates satised literals then the satised literal counter is incremented and as the clause is satised none of the above cases can occur. When backtracking occurs, the various counters

3.1. Systematic Solver Design

33

have to be decremented accordingly. Alternative implementions of counter-based BCP use only

one

literal counter which are explained in

Chapter 4.

Pointer-based BCP proposed in [4] does away with the adjaceny list approach and instead for each clause stores two literal pointers. Literal watching is based on that fact that given a clause c of cardinality |c|, an implication will only occur when

|c|−1 literals are unsatised. Hence it is possible to ignore the rst |c|−2 assignments for a particular clause. this implies that the BCP algorithm only needs to 'watch' any two literals within a clause. Providing there are atleast 2 not-unsatised literals then the clause is either unresolved or satisable. The watched literals can be held in a two dimentional array, with the rst dimention containing each literal and its negation, and the second containing a reference to each clause in which the literal is watched. When a variable is assigned a truth value, only the clauses containing a literal that is watched need to be updated where the following cases may occur if a literal l being watched is unsatised by a truth assignment:

• The BCP algorithm will try to nd new a not unsatised literal m to replace l  the literal pointer is moved from l to m. The clause is still neither implied or conicting.

• If no not unsatised literals can be found to swap the pointer with, then the clause is conicting.

• If the other watched literal is satised, then the clause is satised. • If the only other not unsatised literal is the other watched literal, then the clause is implied. The reader is referred to

4 Figure 3.3

which explains the above points graphically.

The beauty of pointer-based BCP is that during backtracking, no computation has to be made apart form undoing variable assignments. 4 Taken

from Lintao Zhang, Searching For Truth: Techniques for Satisability of Boolean Formulas, Phd Thesis, June 2003, Princeton University.

3.1. Systematic Solver Design

34

Figure 3.3: Watched Literal cases for BCP. A recent paper

[6]

has reviewed data structures for DPLL type SAT-solvers and

concluded that Watched Literals are the most ecient BCP implementation. Other pointer based BCP implementions include Head-Tail lists SATO solver

[14]

[41]

introduced in the

which are competitive but not as ecient as Watched Literals.

3.1.5 Conict Analysis During BCP, a conicting clause is generated if all the literals of a clause are unsatisable, thus rendering the clause containing them unsatisable. When a conicting clause is encountered by the BCP algorithm all deduction halts so any facts equeued for unit propagation are discarded and the conclict analysis procedure begins. Conict analysis is mainly used determine and resolve the reason for the conict, then backtracking erases the variable assignments that led to the conict. Compelex concit analysis procedures can utilise techniques such as conict driven learning which involves recording of additional clauses into the clause database which will prevent similar conicts from happening again. A concit will only happen when a clause c has at least |c| − 2 unassigned literals (all assigned literals (if any) have to be unsatised) for any given decision level and the BCP step for the current decision level assigns the remaining literals such that they are unsatised. At this point the current truth assignment does not satisfy the clause-set.

3.1. Systematic Solver Design

35

If every decsion made throughout the search process is correct then no conicts will occur! For example with 2-SAT it is possible to solve an instance with only one decision variable to start o the unit propagation algorithm (i.e. making one or more clauses implied), if a correct decision variable is chosen then all the values for the other variables will be correctly assigned

[20].

Unfortunately with large SAT-

instances this is very unlikely to happen and solvers will inevitably assign a value to a variable that unsatises the clause-set at some point during the search  this is why conict analysis is needed.

Basic conict analysis involves storing an 'exhausted' ag for each variable such that when a conict occurs, the variable with the highest decision level that has not been exhausted is ipped and its other phase is tried. All variable assignments up until the exhausted variable will be erased and the exhausted variable will be enqueued for unit propagation having been assigned a dierent phase. In

[5]

it

has been mentioned that this basic conict analysis method works well for random SAT-instances because they have no structure, hence clause learning does not present many benets. If a SAT-instance has an underlying strucure then this can be used to the advantage of the solver which is where conict driven learning comes into play, this can be considered one of the more complex parts of the solver which is essential for solving certain classes of clause-sets quickily.

Complex

conict analysis involves utilisation of the implication graph which

represents the series of variable assignments throughout the search process. The implication graph is an instance of a directed acyclic graph (DAG) where the verticies represent variable assignments and the directed edges represent the reasoning behind the assignments5 ; edges originate from antecedent variables and point to consequent variables. Decision variables have no antecedent variables as they are chosen by the branching heuristic. A sample implication graph can be found in

Figure 3.4

6

. Each

variable is represented by Va (b) where a is the variable id and b is the decision level. The implication graph is represented as a series of pointers in a solver implemen5 From 6A

now on the terms vertex and variable can be considered synonymous. common implication graph example, taken from [5].

3.1. Systematic Solver Design

36

Figure 3.4: A sample Implication Graph tation; assigned variables point to the their antecedent clause, which contain the unsatised literals that implied the consequent variable. A conict occurs when a variable appears once for each phase  true and f alse. If there is no conict then obviously each variable will appear once in the graph. The implication graph can be analyzed and the reason for the conict can be deduced, however two important structural properties of implication graphs need to be introduced rst; vertex dominance and unique implication points (UIP)

[2]:

• Vertex a is said to dominate vertex b iif any path from the decision variable of a to b needs to go through a7 .

• A UIP is a vertex at the current decision level that dominates both of the conict verticies. Every decision variable is a UIP. A UIP is a single reason that implies a conict, for example chosing a particular decision variable may cause a conict. When a conict occurs the implication graph can be

cut

into two sections; the

conict side in which the conict variables reside and the reason side, where all other variables raside. Cuts are used to generate conict clauses which can be learnt 7 Taken

from [5].

3.1. Systematic Solver Design

37

by the solver. All variables which have an edge directed to the conict variables (on the conict side) can be considered as the reason for the conict. It is along this cut that a conict clause can be generated. for example in

Figure 3.4

the following

conict clause can be generated:

{x19 , x5 , x3 , x1 , x17 } Dierent learning mechanisms meerly make the cut at dierent places through the implication graph. There are many other vertex cuts that can be made in Figure 3.4, some creating conict clauses which may be more useful than others. clause learning is a crucial part of modern SAT-solving hence generating useful conict clauses helps greatly with pruning of the search space. Once a conict clause has been generated, the backtracking algorithm will backtrack to highest decision level of the variables in the conict clause, all variable assignments up until the backtrack level  which may be be several levels above the current level  will be erased, hence the term non-chronological backtracking. The DP procedure or recursive DPLL cannot do this as the algorithm is recursive and has to traverse back through the recursive calls. A more detailed description of this method of conict analysis using implication graphs can be found in

[5, 2]

which were used as a basis for this explination.

3.1.6 Other techniques Other techniques in conjunction with DPLL solvers can be used though most developers stick to improving the three main functions mentioned above.

Restarting

the search process can be used in a number of ways. For example,

if n conict clauses are encountered then restart the search. The search could also be restarted randomly after a certain period of time as the solver may have been searching in a 'bad' part of the search space. If the solver employes conict driven learning then it can make use of the added conict clauses after the search is restarted.

Early termination

can be used when a partial truth assignment satises a

3.2. Stochastic Solver Design

38

clause-set. If the objective of the solver is just to nd a satisfying assignment then there is no need to nd a total truth assignment. For example the clause-set

{{x, y} , {x, z¯}} is satised after assigning the variable x to true, the other variables can be ignored.

3.2

Stochastic Solver Design

Stochastic local search oers a completely dierent method for SAT-solving, viewing SAT as an optimisation problem. As local search solvers are incomplete by design, they cannot prove the unsatisability of a clause-set. This is an obvious disadvantage, however the speed in which they can produce satisfying assignements cannot be matched by any other class of SAT-solver

[13, 29].

3.2.1 A New Powerful Method The basic idea of stochastic local search algorithms is to rapidly converge on a satisfying assignment whilst preventing getting stuck in local maxima8 . As stated in Chapter

2

a typical stochastic local search algorithm is based around ipping the

the truth assignment of a variable within the variable set. This is usually achieved greedily via an optimisation hueristic as well as randomly to add noise to the search process which hopefully helps the solver avoid local maxima. The following algorithms (GSAT

[3]

and WalkSAT

[1])

both use the same basic

framework, that is; given a specied number of tries and a number of ips (for each try), the algorithms use greedy hill climbing to nd a satisfying assignment, where the (number of) optimal states are equivelant to a satisfying assignments. They will incrementally ip the truth values of indiviual variables until they nd a satisfying assignment or the maximum number of tries is reached. Figure 3.5

shows a typical search history for a greedy local search solver such

as GSAT. The reader will notice that the algorithm rapidly optimises the truth assignment at the beginning of the search, where as it struggles to leave plateaus 8 Local

maxima (or minima) is dened as a search state of which all of its neighbours do not include a more optimal state.

3.2. Stochastic Solver Design

39

Figure 3.5: The search space of local search algorithm on a 66 variable clause-set. later on in the search. Ideally the plateaus shown would be shorter or non-existent, however due to the greedy nature of local search algorithms they nd it harder to locate better moves later on during the search.

3.2.2 GSAT GSAT or Greedy Algorithm for Satisability

[3]

as it is alternatively known follows

the framework mentioned above and for every ip it uses the rule:

• For every variable v let make (v) be the number of unsatised clauses which become satised through ipping the truth assignment of v and let break (v) be the number of satised clauses which become unsatised through ipping the truth assignment of v .

• ip v which maximises the function make (v) − break (v). Hence a positive result increases the number of satised clauses, a zero result makes a sideways move and a negative result increases the number of unsatised clauses. GSAT's ability to make sideways (and downwards) moves allows it to excape from local maxima and as can be seen in Figure 3.5, this is what forms the plateaus during the search. GSAT can either be congered to halt if the current try if it gets stuck in a local maxima, or it can carry on  making a downards move  hopefully to converge on a solution later in the search. Calculating the make and break count

3.2. Stochastic Solver Design

40

Figure 3.6: The GSAT algorithm for all variables takes considerable computational time however it is a good way to determine which variable to ip. The pseudo-code for GSAT can be found in Figure 3.6

9

.

3.2.3 WalkSAT WalkSAT is generally viewed as the fastest and most powerful SAT-solver to date. It implements a few simple changes from the GSAT framework vastly increasing it's speed and ecieny. Again, WalkSAT follows the framework mentioned above and implements the following rule:

• With probabiltiy p chose a variable occuring in a random unsatised clause and ip its truth value.

• With probability 1 − p follow the standard GSAT scheme, however conne the 9 Taken from Lintao Zhang, Searching For Truth: Techniques for Satisability of Boolean Formulas, Phd Thesis, June 2003, Princeton University.

3.2. Stochastic Solver Design

41

variable selection to a random unsatised clause. WalkSAT can converge on a solution very quickily performing roughly 40000 ips a second, as when it applies variable selection it only has to consider variables occuring within

one

unsatised clause. Flipping a random variable in an unsatised clause

will always satisfy one clause and it enables WalkSAT to escape from local maxima. It has been shown that restricting the variable selection to only one unsatised clause vastly improves the speed and eectiveness of the algorithm

[1].

3.2.4 Variable Selection Heuristics Like the DPLL algorithm, local search algorithms can be implemented with comprehensive variable selection heuristics as opposed to randomly selecting variables or using a make / break count. The motivation behind these heuristics is the avoidance of local maxima. Heuristics include: Tabu earch

[45],

Novelty

some of which are discussed later in this paper.

[46]

and clause weighting

[44],

Chapter 4 Implementation This short chapter covers issues regarding the ecient implementation of the SATsolvers described in

Chapter

3. Emphasis will be on comparing the dierence of

particular algorithm implementations and highlighting good engineering practise. Source code listings will not be included here, however all C++ code can be accessed from http://www.dur.ac.uk/r.m.willis/sat.zip.

4.1

Implementation Languages

SAT-solvers are intricate pieces of software, incorporating complex algorithms in which there can be no scope for errors. SAT-solvers, by dention are required to be sound (and complete) in that they should always return the correct answer given an arbitary SAT-instance, hence any bugs that cause the solver to malfunction are unacceptable. To maximise a SAT-solvers performance a developer needs to have maximum control over memory management and CPU usage therefore languages such as the general purpose C++ are popular with SAT-solver developers, infact most modern SAT-solvers (Cha, Berkmin et al.) are implemented in C++ which allows the use of pointers and dynamic memory management operations which are vital for fast SAT-solving. A compromise of using C++ is that it is very easy to make make mistakes such as writing buggy code which leaks memory, hence developers must take great care 42

4.2. Systematic Search

43

when implementing their SAT solvers in C++ as any bugs would prevent the solver from functioning properly. One report from the SAT sompetition 2002, stated that out of 36 solvers, 26 of them had bugs in which prevented them from functioning as they should

[40].

Languages such as Java are useful for academic demonstrations but for a practical implementation however, Java is slow and very heavy on memory usage which is not ideal for solving hard or large SAT-instances.

4.2

Systematic Search

Many of the points raised in this chapter are with reference to the ne tuning of SAT-solvers. Changes can be made to SAT-solver implementations  indepdently of the design  to increase performance.

4.2.1 Static and Dynamic Heuristics For a SAT-solver implementation to be considered ecient

and

eective it needs to

spend minimal time selecting decision variables that prune unwanted areas of the search space. Most of the solvers run-time should be spent propagating facts in the BCP algorithm, as this is how satisability of the input clause-set is decided. Computation of the branching heuristic should not outweigh the benet of the search space reduction, this is very important where ideally developers should strike a balance between pruning large areas of the search space and the computational cost of doing so. Dynamic heuristics that base their decisions only on the current state of the solving process are an eective means of selecting a decision variable. Literal counting heuristics such as DLCS work by counting occurences of literals and select a variable accordingly to induce the most unit propagations. These methods are very CPU intensive as the literal occurence statistics are required to be updated every time the solver state changes (i.e. after every unit resolution step and every backtrack). There are a number of ways the statistics can be calculated:

• Calculating literal occurences from scratch at every decsion level.

4.2. Systematic Search

44

• Incrementally updating literal counters rather than doing so all at once. For example it is much more ecient to update the counters during BCP operations, this way minimal computation has to be done when chosing the decision variable. Ultimately the heuristic requires a lot of CPU time, so is unfavourable in that respect but nevertheless produces good decions that prune large areas of the search space. When learning is added into the equation and many conict clauses of arbitary size are added, literal counting heuristics slow down a great deal such that there is no practical benet of using them. As stated previously, calculating the statistics for this heuristic comparitiviely takes much more CPU time than BCP. The problem with dynamic statistics such as DLCS is that they are paradoxically also static in that their decisions do not depend on the search history. It is more benecial to consider how the solver arrivied in its current state and make a decision based on the search history, this can be done by taking past conicting clauses into account. For example variables which are very constrained  that cause lots of conits  can be targeted and assigned prior to any other variables. This is a common heuristic used in nite domain constraint solvers. The VSIDS heuristic solves the problem of excessive computation and static decisions in that it works in conjunction with the conict analysis procedure. VSIDS is a fast and eective heuristic because the variable scores are updated independently of the current solvers state (i.e. the current truth assignment), all that has to be done before each decision is that the scores are devided by a pre-determined constant, then the variable with the higest score is chosen for branching. If this is incorporated with watched literals then no adjaceny lists have to be traversed for literal counting, hence the solvers performance greatly increases. The berkmin method of only considering literals from the most recent concit clause is apparently more eective than VSIDS

[6].

These heuristics work well on

real world structured instances as well as maintining a high performance on random 3-SAT instances

[6].walksat

With VSIDS there are still implementation issues to consider such as ordering the variables by score such that the optimal choice can be picked in linear time

4.2. Systematic Search

45

when needed. This can be done eciently using a max-heap and is essential to the ecieny of the VSIDS heuristic as performing a linear search through the variable list at each decision level negates the benet of using the VSIDS heuristic.

4.2.2 Pointer and Counter BCP It has been shown that on average over 80% of a SAT-solvers run-time is spent in unit propagation

[9],

this implies that fast, ecient unit propagation algorithms

are of great importance to SAT-solver developers. Again, similar to the heuristical decision making, BCP algorithms can either count literals  the obvious approach  or maintain a smaller set of data (2 pointers for each clause) that is quicker to update and consequently, more ecient. Adjacency lists are not ideal for use with BCP because iterating through all clauses entails a lot of CPU usage, this is exasurbated when conict clauses are learnt and added to the clause-set. Conict clauses may also be of large cardinality, possibly up to 50 literals. Although (2-)counter based BCP has limitations, several improvements can be made. The 2-counter approach  which keeps counters for keeping track of satised and unsatised literals in each clause  essentially has to traverse every clause containing the variable enqueued for unit propagation, this entails on average, traversing

lm 1 n

literals. The improved method  the 1-counter approach  keeps count of the total not-unsatised

literals in each clause and can improve upon 2-counter by a factor

of two. Only literals which become unsatised need to be visited, hence only

lm 2n

literals need to be visited, cutting the BCP time in two. Also, when backtracking, undoing variable assignments has to be considered in a similar manner

[47].

Watched literals can make further improvements for they only need to keep two pointers for each clause (excluding unit clauses), so if there exists m clauses then there are 2m watched literals. Watched literals do not use adjacency lists, instead they just need to access the clause in which a specifc watched literal appears. This can be a maximum of m clauses (the literal would be pure then as if its negation 1 Where

variables.

l is the cardinality of the clauses, m is the number of clauses and n is the number of

4.2. Systematic Search

46

appeared then there would be tautological clauses) but in practise this number will be closer to

m k

for some k , hence only a small subset of the clause-set has to be

visited.

4.2.3 Learning Schemes As previously mentioned a variety of clause learning schemes can be implemented in conjunction with conict analyis. The main questions surrounding clause learning address how comprehensive the process should be. As more conict clauses are learnt and the clause database gets larger, the solver slows down, hence there has to be a way to manage the clause-database, some of which are described below:

• Firstly, the number of clauses in the database has to be limited as for a unsatisable clause-set, thousands of conict clauses would be incrementally added to the clause database, making solving the instance almost an impossibility as memory usage would sky-rocket.

• Periodically delete all of the learnt clauses. • Delete irreleveant clauses  this requires yet more heuristics and algorithms to determine which clauses are of most benet to the solver. A heuristic can be applied which ranks the clauses in order of relevence such that clauses with a low score are removed

[9].

• Learnt clauses can be limited to a maximum size. This is of benet to the solver as larger clauses increase the run-time of counter based BCP algorithms, hence slowing the solver down. Again, as with heuristically selecting a variable, the conict analysis procedure should ideally generate a clause of benet to the solving process. The cost of generating this clause must not outweigh the search space which will be pruned as a result of the learnt clause, which means strategising the conict clause generation such that the learnt clauses will induce many conicts. Many dierent learning schemes have been developed, each have their own benets and drawbacks, some of the most popular ones include:

4.2. Systematic Search

47

• Resolve the conicting clause recursively with its antecedent clauses, working back up the search space until the clause contains only literals lower than the current decision level and the decision variable from the current level. Then backtrack to the highest decision level of the variables in the clause (excluding the decision variable which is a UIP), this makes sure that the new clause will be implied, thus the decision variable can be enqueued for unit propagation with its truth assignment ipped. This scheme is used in the rel_sat solver [51].

• Add only the decision variables involved in the conict into the new clause. However, adding all previous decision varibles into the conict clause is pointless as that space will obviously never be encountered in the search tree again.

• Make the conict clause as small as possible. This can be done by nding an edge cut of minimum size in the implication graph. In general, smaller conict clauses are more powerful, in that they will become satised or conicting with fewer variable assignments, thus enforcing more constrains on the solving process

[5].

Many more learning schemes proposed in the GRASP paper

[2].

4.2.4 Other Factors It has been shown in

[47]

that arrays and vectors give much better memory cache

performance than pointer heavy data structures such as linked lists. Memory locality is of high importance with BCP algorithms where long lists of clauses have to be visited. One disadvantage of using arrays is that the deletion of clauses  through locating the clause, deleting it and shifting back the remaining clauses by one position  becomes an expensive operation. Linked lists on the other hand allow exibility such as ease of deleting and adding new links at arbitary positions in the list. Though as previously mentioned due to performance reasons, the benets of using arrays far out weigh those of using linked lists. Clause database management which is closely linked to conict driven learning can signicantly alter the performance of a solver. The main problem entails how

4.3. Local Search

48

many learnt clauses are allowed to be stored in the database and what can the maximum length of those clauses be. These are settings which when optimised can seriously increase the performance of a solver.

4.3

Local Search

Local search algorithms work by keeping the search technique relatively simple but eective, more complex heuristics allow less computational time for ipping varaible, similarly to the situation with systematic DPLL type solvers. The main implementation issues with local search are centered around choosing the right variable to ip whilst not being too greedy and also nding a way to escape local maxima. Local search algorithms hit plateaus or local maxima because the search process is too greedy, so as the algorithm homes in on a solution there becomes an increasingly smaller number of upwards moves. There may be hundreds of local maxima scattered throughout the search space, many of which the algorithm could get stuck in. Conversly, if the algorithm does not hit a local maxima then it will very rapidly converge on a solution.

4.3.1 Escaping Local Maxima There are various ways to escape local maxima, some of which include:

• Restarting with a new try when a local maxima is encountered. • Allow the choice of sideways and upwards moves in a hope to traverse a new area of the search space.

• Introducing random noise  in the form of random ips  to the search process [49].

• Refrain from making greedy variable selections and generalise the make / break heuristic into three catogries; downwards, sideways and upwards. As there are likely to exist many variables in each category, choose one at random (from the upwards category if possible).

4.3. Local Search

49

• Advanced variable search heuristics can help, such as Tabu-search, which keeps a 'tabu' list of the most recently visited search states

[50]

and Novelty+

[46].

• Weighted clauses which attempt to ll in local maxima. At the end of each ip, if k clauses are unsatised then increment their weighting counter by a constant value. The weighting counter indicates how often the clause should be counted when determining which variable to ip. This gives a bias towards clauses with a larger weight and helps on problems where a certain sub-set of clauses are unsatised for the majority of variable assignments

[48, 49].

Any of these methods can be easily added to the standard GSAT or WalkSAT framework.

4.3.2 Performance Trade O Similarly with all SAT-solvers, there is a performance trade-o to consider when selecting variables for ipping. As previously started, with local search the idea is to keep algorithms simple and maximise the number of operations per second. One extreme algorithm could just randomly ip variables and while this does not require much computational time, it is not very eective. On the other hand, the break and make count heuristic can be used which very greedily ips the

best

variable, this however takes a lot of computational time. Striking a balance between the two is ideal which is why WalkSAT performs so well as it implements the break and make count heuristic for a subset of variables that appear in a particular clause, thus lowering the variable selection time leaving more time for ipping variables.

4.3.3 Conguration On top of variable selection heuristics, both GSAT and WalkSAT need conguring before they can begin solving. The two main parameters,

max ips

and

max tries,

along with the probability pramater (for WalkSAT) are just to name three. More complex implementations entail more settings, however the solvers for this paper will work with the three aformentioned parameters.

4.3. Local Search

50

Without the correct congurations WalkSAT performs very badly. For example on a clause-set with 100 variables, setting the max

ips

to 100 and an arbitary value

for tries will almost certainly return no solution. Usually, it is prudent to set ips

max

to 3 or 4 times the number of variables in the clause-set which has proven to be

a good estimate

[1]. Max tries

is simply used to alter the time spent searching and

the probability prameter is used to decide with what probability WalkSAT should perform a random walk.

Chapter 5 Results and Evaluation This chapter is concerned with the empirical analysis and evaluation of various SAT-solvers using the techniques explained in previous chapters.

5.1

Testing Preliminaries

Before any testing can proceed, the SAT-instances, SAT-solvers and equipment used must be claried.

5.1.1 SAT-instances Used As chosing the right SAT-instances to use is very important a well known range of clause-sets from the DIMACS benchmark suite will be used. This is benecial because DIMACS includes extensive information with respect to hardness about all of the clause-sets in their suite. To test dierent aspects of the SAT-solvers developed, dierent instances will be used:

• For BCP algorithms, pigeon hole principle (PHP) clause-sets will be used. PHP instances require a considerable amount of BCP operations and as they are all unsatisable, they will require the same number of decisions and consequently the same number of conicts. Providing variables are chosen lexographically for each solver, the test conditions will be kept as fair as possible. See

Table 5.4

for the instance statistics and BCP results. 51

5.1. Testing Preliminaries

52

Search and conict analysis test SAT-instances

Instance Vars Clauses Sat? Ratio uf75-01 uuf-75-01 uf200-01 uuf200-01 phole-9 jnh-1 jnh-310 hanoi-4 at200-99 sw100-99

75 56 200 200 90 100 100 718 600 500

325 204 860 860 415 850 900 4934 2237 3100

Yes No Yes No No Yes No Yes Yes Yes

4.33 4.33 4.30 4.30 4.61 8.50 9.00 6.87 3.72 6.20

Notes hard random 3-sat hard random 3-sat very hard random 3-sat very hard random 3-sat pigeon hole variable clause length variable clause length towers of hanoi planar graph morphed graph

Table 5.1: Search and conict analysis test SAT-instances

• For heuristics and conict analysis a range of instances will have to be used from random 3-SAT to structured problems. See

Table 5.1.

• For local search solvers the satisable instances which were used to test systematic solvers will be used, this is so a comparisson can be made between the two classes of solvers. A lot of the recently generated SAT-instances  with thousands of variables  proved too hard for this papers' solvers, so easier instances had to be used. This can only be down to the engineering of the solvers, as a great deal of development goes into producing competition standard SAT-solvers.

5.1.2 Solvers Tested The testing for systematic and local search solvers will mostly be carried out independently as it is hard to compare the radically dierent architectures, however a small series of tests will be conducted comparing their performance on a number of satisable clause-sets. Testing the systematic solvers requires the interchanging of one the three main functions; search, deduction and conict analysis whislt keeping the other two constant.

Table 5.2

shows the combinations of solvers which will be used to test and

compare the dierent function implementations.

lexographical order lexographical order lexographical order

lexographical order random DLCS DLIS RDLCS VSIDS lexographical order RDLCS

lex rand dlcs dlis rdlcs vsids lex-learn rdlcs-learn

1-counter 1-counter 1-counter 1-counter 1-counter watched literals 1-counter 1-counter

1-counter 2-counters watched literals

Branching Heuristic BCP Implementation

1-counter 2-counter watched-lits

Name

basic basic basic basic basic conict driven learning conict driven learning conict driven learning

basic basic basic

Conict Analysis

chronological backtracking chronological backtracking chronological backtracking chronological backtracking chronological backtracking non-chronological backtracking non-chronological backtracking non-chronological backtracking

chronological backtracking chronological backtracking chronological backtracking

Notes

5.1. Testing Preliminaries 53

Table 5.2: Combinations of developed DPLL based SAT-solvers to test

5.2. Results

54

Name

Framework

Selection Heuristic

gsat gsat-weighted gsat-tabu walksat

GSAT GSAT GSAT WalkSAT

make / break weighted make / break make / break with tabu search standard walksat

Table 5.3: Combinations of developed Local search SAT-solvers to test As more attention has been focused towards systematic solvers, there are fewer local search solvers to test, and due to the nature of local search, there is only really one function that can be changed  the variable selection heuristic.

Table 5.3

shows

the combinations of local search solvers to be tested. For all local search solvers

maxf lips = |V | · 3 and maxtries = maxf lips · 10. WalkSAT will perform a random walk with a probabiltiy of 0.3. All tests have a xed time limit of 15 minutes.

5.1.3 The Testing Platform The testing platform was a desktop computer with the following specications: AMD Athlon XP2100, 512MB PC333 DDR RAM on Windows XP professional using the Microsoft C++ compiler. Tests carried out on a dierent machine or using a dierent compiler will dier for obvious reasons.

5.2

See

Results

Appendix A.2

5.3

for the results tables.

Evaluation

Firstly it is worth a mention that more time was spent developing systematic SATsolvers, yet the local search SAT-solvers perform considerably better than systematic search on a particular sub-set of instances  namely, random 3-SAT  this re-enforces just how powerful the stochastic local search framework really is. Due to the nature of systematic and local search solvers it is not really feasible to compare with systematic solvers, however it is obvious through looking at the results that local

5.3. Evaluation

55

search solvers excel in nding truth assignment for random 3-SAT instances. In contrast local search seems to struggle with structured instances, often getting stuck in local maxima and not returning a satisable assignment, this was the case for all of the local search solvers. The tests were run multiple times however the solvers still failed to return a satisfying assignment although they often achieved an optium of 1 unsatised clause, but obviously this cannot constitute a satifying assignment. Regarding the diculity of the SAT-instances used, the following conclusions can be made:

• The graph colouring instances sw100 and at200 are easy for systematic SATsolvers because they contain many 2-SAT clauses, hence if good decisions are made, they should be solved quickily. However despite this, some of the local search solvers struggled to solve them.

• The uniform random 3-SAT-instances (uf / uuf) are very dicult and require an eective algorithm to solve them. they were created such that they are 50% satisable and furthermore they have a clause / variable ratio of 4.3. Many of the solvers failed to solve these instances in under the time limit of 15 minutes.

• Hanoi4 and phole9 proved dicult for all solvers. Hanoi are among the hardest instances in the DIMACS test suite1 and as mentioned in

Chapter 2,

PHP

clause-sets require long resolution refutations.

• The random variable length clause instances proved easy for all solvers, they are known to be an easy benchmark

[52].

Only a small number of instances were used for testing as some of the tests take a long time because randomised algorithms have to be run a number of times to obtain an average case performance and incidentally, most of the algorithms tested include some randomised elements. 1 Visit

http://www.intellektik.informatik.tu-darmstadt.de/SATLIB/Benchmarks/ SAT/DIMACS/HANOI/descr.html for more information.

5.3. Evaluation

56

Overall, VSIDS is shown as the best algorithm through the test results  it was the only algorithm capable of solving all SAT-instances in under the given time limit. It sports a signicant performance increase over its systematic counterparts, though local search convincinly out performs it on hard random 3-SAT. In general the following observations can be made:

• Algorithms that depend on randomised decisions are poor at solving as structured instances, however they perform well on random 3-SAT-instances.

• A solvers performance relies upon the eectiveness of the decision heuristic for the input clause-set. In this sense, there is no ideal decision heuristic.

• Stochastic local search algorithms depend

greatly

upon the ability to escape

local maxima. The following sections cover the evaluation the solvers in more detail.

5.3.1 Deduction Looking at

Table A.13

the results indicate that pointer based BCP is considerably

faster than counter based BCP. As expected, the benets of using pointers are not seen much with easier problems as the number of literals to be counted remain low. On

phole9

and

phole10

however, the speed of pointer BCP is dramatically

shown, with counter based BCP taking

much

longer to prove unsatisability of the

PHP clause-sets. These results can be generalised for performance on an arbitary SAT-instance. The solving times are abnormally long due to the lexigraphical 'heuristic' which was used in conjunction with chronological backtracking and no learning. This was to make sure that the algorithms went through exactly the same states such that the only dierence was the mechansism in which BCP was performed. Consequently, the 15 minute time limit did not apply for this test. It would have been benecial to measure the cache and memory performance of the BCP algorithms but unfortunately the complex software required to do this could not run on any computer systems available.

5.3. Evaluation

57

5.3.2 Heuristics As shown by the results, branching heuristics have a huge impact on a solvers performance. It can be easily said that the

lex

hueristic  which produces bad

results on average  is badly designed and conversely that VSIDS and DLCS are well designed as on average they tend to produce good results. Despite the obvious outcomes there are some anomolous results which need to be addressed. Firstly, the performance of VSIDS was not as good as expected. The implementation of VSIDS was not optimal, as a linear search through the variables was used instead of using a max-heap as previously discussed. This was a small detail neglected during the implementation of the vsids solver and goes to show that small engineering details make a huge of dierence in determining the performance of a SAT-solver. It is hard to compare VSIDS with other heuristics as they are inherently dierent  VSIDS requires conict driven learning and watched literals. However despite the inadequacies of my implementation, VSIDS shows a huge performance increase over literal counting heuristics. It must be appreciated that watched literals and conict driven learning give VSIDS an instant benet over literal counting heurisics and associated BCP algorithms. The naive

lexigraphical

'heuristic' denitely does not exploit the structure of

reduced SAT-instances and as can be seen, it encounters a nearly equal number of conicts as decisions  for satisable clause-sets  which shows it is a bad technique. It does however, perform well on

hanoi4

in which it solves very quickily  this must

be just a lucky variable ordering which may exploit the structure of the clause-set. This shows that if the branching heuristic is eective, the performance of the solver is

greatly

increased.

Lex

is a good example of a simple,

ecient

'heuristic' however

it certainly does not perform well on average, as an ideal a solver would incorporate a simple but (on average) long

eective

heuristic. Conversely,

lex

on

at200

takes a

time to produce a satisable assignment  reversing the variable ordering may

improve the search. The literal counting heuristics generally perform quite well over the whole range of SAT-instances used in the tests. RDLCS seems the best of the literal counting schemes as DLCS is a robust heuristic on its own, then randomisation is added in

5.3. Evaluation

58

which seems to make it more competative on random 3-SAT isntances. On the other hand, RDLCS doesn't work well on

at200, however

DLCS does, probably due to

the absence of randomisation. The literal counting heuristics are incorporated with early termination because due to the literal counting heuristics it is easy to determine if any more variable assignments are needed. If used in other solvers, the benet of early termination is outweighed by the computation needed to make the needed calculations. Despite these benets, when the hard or large clause-sets is then literal counting heuristics start to struggle as it obviously takes longer to count more literals. The decision process can be generally improved by exploiting domain dependent structures in the clause-sets. For example GSAT with clause-weighting can easily solve asymmetric graph problems which are near unsolvable by most other local search algorithms

[48].

In conclusion, the harder a SAT-instance is the more important the variable selection becomes, as if there is a 50% chance of it being satisable then the search is not biassed in either direction, thus poor decisions make little progress. If there are many satisable assignments then variable selection does not matter as much, i.e. the instance is underconstrained so decisions are less likely to cause conicts. Furthermore, simple heuristics such as

lex

and

rand

(mostly) do not perform well

on hard SAT-instances, more informed decisions are needed to eectively prune the search space.

5.3.3 Conict Driven Learning The tests indicate that conict driven learning is useful for unsatisable clause-sets in that the learnt conict clauses add more constraints to the clause-set, hence a contradiction can be reached more rapidly. Conict clauses are only useful if the part of the search space that they constrain will be visited again, this is why it is benicial to back-track up the search tree as far as possible, meaning that more of the search space will be pruned. With PHP, the solvers seem to make a whole string of assignments such they they assign all but a few of the variables and the last few variables assigned cause the conicts. The solver then has to back-track

5.3. Evaluation

59

incrementally up to near the top of the search tree. Non-chronological backtracking helps this by identifying a UIP with a low decision level which prunes many subtrees of the search space. Similarly, conict analysis is useful for satisable clause-sets by reducing the number of decisions required to nd a satisfying truth assignment. In a sense, the learnt conict clauses restrict the search space and tunnel the search in a direction leading towards a satisfying assignment. It can be seen that unstructured clause-sets such as

(u)uf200

do not benet a

huge amount from clause learning. As the whole clause-set is randomly generated, the learnt clause is unlikely to prune the search space a great deal. This can be shown by the results in that learning on hard random 3-SAT does not show a huge performance increase over solvers with no learning. The conict analysis scheme from

rel_sat

was used in the learning SAT-solvers

incorporating conict driven learning, explained in

Chapter 4 Section 4.2.3.

It gen-

erally seems to be a good methods reducing the number of decisions needed to converge on a solution as well as reducing the overall search time, this implies that the overhead of learning conict clauses does not outweigh the search space that they prune. Of course there is always room for improvement:

• The rel_sat learning scheme recursively resolves antecedent clauses, hence decision levels with a large number of unit propagations generate conict clauses that are very large, slowing down counter based BCP algorithms. This does not seem to be a problem for pointer based BCP.

• There was also only a naive clause-database management method in that the conict clauses were periodically deleted. The decision heuristic is deeply tied into the conict driven learning procedue in that if good decisions are made then minimal conicts will occur and conversely, an algorithm with a bad decision heuristic will encounter overhead due to the many (quite possibly) useless conict clauses that will be learnt. Better decisions are likely to generate more useful conict clauses because as the solver is on the right track, the conict clauses constrain the search such that it

5.3. Evaluation

60

would be dicult to veer o the optimal search path. In a sense, both mechanisisms (search and conict analysis) complement each other such that the decision heuristic chooses the right search path and the concit analyis procedure stops the search veering o a search path which leads to a satisable assignment.

5.3.4 Local Search For all varients of stochastic local search algorithms (Tables

A.9

 A.12 ) the results

seem to indicate that they are very good at nding a truth assignment if they do not get stuck in local maxima. If they do nd an assignment with not getting stuck then the search time will be much lower than the DPLL counterparts. All of the local search solvers perform very badly  in that they failed to solve  on half of the test SAT-instances. Only

gsat-tabu

solved

at200.

It is known

that stochastic local search solvers are more suited to solving random 3-SAT but it is suprising that they couldn't not solve all of the instances. Having said that, many of the systematic solvers failed to solve

hanoi4

in under 15 minutes. If the

algorithms were left long enough then they may come up with a asolution, but this is not really a practical approach. The main problem with local seach solvers, as previously mentioned, is getting stuck in local maxima which essentialy halts the search. Structured clause-sets such as graph-colouring seem to trap local search algorithms in some local maxima on every try, thus failing to give a satisable assignment when the DPLL algorithms can nd one in under a second. When local search solvers nd a satisable assignment, they usually do so very quickily, hence it seems prudent to use more complex variable selection heuristics (sacracing some of the solving speed) that employ eective local maxima avoidence strategies. Of the four local search strategies tried, WalkSAT seems the best strategy as the problem with GSAT is that it is too greedy and struggles later on during the search  unable to pass a local maxima for all tries. WalkSAT performs well because the random walk strategy manages to enable the search process to escape local maxima.

5.3. Evaluation

61

5.3.5 Other Observations Restarting the search may have helped with randomised algorithms that seem to pick a wrong decision variable and / or truth value early on in the search. Solvers incorporating learning would still benet from the learnt information before the restart was triggered. Although random restarting was mentioned previously in this paper, it was not incorporated into any of the solvers developed. The learning results were slightly dissapointing, which was most likely due to poor clause database management. The Clause database frequently gets very large during the solving process as clauses are learnt so clauses were periodically removed by deleting their two corresponding watched literal pointers from the watch list. This is a quick way of deleting clauses, however as the clauses themselves are still in memory the clause database will gradually become fragmented, assumingly lowering the cache performance of the BCP data structures. Using static arrays dened at compile time instead of dynamic data structures such as vectors may have increased performance slightly. A brief note with reference to fair testing in that there were no guarentees that CPU usage was identical or even similar for all tests. Eorts were made to try and address this however there was no software available to limit or eectively monitor CPU performance or usage.

Chapter 6 Conclusions This paper has presented a comprehensive overview of existing popular SAT-solving techniques and qualitively examined implementations of them with reference to their engineering and performance over a range of SAT-instances.

6.1

Achievements

As just stated this paper presents a comprehensive analysis of SAT-solving algorithms. Many aspects of SAT-solvers were qualitively examined which unfortunately means that none of the results can really be considered comprehensive. Due to the time constraints only a recuded number of conclusions were made, however the conclusions which were made are nevertheless signicant to the SAT-solving community. The paper did achieve its objective  an empirical analysis of SAT-solvers. Certain SAT-solving techniques have shown to be eective on particular classes of SATinstances and it it possible from the results and conclusions to present a few changes to existing SAT-solving techniques. In retrospect it would have been benecial to carry out more comprehensive tests by concentrating on one class of SAT-solver, or even one aspect of one class of SATsolver. This way a comprehensive conclusion could be made regarding a sub-set of features of the SAT-solvers that were investiagated for this paper.

62

6.1. Achievements

63

6.1.1 Importance of Decision Variables The importance of chosing the correct decision variable cannot be over-stressed as variable selection is possibly the most important part of every class of SAT-solver. If good decisons are made then less conicts will occur and the solver will rapidly converge on a solution. There can be a distinction made between randomised and deterministic heuristics:

• Deterministic heuristics such as DLCS are robust in that they will always quickily produce a solution for certain classes of SAT-instances, however as seen, they do not perform as well on random 3-SAT-instances.

• Randomisation is a very powerful technique that has been shown to eectively solve random 3-SAT-instance. Randomised heuristics are poor at solving structured SAT-isntances.

• No combination of randomised and determinism will produce a heuristic ecient at solving all classes of SAT-isntance. The performance of randomised algorithms varies greatly in that sometimes they produce a variable ordering such that an assignment is generated quickily with little or no conicts. On the other hand they could produce a problematic variable ordering, running into many thousands of conicts. One would wish to maximise the number of optimial variable orderings that produce solutions rapidly. Good approaches to designing heuristics involve the composition of randomisation with some input from a deterministic heuristic to guide the search in the right direction. Heuristics like RDLCS strike a balance between randomisation and determinism which is benecial as it enables it to tackle a wide range of SAT-instances with reasonable overall performance.

6.1.2 Emphasis on Engineering Though the experiments undertaken it has been re-enforced that SAT-solving involves engineering as much as theory. Ecient implementations of BCP such as

6.2. Further Studies

64

watched literals have shown to present huge performance increases over their literal counting counterparts  these algorithms perform exactly the same task but with dierent levels of ecieny, greatly aecting a SAT-solvers performance.

6.1.3 Domain Dependent SAT-Solving There will come a point when existing SAT-solving frameworks based on systematic and local search will reach a peak in terms of average case ecieny for a range of SAT-instances. To improve performance in the future, developers will have to concentrate on developing domain dependent extentions to SAT-solvers such that they exploit the underlying structure of the input SAT-instance. As mentioned above, variable selection heuristics are of high importance and if these heuristics  as well as conict analysis procedures  can be bespokely engineered for a particular instance, then performance will be greatly increased. As stated in the reuslts, a SAT-solvers' performance depends greatly on the type of SAT-instance it is solving. An algorithm can easily be developed to eciently solve a particular type of SAT-instance, however the trade-o is that it will almost certainly be inecient when solving all other classes of SAT-instance. The real question is,

does this actually matter ?

SAT-solvers are used in industry for a specic purposes hence they can be heavily customised for a particular domain and their inadequacies when solving other classes of SAT-instance can be disregarded.

Jack-of-all-trades

SAT-solvers such as Cha

and Berkmin do perform very well on a very wide range of SAT-instances and this is good from an academic perspective but a domain specic algorithm could out perform them both on a particular class of SAT-instance that it was bespokely engineered for.

6.2

Further Studies

Furthers studies into SAT-solving with reference to following:

Section 1.1.3

may include the

6.2. Further Studies

65

• Combine existing frameworks such as stochastic local search and systematic search to create hybrid algorithms.

• Developing genetic algorithms with crossover and mutation functions tailored to a particular class of SAT-instance.

• More emphasis on bespoke decision heuristics for a particular class of SATisntances. This would require detailed research into the structure of SATinstances for any given problem.

Bibliography [1] B. Selman, H. Kautz, and B. Cohen. Local ing.

search strategies for satisability test-

DIMACS Series in Discrete Mathematics and Theoretical Computer Science,

26:521532, 1996. [2] J. P. Marques-Silva and K. A. Sakallah. for satisability.

GRASP: A new search algorithm

In Proceedings of the ACM/IEEE International Conference on

Computer-Aided Design, pages 220227, November 1996. [3] B. Selman, H. Levesque, and D. Mitchell. isability Problems.

A New Method for Solving Hard Sat-

In Proc. of the 10th National Conference on Articial Intel-

ligence (AAAI-92), pages 440446, San Jose, CA, USA, 1992. [4] Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik.

Cha: Engineering an Ecient SAT Solver.

In Proceedings of

the 38th Design Automation Conference (DAC'01), June 2001. [5] L. Zhang, C. Madigan, M. Moskewicz, and S. Malik. learning in a boolean satisability solver.

Ecient conict driven

In Proceedings of the International

Conference on Computer Aided Design (ICCAD), San Jose, California, 11 2001. [6] I. Lynce and J. P. Marques-Silva. SAT solvers.

Ecient data structures for backtrack search

In Proceedings of the International Symposium on Theory and

Applications of Satisability Testing, pages 308315, May 2002. [7] Martin Davis, George Logemann and Donald W. Loveland. for theorem proving.

Journal of the ACM, 394397, 1962.

66

A machine program

Bibliography

67

[8] Martin Davis and Hilary Putnam. ory.

A computing procedure for quantication the-

Journal of the ACM, 201215, 1960.

[9] Niklas Eén, Niklas Sörensson.

An extensible SAT solver.

In International Con-

ference on Theory and Applications of Satisability Testing (SAT 03), (2003). [10] DIMACS Challenge Committee.

Satisability Suggested Format.

Available via

anonymous FTP from dimacs.rutgers.edu, May 1993. [11] J. P. Marques-Silva. The impact of branching heuristics in propositional satisability algorithms.

In 9th Portuguese Conference on Articial Intelligence (EPIA),

1999. [12] D. Mitchell, B. Selman, and H. Levesque. problems.

Hard and easy distributions of SAT

In Proc. 10th National Conf. on Articial Intelligence (AAAI-92),

pages 459465, San Jose, CA, July 12-17 1992. [13] Holger Hoos. for SAT.

On the run-time behaviour of stochastic local search algorithms

In Proceedings of AAAI-99, 1999.

[14] H. Zhang.

SATO: An Ecient Propositional Prover.

In W. McCune, editor,

Proceedings of the 14th Conference on Automated Deduction, LNAI 1249, pages 272275, Townsville, Australia, 1997. Springer, Berlin, Germany. [15] S.A. Cook,

The Complexity of Theorem-Proving Procedures.

In Annual ACM

Symposium on Theory of Computing, pages 151158, New York, 1971. [16] Mary Sheeran and Gunnar Stålmarck. cedure for Propositional Logic.

A tutorial on Stalmarck's Proof Pro-

In Formal Methods in Computer-Aided Design,

number 1522 in LNCS, pages 82100. [17] G. C. Tseitin.

On the complexity of derivations in propositional calculus.

In

Studies in constructive mathematics and mathematical logic, Part II. Consultants Bureau, New-York-London, 1968.

Bibliography

68

[18] Levin, L.A.

Universal Search Problems.

Problemy Peredaci Informacii 9 , pp.

115116, 1973. Translated in Problems of Information Transmission 9 , pp. 265 266. [19] A. Horn.

On sentences which are true of direct unions of algebras.

Journal of

Symbolic Logic, (16):1421, 1951. [20] C. H. Papadimitriou. stract).

On selecting a satisfying truth assignment (Extended Ab-

32nd IEEE Symposium on Foundations of Comput. Sci., 1991, pp. 163-

169. [21] A. Haken,

The intractability of resolution.

Theoretical Computer Science, vol.

39, pp. 297308, 1985. [22] Inês Lynce, Jöel Ouaknine, Sudoku as a SAT Problem. Proceedings of the Ninth International Symposium on Articial Intelligence and Mathematics (AIMATH 2006), Jan. 2006. [23] O. Dubois, P. Andre, Y. Boufkhad, and J. Carlier, rithm be ecient for solving the SAT problem.

Can a very simple algo-

In Proc. DIMACS Challenge II

Workshop, 1993. [24] E. Goldberg and Y. Novikov,

BerkMin: A Fast and Robust SAT Solver.

Design

Automation and Test in Europe (DATE) 2002, pp. 142-149. [25] S. Cook and D. Mitchell. A survey.

Finding hard instances of the satisability problem:

Proceedings of the DIMACS Workshop on Satisability Problems, To

Appear, 1997. [26] Ben-Ari, Mordechai. [27] J. Franco. problem.

Mathematical Logic for Computer Science.

Springer 2001.

On the probabilistic performances of algorithms for the satisability

Information Processing Letters, 23:103106, 1986.

[28] V. Chv'atal and E. Szemer'edi. (4) (1988), 759768.

Many hard examples for resolution.

J. ACM 35

Bibliography

69

[29] J. Gu. Ecient

local search for very large-scale satisability problems.

SIGART

Bulletin, 3:812, 1992. [30] Goldberg, A.

Average case complexity of the satisability problem.

In Proceed-

ings of the 4th Workshop on Automated Deduction Austin, Texas (1979). [31] J. Franco and M. Paull.

Probabilistic analysis of the Davis-Putnam procedure

for solving the satis ability problem.

[32] C.H. Papadimitriou.

Discrete Appl. Math., 5(1):77-87, 1983.

On selecting a satisfying truth assignment.

Proceedings of

the Conference on the Foundations of Computer Science, pages 163169, 1991. [33] W.M. Spears. A

nn algorithm for boolean satisability problems.

In Proceedings

of the 1996 International Conference on Neural Networks, pages 11211126, 1996. [34] W.M. Spears.

Simulated Annealing for hard satisability problems.

Technical

report, Naval Research Laboratory, Washington D.C., 1993. [35] Lynce, I., Baptista, L., and Marques-Silva, J. P., Algorithms for Satisability,

Stochastic Systematic Search

in the LICS Workshop on Theory and Applications

of Satisability Testing (LICS-SAT), June 2001. [36] M.F. Plass B. Aspval and R.E. Tarjan.

A linear time algorithm for testing

the truth of certain quantied boolean formulas.

Information Processing Letter,

8:121123, 1979. [37] Jan Johannsen, mated Reasoning,

The Complexity of Pure Literal Elimination, Journal of Auto-

Feb 2006, Pages 1 - 7, URL http://dx.doi.org/10.1007/s10817-

005-9008-8. [38] Hooker, J.N., Vinay, V. Branching Reasoning,

rules for satisability. Journal of Automated

1995, 15, No.3 359-383.

[39] Jeroslow, R. E. and Wang, J. Solving propositional satisability problems. Annals of mathematics and AI, 1990, 1:167-187. [40] Buro M., Kleine Buning H.: No 49, Feb 1993, 143151 .

Report on a SAT competition,

EATCS Bulletin,

Bibliography

70

[41] H. Zhang and M. E. Stickel.

An ecient algorithm for unit-propagation.

In

Proc. of AI-MATH-96, 1996. [42] Crawford, J., & Auton, L. (1993). Experimental results on the crossover point in satisability problems.

Proceedings of the 11th National Conference on Articial

Intelligence, 2127. [43] B. Selman and H. A. Kautz, ability testing,

An empirical study of greedy local search for satis-

Proc. of the 11th National Conf. on Articial Intelligence (Wash-

ington, DC), 1993, pp. 4651. [44] Alex S. Fukunaga,

Ecient Implementations of SAT local Search,

SAT 2004 

The Seventh International Conference on Theory and Applications of Satisability Testing, 10-13 May 2004, Vancouver, BC, Canada. [45] L. Sais B. Mazure and E. Gregoire. Tabu

search for SAT.

In Proceedings of the

National Conference on Arti cial Intelligence, pages 281285, 1997. [46] Chu Min Li, Wen Qi Huang, Diversication satisability,

and determinism in local search for

in Theory and Theory and Applications of Satisability Testing,

8th International conference, SAT 2005, St. Andrews, UK, June 1923. [47] L. Zhang and S. Malik,

Cache Performance of SAT Solvers: A Case Study for

Ecient Implementation of Algorithms,

Sixth International Conference on The-

ory and Applications of Satisability Testing (SAT2003), S. Margherita Ligure - Portono ( Italy), May 5-8 2003 [48] Frank, J.

Weighting for Godot: Learning heuristics for GSAT,

Proc. AAAI-96,

pp.338-343. 1996. [49] B. Selman and H. Kautz,

Domain-independent extensions to GSAT: Solving

large structured satisability problems,

Proc. of the 13th Int'l Joint Conf. on

Articial Intelligence, 1993, pp. 290295. [50] L. Sais B. Mazure and E. Gregoire. Tabu

search for SAT.

In Proceedings of the

National Conference on Articial Intelligence, pages 281285, 1997.

Bibliography

71

[51] R.J. Bayardo and R.C. Schrag. world SAT instances.

Using CSP look-back techniques to solve real-

In Proceedings, AAAI-97, 1997.

[52] B. Selman, D.G. Mitchell, and H.J. Levesque. Instances.

Generating Hard Satisability

Articial Intelligence, Vol. 81, pages 17-29, 1996.

Appendix A Additional Information A.1

Plan

The original plan is depicted in

A.2

Figure A.1.

Results

The section shows all test results in tabular form from

Instance uf75-01 uuf-75-01 uf200-01 uuf200-01 phole-9 jnh-1 jnh-310 hanoi-4 at200-99 sw100-99

Table A.1

Decisions Implications Conicts 2626 5476 4912514 8214 231 668459 2677622 69

52222 89176 52204514 157708 5449 22284846 258463645 500

2609 5477 4912515 8235 232 668447 2677578 0

Table A.1: lex results 72

to

Time 0.234 0.390 290.312 1.531 0.078 162.671 726.703 0.093

Table A.13.

A.2. Results

73

Figure A.1: GANTT Chart

A.2. Results

74

Instance uf75-01 uuf-75-01 uf200-01 uuf200-01 phole-9 jnh-1 jnh-310 hanoi-4 at200-99 sw100-99

Decisions Implications Conicts 1746 4121 1176423 6142 201 574493 2147103 69

37266 69761 9467513 937434 3993 20649372 193744193 500

1525 4003 1176322 6007 197 574126 2146632 0

Time 0.297 0.410 211.691 1.899 0.136 149.332 632.114 0.093

Table A.2: lex-learn results

Instance uf75-01 uuf-75-01 uf200-01 uuf200-01 phole-9 jnh-1 jnh-310 hanoi-4 at200-99 sw100-99

Decisions Implications Conicts 96 121 102374 476829 362879 244 47 294632 69

1462 2315 2063354 9438766 5323013 5295 801 21764920 500

84 122 100251 476132 362880 233 46 294597 0

Time 0.062 0.096 57.600 134.781 136.450 1.743 0.954 211.913 0.062

Table A.3: rand results

Instance uf75-01 uuf-75-01 uf200-01 uuf200-01 phole-9 jnh-1 jnh-310 hanoi-4 at200-99 sw100-99

Decisions Implications Conicts 144 148 121596 128929 362879 244 47 4411 169

2873 2875 4553355 4670366 5323013 5295 801 428778 500

Table A.4: dlcs results

130 149 121584 128930 362880 233 46 4362 0

Time 0.062 0.078 84.921 87.468 57.797 0.218 0.078 4.890 0.156

A.2. Results

75

Instance uf75-01 uuf-75-01 uf200-01 uuf200-01 phole-9 jnh-1 jnh-310 hanoi-4 at200-99 sw100-99

Decisions Implications Conicts 158 328 629662 631721 362879 196 77 4411 169

2965 6485 21487193 21303248 5323013 3751 1261 428778 500

143 329 629648 631722 362880 185 78 4362 0

Time 0.062 0.109 391.562 451.625 135.251 0.156 0.093 5.000

0.015

Table A.5: dlis results

Instance uf75-01 uuf-75-01 uf200-01 uuf200-01 phole-9 jnh-1 jnh-310 hanoi-4 at200-99 sw100-99

Decisions Implications Conicts 108 149 48364 128929 362879 841 47 319801 66

2198 2785 163854 4670366 5323013 16056 801 28429154 580

96 148 48351 128930 362880 824 46 319745 2

Time 0.046 0.062 38.734 84.781 58.984 0.609 0.062 295.093 0.093

Table A.6: rdlcs results

Instance uf75-01 uuf-75-01 uf200-01 uuf200-01 phole-9 jnh-1 jnh-310 hanoi-4 at200-99 sw100-99

Decisions Implications Conicts 92 133 41226 989918 294061 1204 47 246156 66

1994 2463 149612 2994631 3776412 23462 801 12946133 580

85 111 41127 989514 293887 981 31 245517 2

Table A.7: rdlcs-learn results

Time 0.326 0.558 34.661 69.800 42.772 0.910 0.203 97.602 0.093

A.2. Results

76

Instance uf75-01 uuf-75-01 uf200-01 uuf200-01 phole-9 jnh-1 jnh-310 hanoi-4 at200-99 sw100-99

Decisions Implications Conicts 35 149 66482 86571 19481 52 6 476013 1763 137

138 2785 8716439 9652137 5323013 495 49 9746833 228668 500

4 148 66002 86572 19482 12 3 475845 1694 0

Time 0.016 0.062 21.463 24.610 12.623 0.046 0.015 37.340 2.374 0.140

Table A.8: vsids results

Instance uf75-01 uf200-01 jnh-1 hanoi-4 at200-99 sw100-99

Tries Flips Flips / Second Time Notes 1 14 1 1

59 8433 182 309

1282.6 994 834.9 507.4

0.046 9.551 0.218 0.609

Failed Failed -

Table A.9: gsat results

Instance uf75-01 uf200-01 jnh-1 hanoi-4 at200-99 sw100-99

Tries Flips Flips / Second Time Notes 3 18 3 1

639 14852 1001 316

20612.9 56045.3 16145.2 2257.1

0.031 0.265 0.062 0.140

Fast Failed Failed -

Table A.10: walksat results

Instance uf75-01 uf200-01 jnh-1 hanoi-4 at200-99 sw100-99

Tries Flips Flips / Second Time Notes 3 7 -

1090 3930 -

3879 1098.38 -

Table A.11: gsat-weighted

0.281 3.578 -

Failed Failed Failed Failed

A.2. Results

77

Instance uf75-01 uf200-01 jnh-1 hanoi-4 at200-99 sw100-99

Tries Flips Flips / Second Time Notes 1 5 2 1

237 3762 768 354

2746 934 1098 916

Table A.12: gsat-tabu

0.102 4.995 3.578 0.438

Failed Failed -

3.17 3.64 4.13 4.61 5.10

30571 321992 3868493 52204514 781643631

3246 32781 378344 4912515 70872610

0.109 1.203 15.828 290.312 2462.713

0.140 1.609 21.484 340.523 2942.104

0.109 1.203 8.238 112.582 1722.417

3245 32780 378343 4912514 70872609

No No No No No

phole-6 phole-7 phole-8 phole-9 phole-10

133 204 297 415 561

Decisions Implications Conicts 1-counter 2-counter watched-lits

Instance Vars Clauses Sat? Ratio

42 56 72 90 110

BCP Performance (in seconds)

Pigeon Hole Problem Instance Properties

A.2. Results 78

Table A.13: BCP test results