Part 1, Chapter 1: A History of Satisfiability 

John Franco
John Martin

This chapter traces the links between the notion of Satisfiability and
the attempts by mathematicians, philosophers, engineers, and
scientists over the last 2300 years to develop effective processes for
emulating human reasoning and scientific discovery, and for assisting
in the development of electronic computers and other electronic
components. Satisfiability was present implicitly in the development
of ancient logics such as Aristotle's syllogistic logic, its
extentions by the Stoics, and Lull's diagrammatic logic of the
medieval period.  From the renaissance to Boole algebraic approaches
to effective process replaced the logics of the ancients and all but
enunciated the meaning of Satisfiability for propositional logic.
Clarification of the concept is credited to Tarski in working out
necessary and sufficient conditions for "p is true" for any formula p
in first-order syntax.  At about the same time, the study of effective
process increased in importance with the resulting development of
lambda calculus, recursive function theory, and Turing machines, all
of which became the foundations of computer science and are linked to
the notion of Satisfiability. Shannon provided the link to the
computer age and Davis and Putnam directly linked Satisfiability to
automated reasoning via an algorithm which is the backbone of most
modern SAT solvers.  These events propelled the study of
Satisfiability for the next several decades, reaching "epidemic
proportions" in the 1990s and 2000s, and the chapter concludes with a
brief history of each of the major Satisfiability-related research
tracks that developed during that period.

Part 1, Chapter 2: CNF encodings 

Steve Prestwich

Before a combinatorial problem can be solved by current SAT methods,
it must usually be encoded in conjunctive normal form, which
facilitates algorithm implementation and allows a common file format
for problems.  Unfortunately there are several ways of encoding most
problems and few guidelines on how to choose among them, yet the
choice of encoding can be as important as the choice of search
algorithm.  This chapter reviews theoretical and empirical work on
encoding methods, including the use of Tseitin encodings, the encoding
of extensional and intensional constraints, the interaction between
encodings and search algorithms, and some common sources of error.
Case studies are used for illustration.

Part 1, Chapter 3: Complete Algorithms 

Adnan Darwiche
Knot Pipatsrisawat

Complete SAT algorithms form an important part of the SAT literature.
From a theoretical perspective, complete algorithms can be used as
tools for studying the complexities of different proof systems. From a
practical point of view, these algorithms form the basis for tackling SAT 
problems arising from real-world applications. The practicality of modern,
complete SAT solvers undoubtedly contributes to the growing interest
in the class of complete SAT algorithms. We review these algorithms in
this chapter, including Davis-Putnum resolution, Stalmarck's
algorithm, symbolic SAT solving, the DPLL algorithm, and modern
clause-learning SAT solvers. We also discuss the issue of certifying
the answers of modern complete SAT solvers.

Part 1, Chapter 4: Conflict-Driven Clause Learning SAT Solvers 

Joao Marques-Silva
Ines Lynce
Sharad Malik

One of the most important paradigm shifts in the use of SAT solvers
for solving industrial problems has been the introduction of clause
learning. Clause learning entails adding a new clause for each
conflict during backtrack search. This new clause prevents the same
conflict from occurring again during the search process. Moreover,
sophisticated techniques such as the identification of unique
implication points in a graph of implications, allow creating clauses
that more precisely identify the assignments responsible for
conflicts. Learned clauses often have a large number of literals. As a
result, another paradigm shift has been the development of new data
structures, namely lazy data structures, which are particularly
effective at handling large clauses. These data structures are called
lazy due to being in general unable to provide the actual status of a
clause. Efficiency concerns and the use of lazy data structures
motivated the introduction of dynamic heuristics that do not require
knowing the precise status of clauses. This chapter describes the
ingredients of conflict-driven clause learning SAT solvers, namely
conflict analysis, lazy data structures, search restarts,
conflict-driven heuristics and clause deletion strategies.

Part 1, Chapter 5: Look-Ahead Based SAT Solvers 

Marijn Heule
Hans van Maaren

The chapter on look-a-head architecture based solvers provides a state of
the art description of how heuristics, data structures and learning in
this context have evolved over the past year.
Contributions on the results of various scientific teams working with this
architecture are described and unified. It also provides insight on its
weakness when applied to a certain type of problems which are not
appropriate to solve using this architecture. It aims to describe the
complementary role of this architecture and that of conflict driven
solving mechanisms.

Part 1, Chapter 6: Incomplete Algorithms 

Henry Kautz
Ashish Sabharwal
Bart Selman

Research on incomplete algorithms for satisfiability testing lead to
some of the first scalable SAT solvers in the early 1990's. Unlike
systematic solvers often based on an exhaustive branching and
backtracking search, incomplete methods are generally based on
stochastic local search. On problems from a variety of domains, such
incomplete methods for SAT can significantly outperform DPLL-based
methods. While the early greedy algorithms already showed promise,
especially on random instances, the introduction of randomization and
so-called uphill moves during the search significantly extended the
reach of incomplete algorithms for SAT. This chapter discusses such
algorithms, along with a few key techniques that helped boost their
performance such as focusing on variables appearing in currently
unsatisfied clauses, devising methods to efficiently pull the search
out of local minima through clause re-weighting, and adaptive noise
mechanisms. The chapter also briefly discusses a formal foundation for
some of the techniques based on the discrete Lagrangian method.

Part 1, Chapter 7: Fundaments of Branching Heuristics 

Oliver Kullmann

"Search trees", "branching trees", "backtracking trees" or "enumeration trees" 
are at the heart of many (complete) approaches towards hard combinatorial 
problems, constraint problems, and, of course, SAT problems. Given many 
choices for branching, the fundamental question is how to guide the choices 
so that the resulting trees are (relatively) small. Despite (or perhaps 
because) of its apparently more narrow scope, especially in the SAT area 
several approaches from theory and applications have found together, and 
the rudiments of a theory of branching heuristics emerged. In this chapter 
the first systematic treatment is given.

So a general theory of heuristics guiding the construction of "branching trees"
is developed, ranging from a general theoretical analysis to the analysis
of the historical development of branching heuristics for SAT solvers,
and also to heuristics beyond SAT solving.

Part 1, Chapter 8: Random Satisfiability 

Dimitris Achlioptas

In the last twenty years a significant amount of effort has been devoted 
to the study of randomly generated satisfiability instances. While a 
number of generative models have been proposed, uniformly random k-CNF 
formulas are by now the dominant and most studied model. One reason for 
this is that such formulas enjoy a number of intriguing mathematical 
properties, including the following: for each k >= 3, there is a critical 
value, r_k, of the clauses-to-variables ratio, r, such that for r < r_k 
a random k-CNF formula is satisfiable with probability that tends to 
1 as n → ∞, while for r > r_k it is unsatisfiable with probability that 
tends to 1 as n → ∞. 
Algorithmically, even at densities much below r_k, no polynomial-time 
algorithm is known that can find any solution even with constant 
probability, while for all densities greater than r_k, the length of 
every resolution proof of unsatisfiability is exponential (and, thus, so 
is the running time of every DPLL-type algorithm). By now, the study of 
random k-CNF formulas has also attracted attention in areas such as  
mathematics and statistical physics and is at the center of an area of 
intense research activity. At the same time, random k-SAT instances 
are a popular benchmark for testing and tuning satisfiability 
algorithms. Indeed, some of the better practical ideas in use today come 
from insights gained by studying the performance of algorithms on them.  
We review old and recent mathematical results about random k-CNF 
formulas, demonstrating that the connection between computational 
complexity and phase transitions is both deep and highly nuanced.

Part 1, Chapter 9: Exploiting Runtime Variation in Complete Solvers 

Carla Gomes
Ashish Sabharwal

It has become well know over time that the performance of
backtrack-style complete SAT solvers can vary dramatically depending
on "little" details of the heuristics used, such as the way one
selects the next variable to branch on and in what order the possible
values are assigned to the variable. Extreme variations can result
even from simple tie breaking mechanisms necessarily employed in all
SAT solvers. The discovery of this extreme runtime variation has been
both a stumbling block and an opportunity. This chapter focuses on
providing an understanding of this intriguing phenomenon, particularly
in terms of the so-called heavy tailed nature of the runtime
distributions of systematic SAT solvers. It describes a simple formal
model based on expensive mistakes to explain runtime distributions
seen in practice, and discusses randomization and restart strategies
that can be used to effectively overcome the negative impact of heavy
tailed behavior. Finally, the chapter discusses the notion of backdoor
variables, which explain the unexpectedly short runs one also often
sees in practice.

Part 1, Chapter 10. Symmetry and Satisfiability 

Karem Sakallah

Symmetry is at once a familiar concept (we recognize it when we see it!) 
and a profoundly deep mathematical subject. At its most basic, a 
symmetry is some transformation of an object that leaves the object (or 
some aspect of the object) unchanged. For example, a square can be 
transformed in eight different ways that leave it looking exactly the 
same: the identity "do-nothing" transformation, 3 rotations, and 4 
mirror images (or reflections). In the context of decision problems, the 
presence of symmetries in a problem's search space can frustrate the 
hunt for a solution by forcing a search algorithm to fruitlessly explore 
symmetric subspaces that do not contain solutions. Recognizing that such 
symmetries exist, we can direct a search algorithm to look for solutions 
only in non-symmetric parts of the search space. In many cases, this can 
lead to significant pruning of the search space and yield solutions to 
problems which are otherwise intractable.

This chapter explores the symmetries of Boolean functions, particularly 
the symmetries of their conjunctive normal form (CNF) representations. 
Specifically, it examines what those symmetries are, how to model them 
using the mathematical language of group theory, how to derive them from 
a CNF formula, and how to utilize them to speed up CNF SAT solvers.

Part 1, Chapter 11: Minimal Unsatisfiability and Autarkies 

Oliver Kullmann
Hans Kleine Büning

Minimal unsatisfiability describes the reduced kernel of unsatisfiable formulas. 
The investigation of this property is very helpful in understanding the reasons 
for unsatisfiability as well as the behaviour of SAT-solvers and proof calculi. 
Moreover, for propositional formulas and quantified Boolean formulas the 
computational complexity of various SAT-related problems are strongly related 
to the complexity of minimal unsatisfiable formulas.

While "minimal unsatisfiability" studies the structure of problem instances
without redundancies, the study of "autarkies" considers the redundancies
themselves, in various guises related to partial assignments which satisfy 
some part of the problem instance while leaving the rest "untouched".
As it turns out, autarky theory creates many bridges to combinatorics,
algebra and logic, and the second part of this chapter provides a solid
foundation of the basic ideas and results of autarky theory: the basic
algorithmic problems, the algebra involved, and relations to various
combinatorial theories (e.g., matching theory, linear programming, graph
theory, the theory of permanents). Also the general theory of autarkies
as a kind of combinatorial "meta theory" is sketched (regarding its 
basic notions).

Part 1, Chapter 12: Worst-Case Upper Bounds 

Evgeny Dantsin
Edward Hirsch

The chapter is a survey of ideas and techniques behind satisfiability 
algorithms with the currently best asymptotic upper bounds on the 
worst-case running time. The survey also includes related 
structural-complexity topics such as Schaefer's dichotomy theorem, 
reductions between various restricted cases of SAT, the exponential time 
hypothesis, etc.

Part 1, Chapter 13: Fixed-Parameter Tractability 

Marko Samer
Stefan Szeider

Parameterized complexity is a new theoretical framework that
considers, in addition to the overall input size, the effects on
computational complexity of a secondary measurement, the
parameter. This two-dimensional viewpoint allows a fine-grained
complexity analysis that takes structural properties of problem
instances into account.  The central notion is "fixed-parameter
tractability" which refers to solvability in polynomial time for each
fixed value of the parameter such that the order of the polynomial
time bound is independent of the parameter. This chapter presents main 
concepts and recent results on the parameterized complexity of the 
satisfiability problem and it outlines fundamental algorithmic ideas 
that arise in this context. Among the parameters considered are the size 
of backdoor sets with respect to various tractable base classes and the 
treewidth of graph representations of satisfiability instances.

Part 2, Chapter 14: Bounded Model Checking 

Armin Biere

One of the most important industrial applications of SAT is currently
Bounded Model Checking (BMC). This technique is typically used for formal
hardware verification in the context of Electronic Design Automation.  But
BMC has successfully been applied to many other domains as well.  In
practice, BMC is mainly used for falsification, which is concerned with
violations of temporal properties.  In addition, a considerable part of this
chapter discusses complete extensions, including k-induction and
interpolation.  These extensions also allow to prove properties.

Part 2, Chapter 15: Planning and SAT 

Jussi Rintanen

The planning problem in Artificial Intelligence was the first application
of SAT to reasoning about transition systems and a direct precursor to 
the use of SAT in a number of other applications, including bounded 
model-checking in computer-aided verification.
This chapter presents the main ideas about encoding goal reachability
problems as a SAT problem, including parallel plans and different forms
of constraints for speeding up SAT solving, as well as algorithms
for solving the AI planning problem with a SAT solver.
Finally, more general planning problems that require the use of QBF
or other generalizations of SAT are discussed.

Part 2, Chapter 16: Software verification 

Daniel Kroening

This chapter covers an application of propositional satisfiability to
program analysis. We focus on the discovery of programming flaws in
low-level programs, such as embedded software. The loops in the program
are unwound together with a property to form a formula, which is then
converted into CNF. The method supports low-level programming constructs
such as bit-wise operators or pointer arithmetic.

Part 2, Chapter 17: Combinatorial Designs by SAT Solvers 

Hantao Zhang

The theory of combinatorial designs has always been a rich source of                                                                     
structured, parametrized families of SAT instances.  On one hand,                                                                        
design theory provides interesting problems for testing various SAT                                                                      
solvers; on the other hand, high-performance SAT solvers provide an                                                                      
alternative tool for attacking open problems in design theory, simply                                                                    
by encoding problems as propositional formulas, and then searching for                                                                   
their models using off-the-shelf general purpose SAT solvers.  This                                                                      
chapter presents several case studies of using SAT solvers to solve                                                                      
hard design theory problems, including quasigroup problems, Ramsey                                                                       
numbers, Van der Waerden numbers, covering arrays, Steiner systems,                                                                      
and Mendelsohn designs. It is shown that over a hundred of                                                                               
previously-open design theory problems were solved by SAT solvers,                                                                       
thus demonstrating the significant power of modern SAT solvers.                                                                          
Moreover, the chapter provides a list of 30 open design theory                                                                           
problems for the developers of SAT solvers to test their new ideas and                                                                   

Part 2, Chapter 18: Connections to Statistical Physics 

Fabrizio Altarelli
Remi Monasson
Guilhem Semerjian
Francesco Zamponi

This chapter surveys a part of the intense research activity that has 
been devoted by theoretical physicists to the study of randomly 
generated k-SAT instances. It can be at first sight surprising that 
there is a connection between physics and computer science. However 
low-temperature statistical mechanics concerns precisely the behaviour 
of the low-lying configurations of an energy landscape, in other words 
the optimization of a cost function. Moreover the ensemble of random 
k-SAT instances exhibit phase transitions, a phenomenon mostly studied 
in physics (think for instance at the transition between liquid and 
gaseous water). Besides the introduction of general concepts of 
statistical mechanics and their translations in computer science 
language, the chapter presents results on the location of the 
satisfiability transition, the detailed picture of the satisfiable 
regime and the various phase transitions it undergoes, and algorithmic 
issues for random k-SAT instances.

Part 2, Chapter 19: MaxSAT 

Chu Min Li
Felip Manya

MaxSAT solving is becoming a competitive generic approach for solving 
combinatorial optimization problems, partly due to the development of 
new solving techniques that have been recently incorporated into modern 
MaxSAT solvers, and to the challenge problems posed at the MaxSAT 
Evaluations. In this chapter we present the most relevant results on 
both approximate and exact MaxSAT solving, and survey in more
detail the techniques that have proven to be useful in branch and bound 
MaxSAT and Weighted MaxSAT solvers. Among such techniques, we pay 
special attention to the definition of good quality lower bounds, 
powerful inference rules, clever variable selection heuristics and 
suitable data structures. Moreover, we discuss the advantages of 
dealing with hard and soft constraints in the Partial MaxSAT formalims, 
and present a summary of the MaxSAT Evaluations that have been organized 
so far as affiliated events of the International Conference on Theory 
and Applications of Satisfiability Testing.

Part 2, Chapter 20: Model Counting 

Carla Gomes
Ashish Sabharwal
Bart Selman

Model counting, or counting the number of solutions of a propositional
formula, generalizes SAT and is the canonical #P-complete problem.
Surprisingly, model counting is hard even for some polynomial-time
solvable cases like 2-SAT and Horn-SAT. Efficient algorithms for this
problem will have a significant impact on many application areas that
are inherently beyond SAT, such as bounded-length adversarial and
contingency planning, and, perhaps most importantly, general
probabilistic inference. Model counting can be solved, in principle
and to an extent in practice, by extending the two most successful
frameworks for SAT algorithms, namely, DPLL and local search. However,
scalability and accuracy pose a substantial challenge. As a result,
several new ideas have been introduced in the last few years that go
beyond the techniques usually employed in most SAT solvers. These
include division into components, caching, compilation into normal
forms, exploitation of solution sampling methods, and certain
randomized streamlining techniques using special constraints. This
chapter discusses these techniques, exploring both exact methods as
well as fast estimation approaches, including those that provide
probabilistic or statistical guarantees on the quality of the reported
lower or upper bound on the model count.

Part 2, Chapter 21: Non-clausal SAT and ATPG 

Rolf Drechsler
Tommi Junttila
Ilkka Niemelä

When studying the propositional satisfiability problem (SAT), that is, the
problem of deciding whether a propositional formula is satisfiable, it is
typically assumed that the formula is given in the conjunctive normal form
(CNF).  Also most software tools for deciding satisfiability of a formula
(SAT solvers) assume that their input is in CNF.  An important reason for
this is that it is simpler to develop efficient data structures and
algorithms for CNF than for arbitrary formulas.  On the other hand, using
CNF makes efficient modeling of an application cumbersome.  Therefore one
often employs a more general formula representation in modeling and then
transforms the formula into CNF for SAT solvers.  Transforming a
propositional formula in CNF either increases the formula size exponentially
or requires the use of auxiliary variables, which can have an negative
effect on the performance of a SAT solver in the worst-case.  Moreover, by
translating to CNF one often loses information about the structure of the
original problem.  In this chapter we survey methods for solving
propositional satisfiability problems when the input formula is not given in
CNF but as a general formula or even more compactly as a Boolean circuit.
We show how the techniques applied in CNF level
Davis-Putnam-Loveland-Logemann algorithm generalize to Boolean circuits and
how the problem structure available in the circuit form can be exploited.
Then we consider a closely related area of automatic test pattern generation
(ATPG) for digital circuits and review classical ATPG algorithms,
formulation of ATPG as a SAT problem, and advanced techniques for SAT-based

Part 2, Chapter 22: Pseudo-Boolean and Cardinality Constraints 

Olivier Roussel
Vasco Manquinho

Pseudo-Boolean and cardinality constraints are a natural
generalization of clauses. While a clause expresses that at least
one literal must be true, a cardinality constraint expresses that
at least n literals must be true and a pseudo-Boolean
constraint states that a weighted sum of literals must be greater
than a constant. These contraints have a high expressive power,
have been intensively studied in 0/1 programming and are close
enough to the satisfiability problem to benefit from the recents
advances in this field. Besides, optimization problems are
naturally expressed in the pseudo-Boolean context.

This chapter presents the inference rules on pseudo-Boolean
constraints and demonstrates their increased inference power in
comparison with resolution. It also shows how the modern
satisfiability algorithms can be extended to deal with pseudo-Boolean

Part 2, Chapter 23: Theory of Quantified Boolean Formulas 

Hans Kleine Büning 
Uwe Bubeck

Quantified Boolean formulas (QBF) are a generalization of propositional 
formulas by allowing universal and existential quantifiers over 
variables. This enhancement makes QBF a concise and natural modeling 
language in which problems from many areas, such as planning, scheduling 
or verification, can often be encoded in a more compact way than with 
propositional formulas.

We introduce in this chapter the syntax and semantics of QBF and present 
fundamental concepts. This includes normal form transformations and 
Q-resolution, an extension of the propositional resolution calculus. In 
addition, Boolean function models are introduced to describe the 
valuation of formulas and the behavior of the quantifiers. We also 
discuss the expressive power of QBF and provide an overview of important 
complexity results. These illustrate that the greater capabilities of 
QBF lead to more complex problems, which makes it interesting to 
consider suitable subclasses of QBF. In particular, we give a detailed 
look at quantified Horn formulas (QHORN) and quantified 2-CNF (Q2-CNF).

Part 2, Chapter 24: Reasoning with Quantified Boolean Formulas 

Enrico Giunchiglia
Paolo Marin
Massimo Narizzano

The implementation of effective reasoning tools for deciding the
satisfiability of Quantified Boolean Formulas(QBFs) is an
important research issue in Artificial Intelligence and Computer
Science. Indeed, QBF solvers have already been proposed for many
reasoning tasks in knowledge representation and reasoning, in
automated planning and in formal methods for computer aided
design. Even more, since QBF reasoning is the prototypical PSPACE
problem, the reduction of many other decision problems in PSPACE are
readily available.  For these reasons, in the last few years several 
decision procedures for QBFs have been proposed and implemented, mostly
based either on search or on variable elimination, or on a combination 
of the two.

In this chapter, after a brief recap of the basic terminology and
notation about QBFs, we briefly review various applications of QBF
reasoning that have been recently proposed, and then we focus
on the description of the main approaches which are at the basis
of currently available solvers for prenex QBFs in conjunctive normal 
form (CNF). Other approaches and extensions to non prenex, non CNF QBFs 
are briefly reviewed at the end of the chapter.

Part 2, Chapter 25: SAT Techniques for Modal and Description Logics 

Roberto Sebastiani
Armando Tacchella

In the last two decades, modal and description logics have provided a
theoretical framework for important applications in many areas of
computer science. For this reason, the problem of automated reasoning
in modal and description logics has been thoroughly investigated.
In this chapter we show how efficient Boolean reasoning techniques
have been imported, used and integrated into reasoning tools for modal
and description logics.  To this extent, we focus on modal logics, and
in particular mainly on K(m).
In particular, we provide some background in modal logics; we describe
a basic theoretical framework and we present and analyze the basic
tableau-based and DPLL-based techniques; we describe optimizations and
extensions of the DPLL-based procedures; we introduce the
automata-theoretic/OBDD-based approach; finally, we present the eager

Part 2, Chapter 26: Satisfiability Modulo Theories 

Clark Barrett
Cesare Tinelli
Roberto Sebastiani
Sanjit Seshia

Applications in artificial intelligence, formal verification, and other areas
have greatly benefited from the recent advances in SAT.  It is often the case,
however, that applications in these fields require determining the 
satisfiability of formulas in more expressive logics such as first-order logic.
Also, these applications typically require not general first-order 
satisfiability, but rather satisfiability with respect to some background theory,
which fixes the interpretations of certain predicate and function symbols.

For many background theories, specialized methods yield decision procedures 
for the satisfiability of quantifier-free formulas or some subclass thereof.
Specialized decision procedures have been discovered for a long and still
growing list of theories with practical applications.  These include the theory
of equality, various theories of arithmetic, and certain theories of arrays, as
well as theories of lists, tuples, records, and bit-vectors of a fixed or
arbitrary finite size.  The research field concerned with determining the
satisfiability of formulas with respect to some background theory is called
Satisfiability Modulo Theories (SMT).

This chapter provides a brief overview of SMT together with references to the
relevant literature for a deeper study.  It begins with an overview of
techniques for solving SMT problems by encodings to SAT.  The rest of 
the chapter is mostly concerned with an alternative approach in which a SAT 
solver is integrated with a separate decision procedure (called a theory solver) 
for conjunctions of literals in the background theory.  After presenting this 
approach as a whole, the chapter provides more details on how to construct and
combine theory solvers, and discusses several extensions and enhancements.

Part 2, Chapter 27. Stochastic Boolean Satisfiability 

Stephen M. Majercik

Stochastic satisfiability (SSAT) is an extension of satisfiability (SAT) that merges 
two important areas of artificial intelligence:  logic and probabilistic reasoning.  
Initially suggested by Papadimitriou, who called it a ``game against nature'', 
SSAT is interesting both from a theoretical perspective---it is complete for PSPACE, 
an important complexity class---and from a practical perspective---a broad class of 
probabilistic planning problems can be encoded and solved as SSAT instances.  
This chapter describes SSAT and its variants, their computational complexity, 
applications of SSAT, analytical results, algorithms and empirical results, 
related work, and directions for future work.