1
Satisfiability Theories

After reading this chapter, you should be able to:

• Comprehend fundamental concepts of Boolean satisfiability (SAT), maximum satisfiability (MaxSAT), and MaxSAT extensions.
• Understand mainstream algorithms for solving SAT and MaxSAT problems.

1.1 Boolean Satisfiability (SAT)

A Boolean formula is a string that represents a Boolean function. A Boolean function is a function of the form: , where is a Boolean domain and is the arity of the function. Usually, and are represented by 1 and 0, respectively. A propositional Boolean formula is a Boolean formula that only contains logic operations and, or and not (sometimes called negation or complement), symbolized as , , and , respectively. Some examples of propositional Boolean formulas are listed as follows:

A propositional Boolean formula can be expressed in conjunctive normal form (CNF), also known as product of sum (POS) form. A formula in CNF consists of a conjunction (logic and) of one or more clauses. A clause is a disjunction (logic or) of one or more literals, and a literal is an occurrence of a Boolean variable or its negation. An example of a propositional Boolean formula in CNF is , which can also be represented by a set of clauses as , or an assemble of literal sets like . Usually, a CNF formula is denoted by a set of clauses, i.e., conjunction is omitted.

The problem of determining whether there exists a variable assignment that makes a propositional Boolean formula evaluate to true is called a Boolean satisfiability (SAT) problem. In other words, the SAT problem tries to find a variable assignment to a CNF formula that satisfies all the clauses in a Boolean propositional formula. If such an assignment exists, the formula is satisfiable; otherwise, the formula is unsatisfiable.

Example 1.1 is a Boolean propositional formula in CNF. This formula contains five clauses: , , , , and . The first clause contains four literals, i.e., , , , and . This formula is unsatisfiable because the last two clauses are conflicting, which means they cannot be satisfied at the same time.

SAT problem is the first known nondeterministic polynomial time (NP)-complete problem proven by Cook [1]. The proof shows how every decision problem in the complexity class NP can be reduced to the SAT problem for CNF formulas. That the SAT problem is NP-complete problem briefly means that there is no known algorithm that efficiently solves all instances of SAT, and it is generally believed that no such algorithm can exist. A class of algorithms to efficiently solve a large enough subset of SAT instances is called SAT solver. Extending the capabilities of SAT solving algorithms is an ongoing area of progress. However, no current such methods can efficiently solve all SAT instances.

In the last century, showing that a certain problem is as hard as SAT was the end of the story and trying to solve it directly seemed to be hopeless. With the significant progress made in SAT solving, it is now widely accepted that being able to encode a problem into SAT is highly likely to lead to a practical solution. This "SAT Revolution" started at the end of the last century and continues to produce amazing new practical and theoretical results [2].

Examples of SAT applications include software verification [3, 4], bounded model checking [5, 6], artificial intelligence (AI) planning [7, 8], cryptographic attacks [9-13], scheduling [14-17], etc. These applications rely on the ability of SAT solvers to determine whether there exists an assignment that makes a given Boolean formula evaluate to true and return one satisfying assignment if the formula is satisfiable. It is noticeable that there are applications that require enumerating all the satisfying assignments. For example, in frequent itemset mining, it is necessary to generate all sets of items with high support from a given transaction database [18]. This opens up a new variant of SAT, called all solutions SAT (AllSAT). Solving an AllSAT problem aims to enumerate all satisfying assignments if a given CNF formula is satisfiable. Readers may refer to [19] for major techniques of ALLSAT solvers.

1.2 Maximum Satisfiability (MaxSAT)

Given a Boolean propositional formula, if it is unsatisfiable, SAT solvers only report that no solution exists, without any information on unsatisfiable instances. However, assignments violating a minimum number of constraints, or satisfying all the compulsory (hard) constraints and as many optional (soft) constraints as possible, can be considered as acceptable solutions in real-life scenarios. To cope with this limitation of SAT, maximum satisfiability (MaxSAT) and its extensions, such as partial MaxSAT and weighted MaxSAT, are becoming an alternative for representing and efficiently solving over-constrained problems [2].

The MaxSAT problem for a CNF formula is the problem of finding a variable assignment that maximizes the number of satisfied clauses. MaxSAT is often used to mean MinUNSAT because finding an assignment that maximizes the number of satisfied clauses is equivalent to finding an assignment that minimizes the number of unsatisfied clauses. MaxSAT is useful to measure the extent of unsatisfiability of a CNF formula.

Three extensions of MaxSAT are more well suited for representing and solving over-constrained problems: partial MaxSAT, weighted MaxSAT, and weighted partial MaxSAT (WPM).

In a partial MaxSAT instance, each clause is labeled either hard or soft. The hard clauses must be obligatorily satisfied, while the soft clauses can be unsatisfied. The goal of solving the partial MaxSAT instance is to satisfy all hard clauses and the maximal number of soft clause. The partial MaxSAT problem is easily extended to a SAT problem if all the clauses are hard, and a MaxSAT problem if all the clauses are soft.

Example 1.2 Given a partial MaxSAT instance , the first and second clause, enclosed by "," are hard clauses, and the third clause, enclosed by "," is a soft clause. To satisfy the hard clauses, and are forced to be 1 and 0, respectively. Based on the assignment of and , the true assignment of has to be 1 so that the soft clause can be satisfied.

A weighted MaxSAT instance is expressed in weighted CNF, where each clause is assigned a positive integer. The problem is to find a truth assignment that maximizes the sum of weights of satisfied clauses. In a special case, if the weights of all the clauses in weighted MaxSAT are equal to one, the problem is regarded as a MaxSAT problem.

Example 1.3 A weighted MaxSAT instance has three weighed clauses holding weights 2, 3, 4, respectively. All of the three clauses can be satisfied by assigning 1, 0, 1 to , , , respectively, which leads to the maximal sum of weights of satisfied clauses.

The WPM is the combination of partial MaxSAT and WPM. A WPM instance distinguishes hard and soft clauses, where each soft clause is assigned a positive integer. Solving the WPM instance is to satisfy all hard clauses and maximize the sum of weights of satisfied soft clauses. The definition of WPM can be easily extended to partial MaxSAT, where all soft clauses have weight 1, and weighted MaxSAT, where no clauses are hard.

Example 1.4 Given a WPM instance , the first and second clause, enclosed by "," are hard clauses, while the third and fourth clauses, enclosed by "," are soft clauses. To satisfy the hard clauses, and are forced to be 1 and 0, respectively. Based on the assignment of and , the true assignment of is preferred to be 0 so that the weight 7 can be earned, which is larger than the other case that the gain is merely 2.

Many important problems can be naturally expressed as MaxSAT, including academic problems such as Max-Cut or Max-Clique, as well as problems from many industrial domains. Concrete examples include the following domains: routing problems [20], hardware debugging [21-23], software debugging [24, 25], scheduling [17,26-28], planning [29-32], coalitional games [33-37], etc. Additionally, many problems originally formulated in other optimization frameworks can be easily reformulated as MaxSAT, such as the Pseudo-Boolean Optimization framework [38], the Weighted Constraint Satisfaction Problem (WCSP) framework [39], and the MaxSMT framework [40]. Readers may refer [41] for more traditional applications of MaxSAT.

1.3 Satisfiability Algorithms

The last two decades have witnessed significant progress in the development of theoretical, logical and algorithmic aspects of SAT and MaxSAT solving techniques. Moreover, the SAT competition1 (starting from 2002), MaxSAT evaluation2 (starting from 2006), and the international conference on theory and applications of satisfiability testing3 (first held in 1996) jointly play as a driving force for motivating the development of novel SAT and MaxSAT technologies.

1.3.1 SAT Algorithms

Algorithms for solving the SAT problem are mainly based on incomplete algorithms and complete algorithms. Incomplete algorithms (e.g., GSAT...