WWW.DISSERTATION.XLIBX.INFO
FREE ELECTRONIC LIBRARY - Dissertations, online materials
 
<< HOME
CONTACTS



Pages:   || 2 | 3 | 4 | 5 |

«Chapter 4 Conflict-Driven Clause Learning SAT Solvers Joao Marques-Silva, Ines Lynce and Sharad Malik 4.1. Introduction One of the main reasons for ...»

-- [ Page 1 ] --

Handbook of Satisfiability 131

Armin Biere, Marijn Heule, Hans van Maaren and Toby Walsh (Eds.)

IOS Press, 2009

c 2009 Joao Marques-Silva, Ines Lynce and Sharad Malik and IOS Press. All

rights reserved.

doi:10.3233/978-1-58603-929-5-131

Chapter 4

Conflict-Driven Clause Learning

SAT Solvers

Joao Marques-Silva, Ines Lynce and Sharad Malik

4.1. Introduction

One of the main reasons for the widespread use of SAT in many applications is that Conflict-Driven Clause Learning (CDCL) Boolean Satisfiability (SAT) solvers are so effective in practice. Since their inception in the mid-90s, CDCL SAT solvers have been applied, in many cases with remarkable success, to a number of practi- cal applications. Examples of applications include hardware and software model checking, planning, equivalence checking, bioinformatics, hardware and software test pattern generation, software package dependencies, and cryptography. This chapter surveys the organization of CDCL solvers, from the original solvers that inspired modern CDCL SAT solvers, to the most recent and proven techniques.

The organization of CDCL SAT solvers is primarily inspired by DPLL solvers.

As a result, and even though the chapter is self-contained, a reasonable knowledge of the organization of DPLL is assumed. In order to offer a detailed account of CDCL SAT solvers, a number of concepts have to be introduced, which serve to formalize the operations implemented by any DPLL SAT solver.

DPLL corresponds to backtrack search, where at each step a variable and a propositional value are selected for branching purposes. With each branching step, two values can be assigned to a variable, either 0 or 1. Branching cor- responds to assigning the chosen value to the chosen variable. Afterwards, the logical consequences of each branching step are evaluated. Each time an unsat- isfied clause (i.e. a conflict) is identified, backtracking is executed. Backtracking corresponds to undoing branching steps until an unflipped branch is reached.

When both values have been assigned to the selected variable at a branching step, backtracking will undo this branching step. If for the first branching step both values have been considered, and backtracking undoes this first branching step, then the CNF formula can be declared unsatisfiable. This kind of back- tracking is called chronological backtracking. An alternative backtracking scheme is non-chronological backtracking, which is described later in this chapter. A more detailed description of the DPLL algorithm is given in Part 1, Chapter 3.

132 Chapter 4. CDCL Solvers Besides using DPLL, building a state-of-the-art CDCL SAT solver involves a

number of additional key techniques:

• Learning new clauses from conflicts during backtrack search [MSS96].

• Exploiting structure of conflicts during clause learning [MSS96].

• Using lazy data structures for the representation of formulas [MMZ+ 01].

• Branching heuristics must have low computational overhead, and must receive feedback from backtrack search [MMZ+ 01].

• Periodically restarting backtrack search [GSK98].

• Additional techniques include deletion policies for learnt clauses [GN02], the actual implementation of lazy data structures [Rya04], the organization of unit propagation [LSB05], among others.

The chapter is organized as follows. The next section introduces the notation used throughout the chapter. Afterwards, Section 4.3 summarizes the organization of modern CDCL SAT solvers. Section 4.4 details conflict analysis, the procedure used for learning new clauses. Section 4.5 outlines more recent techniques that have been shown to be effective in practice. The chapter concludes in Section 4.6 by providing a historical perspective of the work on CDCL SAT solvers.

4.2. Notation

In this chapter, propositional formulas are represented in Conjunctive Normal Form (CNF). A finite set of Boolean variables is assumed X = {x1, x2, x3,..., xn }.

A CNF formula ϕ consists of a conjunction of clauses ω, each of which consists of a disjunction of literals. A literal is either a variable xi or its complement ¬xi.

A CNF formula can also be viewed as a set of clauses, and each clause can be viewed as a set of literals. Throughout this chapter, the representation used will be clear from the context.

Example 4.2.1 (CNF Formula). An example of a CNF formula is:

–  –  –

In the context of search algorithms for SAT, variables can be assigned a logic value, either 0 or 1. Alternatively, variables may also be unassigned. Assignments to the problem variables can be defined as a function ν : X → {0, u, 1}, where u denotes an undefined value used when a variable has not been assigned a value in {0, 1}. Given an assignment ν, if all variables are assigned a value in {0, 1}, then ν is referred to as a complete assignment. Otherwise it is a partial assignment.

Assignments serve for computing the values of literals, clauses and the complete CNF formula, respectively, lν, ω ν and ϕν. A total order is defined on the possible assignments, 0 u 1. Moreover, 1 − u = u. As a result, the following Chapter 4. CDCL Solvers 133





definitions apply:

–  –  –

The assignment function ν will also be viewed as a set of tuples (xi, vi ), with vi ∈ {0, 1}. Adding a tuple (xi, vi ) to ν corresponds to assigning vi to xi, such that ν(xi ) = vi. Removing a tuple (xi, vi ) from ν, with ν(xi ) = u, corresponds to assigning u to xi.

Clauses are characterized as unsatisfied, satisfied, unit or unresolved. A clause is unsatisfied if all its literals are assigned value 0. A clause is satisfied if at least one of its literals is assigned value 1. A clause is unit if all literals but one are assigned value 0, and the remaining literal is unassigned. Finally, a clause is unresolved if it is neither unsatisfied, nor satisfied, nor unit.

A key procedure in SAT solvers is the unit clause rule [DP60]: if a clause is unit, then its sole unassigned literal must be assigned value 1 for the clause to be satisfied. The iterated application of the unit clause rule is referred to as unit propagation or Boolean constraint propagation (BCP) [ZM88]. In modern CDCL solvers, as in most implementations of DPLL, logical consequences are derived with unit propagation. Unit propagation is applied after each branching step (and also during preprocessing), and is used for identifying variables which must be assigned a specific Boolean value. If an unsatisfied clause is identified, a conflict condition is declared, and the algorithm backtracks.

In CDCL SAT solvers, each variable xi is characterized by a number of properties, including the value, the antecedent and the decision level, denoted respectively by ν(vi ) ∈ {0, u, 1}, α(xi ) ∈ ϕ ∪ {NIL}, and δ(xi ) ∈ {−1, 0, 1,..., |X|}. A variable xi that is assigned a value as the result of applying the unit clause rule is said to be implied. The unit clause ω used for implying variable xi is said to be the antecedent of xi, α(xi ) = ω. For variables that are decision variables or are unassigned, the antecedent is NIL. Hence, antecedents are only defined for variables whose value is implied by other assignments. The decision level of a variable xi denotes the depth of the decision tree at which the variable is assigned a value in {0, 1}. The decision level for an unassigned variable xi is −1, δ(xi ) = −1. The decision level associated with variables used for branching steps (i.e. decision assignments) is specified by the search process, and denotes the current depth of the decision stack. Hence, a variable xi associated with a decision assignment is characterized by having α(xi ) = NIL and δ(xi ) 0. More formally, the decision

level of xi with antecedent ω is given by:

δ(xi ) = max({0} ∪ {δ(xj ) | xj ∈ ω ∧ xj = xi }) (4.6)

i.e. the decision level of an implied literal is either the highest decision level of the implied literals in a unit clause, or it is 0 in case the clause is unit. The notation xi = v @ d is used to denote that ν(xi ) = v and δ(xi ) = d. Moreover, the decision level of a literal is defined as the decision level of its variable, δ(l) = δ(xi ) if l = xi or l = ¬xi.

134 Chapter 4. CDCL Solvers

–  –  –

Assume decision assignments x21 = 0@2 and x31 = 0@3. Moreover, assume the current decision assignment x1 = 0@5. The resulting implication graph is shown in figure 4.2, and yields a conflict because clause (x5 ∨ x6 ) becomes unsatisfied.

4.3. Organization of CDCL Solvers Algorithm 4.1 shows the standard organization of a CDCL SAT solver, which essentially follows the organization of DPLL. With respect to DPLL, the main

136 Chapter 4. CDCL Solvers

–  –  –

differences are the call to function ConflictAnalysis each time a conflict is identified, and the call to Backtrack when backtracking takes place. Moreover, the Backtrack procedure allows for backtracking non-chronologically.

In addition to the main CDCL function, the following auxiliary functions are

used:

• UnitPropagation consists of the iterated application of the unit clause rule. If an unsatisfied clause is identified, then a conflict indication is returned.

• PickBranchingVariable consists of selecting a variable to assign and the respective value.

• ConflictAnalysis consists of analyzing the most recent conflict and learning a new clause from the conflict. The organization of this procedure is described in section 4.4.

• Backtrack backtracks to the decision level computed by ConflictAnalysis.

• AllVariablesAssigned tests whether all variables have been assigned, in which case the algorithm terminates indicating that the CNF formula is satisfiable. An alternative criterion to stop execution of the algorithm is to check whether all clauses are satisfied. However, in modern SAT solvers that use lazy data structures, clause state cannot be maintained accurately, and so the termination criterion must be whether all variables are assigned.

Arguments to the auxiliary functions are assumed to be passed by reference.

Hence, ϕ and ν are supposed to be modified during execution of the auxiliary functions.

The typical CDCL algorithm shown does not account for a few often used techniques, namely search restarts [GSK98, BMS00] and implementation of clause deletion policies [GN02]. Search restarts cause the algorithm to restart itself, but already learnt clauses are kept. Clause deletion policies are used to decide learnt clauses that can be deleted. Clause deletion allows the memory usage of the SAT solver to be kept under control.

Chapter 4. CDCL Solvers 137

4.4. Conflict Analysis This section outlines the conflict analysis procedure used by modern SAT solvers.

4.4.1. Learning Clauses from Conflicts Each time the CDCL SAT solver identifies a conflict due to unit propagation, the ConflictAnalysis procedure is invoked. As a result, one or more new clauses are learnt, and a backtracking decision level is computed. The conflict analysis procedure analyzes the structure of unit propagation and decides which literals to include in the learnt clause.

The decision levels associated with assigned variables define a partial order of the variables. Starting from a given unsatisfied clause (represented in the implication graph with vertex κ), the conflict analysis procedure visits variables implied at the most recent decision level (i.e. the current largest decision level), identifies the antecedents of visited variables, and keeps from the antecedents the literals assigned at decision levels less than the most recent decision level. This process is repeated until the most recent decision variable is visited.

Let d be the current decision level, let xi be the decision variable, let ν(xi ) = v be the decision assignment, and let ωj be an unsatisfied clause identified with unit propagation. In terms of the implication graph, the conflict vertex κ is such that α(κ) = ωj. Moreover, let represent the resolution operator. For two clauses ωj and ωk, for which there is a unique variable x such that one clause has a literal x and the other has literal ¬x, ωj ωk contains all the literals of ωj and ωk with the exception of x and ¬x.

The clause learning procedure used in SAT solvers can be defined by a sequence of selective resolution operations [MSS00, BKS04], that at each step yields a new temporary clause. First, define a predicate that holds if a clause ω has an

implied literal l assigned at the current decision level d:

–  –  –

Equation (4.16) can be used for formalizing the clause learning procedure.

The first condition, i = 0, denotes the initialization step given κ in I, where all literals in the unsatisfied clause are added to the first intermediate clause clause.

Afterwards, at each step i, a literal l assigned at the current decision level d is d,i−1 selected and the intermediate clause (i.e. ωL ) is resolved with the antecedent of l.

138 Chapter 4. CDCL Solvers

–  –  –

d,i d,i−1 For an iteration i such that ωL = ωL, then a fixed point is reached, and d,i ωL ωL represents the new learnt clause. Observe that the number of resolution operations represented by (4.16) is no greater than |X|.

Modern SAT solvers implement an additional refinement of equation (4.16), by further exploiting the structure of implied assignments. This is discussed in sub-section 4.4.3.

Example 4.4.

1 (Clause Learning). Consider example 4.2.4. Applying clause learning to this example, results in the intermediate clauses shown in table 4.1.



Pages:   || 2 | 3 | 4 | 5 |


Similar works:

«CDHO Advisory | Immunosuppression COLLEGE OF DENTAL HYGIENISTS OF ONTARIO ADVISORY ADVISORY TITLE Use of the dental hygiene interventions of scaling of teeth and root planing including curetting surrounding tissue, orthodontic and restorative practices, and other invasive interventions for persons1 subject to immunosuppression. ADVISORY STATUS Cite as College of Dental Hygienists of Ontario, CDHO Advisory Immunosuppression, 2012-01-01 INTERVENTIONS AND PRACTICES CONSIDERED Scaling of teeth and...»

«U.S. Food and Drug Administration Notice: Archived Document The content in this document is provided on the FDA’s website for reference purposes only. It was current when produced, but is no longer maintained and may be outdated. Sodium Hyaluronate Ophthalmic Solution 0.18% NDA 22-358 FDA Advisory Committee Briefing Document June 2009 Dermatologic and Ophthalmic Drugs Advisory Committee Meeting Briefing Document Title: Sodium Hyaluronate Ophthalmic Solution 0.18% for the Treatment of the...»

«Etext of A Study In Scarlet, by Doyle 1 CHAPTER I. CHAPTER II. CHAPTER III. CHAPTER IV. CHAPTER V. CHAPTER VI. CHAPTER VII. CHAPTER I. CHAPTER II. CHAPTER III. CHAPTER IV. CHAPTER V. CHAPTER VI. CHAPTER VII. Etext of A Study In Scarlet, by Doyle **The Project Gutenberg Etext of A Study In Scarlet, by Doyle** Please take a look at the important information in this header. We encourage you to keep this file on your own disk, keeping an electronic path open for the next readers. Do not remove...»

«Y Myfyriwr Ymchwil Prifysgol Cymru Cyfrol 3, Rhif 1, Mai 2014, 7–17 Y Drindod Dewi Sant The Student Researcher University of Wales Vol. 3, No. 1, May 2014, 7–17 Trinity Saint David A Happy Ancient Egyptian Family?: The Bronze Statuettes of Osiris, Horus and Isis (Cyfarthfa Castle, Merthyr Tydfil: 1697.004, 1705.004, 1699.004) Karen Elliott Level 6, BA (Hons) Archaeology Crynodeb Mae’r erthygl hon yn rhoi manylion dadansoddiad ymchwil gwreiddiol i dri cherflun bach efydd o’r Hen Aifft...»

«Intraday Momentum: The First Half-Hour Return Predicts the Last Half-Hour Return∗ Lei Gao Iowa State University and Yufeng Han University of Colorado Denver and Sophia Zhengzi Li Michigan State University and Guofu Zhou Washington University in St. Louis† First Draft: March, 2014 Current Version: November, 2014 ∗ We are grateful to Campbell Harvey, Matthew Ringgenberg, Ronnie Sadka, Robert Stambaugh, seminar participants at Michigan State University, Singapore Management University,...»

«O-144-16 TRADE MARKS ACT 1994 IN THE MATTER OF TRADE MARK APPLICATION NO. 3016595 BY ANDREW JOHNSTON TO REGISTER THE TRADE MARK PANDEMONIUM DRUMMERS IN CLASS 41 AND OPPOSITION THERETO UNDER NO 401320 BY THE PANDEMONIUM DRUMMERS ASSOCIATION Background and pleadings 1. On 3 August 2013 (“the relevant date”), Andrew Johnston (“the applicant”) applied to register the trade mark PANDEMONIUM DRUMMERS (“the application”). Details of the application are as follows: Number: 3016595...»

«Build a Security Culture Kai Roer Build a Security Culture KAI ROER Every possible effort has been made to ensure that the information contained in this book is accurate at the time of going to press, and the publisher and the author cannot accept responsibility for any errors or omissions, however caused. Any opinions expressed in this book are those of the author, not the publisher. Websites identified are for reference only, not...»

«Provided by the author(s) and NUI Galway in accordance with publisher policies. Please cite the published version when available. Reinvented, Re-imagined and Somehow Dislocated: The Title Evolution of Two John McGahern Short Stories Author(s) Fahey, Fergus Publication 2008-09-03T16:03:03Z Date Publication Fahey, F., Reinvented, Re-imagined and Somehow Dislocated: Information The Evolution of Two John McGahern Short Stories (2008) Item record http://hdl.handle.net/10379/16 Downloaded...»

«A Qualitative Investigation into the Decision Making Patterns of Community Pharmacists By Brenna Whyte, M.Sc.(c) A thesis submitted in conformity with the requirements for the degree of Master of Science, Graduate Department of Pharmaceutical Sciences Leslie Dan Faculty of Pharmacy University of Toronto © Copyright by Brenna Whyte 2015 A Qualitative Investigation into the Decision Making Patterns of Pharmacists Master of Science, 2015 Graduate Department of Pharmaceutical Sciences, Leslie Dan...»

«The Occurrence and Identification of Red-necked Stint in British Columbia Rick Toochin (Revised: December 3, 2013) Introduction The first confirmed report of a Red-necked Stint (Calidris ruficollis) in British Columbia was an adult in full breeding plumage found on June 24, 1978 at Iona Island (see Table 1, confirmed records item 1). Recently another older sighting has been uncovered that fits the timing of occurrence for this species in BC and may be valid (see Table 2, hypothetical records...»

«August 2011 | Vol 2 | No 2 The Enforcement and Supervision Bulletin of the Securities Commission Malaysia Executive Summary CONTENTS 2 Corporate Governance Blueprint The SC’s commitment to fostering strong corporate governance Corporate Governance 2011 among market participants was reinforced by the launching of the Blueprint 2011 Corporate Governance Blueprint 2011 on 8 July 2011. The Blueprint, launched 3 Two directors charged for failing among others, underlines the crucial role of...»

«SPEECH BY MR. MANDLA NKOMFE, GAUTENG MEC FOR FINANCE, ON THE OCCASION TO PRESENT THE 2014/15 PROVINCIAL BUDGET, GAUTENG PROVINCIAL LEGISLATURE, 04 MARCH 2014. Honourable Speaker; Honourable Premier; Colleagues in the Executive Council; Honourable Members of this House; Heads of Departments present here today; Leaders from various sectors of our society; Fellow citizens of this great province; Madam Speaker, once more we are gathered in this esteemed House to give account of how we have fared in...»





 
<<  HOME   |    CONTACTS
2016 www.dissertation.xlibx.info - Dissertations, online materials

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.