Chapter 1

Optimal Satisfiability

1.1. Introduction

Given a set of constraints defined on Boolean variables, a satisfiability problem, also called a Boolean constraint satisfaction problem, consists of deciding whether there exists an assignment of values to the variables that satisfies all the constraints (and possibly establishing such an assignment). Often, such an assignment does not exist and, in this case, it is natural to seek an assignment that satisfies a maximum number of constraints or minimizes the number of non-satisfied constraints.

An example of a Boolean constraint satisfaction problem is the problem known as Sat, which consists of deciding whether a propositional formula (expressed as a conjunction of disjunctions) is satisfiable or not. Sat was the first problem shown t o be NP-complete by Cook [COO 71] and Levin [LEV 73] and it has remained a central problem in the study of NP-hardness of optimization problems [GAR 79]. The NP-completeness of Sat asserts that no algorithm for this problem can be efficient in the worst case, under the hypothesis P ≠ NP. Nevertheless, in practice many efficient algorithms exist for solving the Sat problem.

Satisfiability problems have direct applications in various domains such as operations research, artificial intelligence and system architecture. For example, in operations research, the graph-coloring problem can be modeled as an instance of Sat. To decide whether a graph with n vertices can be colored with k colors, we consider k × n Boolean variables, xij, i = 1,…, n, j = 1,…, k, where xij takes the value true if and only if the vertex i is assigned the color j. Hoos [HOO 98] studied the effectiveness of various modelings of the graph-coloring problem as a satisfiability problem where we apply a specific local search algorithm to the instance of the obtained satisfiability problem. The Steiner tree problem, widely studied in operations research, contributes to network design and routing applications. In [JIA 95], the authors reduced this problem to a problem that consists of finding an assignment that maximizes the number of satisfied constraints. Certain scheduling problems have been solved by using modeling in terms of a satisfiability problem [CRA 94]. Testing various properties of graphs or hypergraphs is also a problem that reduces to a satisfiability problem. In artificial intelligence, an interesting application is the planning problem that can be represented as a set of constraints such that every satisfying assignment corresponds to a valid plan (see [KAU 92] for such a modeling). Other applications in artificial intelligence are: learning from examples, establishing the coherence of a system of rules of a knowledge base, and constructing inferences in a knowledge base. In the design of electrical circuits, we generally wish to construct a circuit with certain functionalities (described by a Boolean function) that satisfy various constraints justified by technological considerations of reliability or availability, such as minimizing the number of gates used, minimizing the depth of the circuit or only using certain types of gates.

Satisfiability problems also have other applications in automatic reasoning, computer vision, databases, robotics, and computer-assisted design. Gu, Purdom, Franco and Wah wrote an overview article [GU 97] that cites many applications of satisfiability problems (about 250 references).

Faced with a satisfiability problem, we can either study it from the theoretical point of view (establish its exact or approximate complexity, construct algorithms that guarantee an exact or approximate solution), or solve it from the practical point of view. Among the most effective methods for the practical solution of satisfiability problems are local search, Tabu search, and simulated annealing. For further details, refer to [GU 97] and [GEN 99], which offer a summary of the majority of practical algorithms for satisfiability problems.

In this chapter, we present the principal results of exact and approximation complexity for satisfiability problems according to the type of Boolean functions that participate in the constraints. Our goal is not to present exhaustively all the results that exist in the literature but rather to identify the most studied problems and to introduce the basic concepts and algorithms. The majority of satisfiability problems are hard. It is therefore advantageous, both from the theoretical and practical points of view, to identify some specific cases that are easier. We have chosen to present the most studied specific cases: planar instances, instances with a bounded number of occurrences of each variable, and dense instances. Several optimization problems can be modeled as a satisfiability problem with an additional global constraint on the set of feasible solutions. In particular, the MIN BISECTION problem, whose approximation complexity has not yet been established, can be modeled as a satisfiability problem where the set of feasible solutions is the set of the balanced assignments (with as many variables set to 0 as to 1). We also present a few results obtained on satisfiability problems under this global constraint.

Readers who wish to acquire a deeper knowledge of the complexity of satisfiability problems should consult the monograph by Creignou, Khanna and Sudan [CRE 01], where the proofs of the majority of important results in this domain can be found and that cover, besides the results presented here, other aspects such as counting complexity and function representation complexity, as well as other satisfiability problems. Note also that there is an electronic compendium by Crescenzi and Kann [CRE 95b], which regroups known results of approximation complexity for optimization problems, in particular for satisfiability problems.

This chapter is structured as follows. In section 1.2, we introduce the types of Boolean functions that we will use and we define the decision and optimization problems considered. In section 1.3, we study decision problems, and in section 1.4, maximization and minimization problems. We then discuss a few specific instances of satisfiability problems: planar instances (section 1.5.1), dense instances (section 1.5.2), and instances with a bounded number of occurrences of each variable (section 1.5.3). We also present the complexity of satisfiability problems when the set of feasible solutions is restricted to balanced assignments (section 1.6). We close our chapter with a brief conclusion (section 1.7).

1.2. Preliminaries

An instance of a satisfiability problem is a set of m constraints C1,…, Cm defined on a set of n variables x1,…, xn. A constraint Cj is the application of a Boolean function f: {0, 1}k → {0, 1} to a subset of variables xi1,…, xik, where i1,…, ik ∈ {1,…, n}. This constraint is also expressed as f(xi1,…, xik). An assignment xi = υi, for i = 1,…, n, where υi ∈ {0, 1}, satisfies the constraint f(xi1,…, xik) if and only if f(υi1,…, υik) = 1.

A literal is a variable xi (positive literal) or its negation (negative literal).

EXAMPLE 1.1.– A few examples of Boolean functions used to define constraints:

A constraint can also be represented as a Boolean expression that can be in various forms. An expression is in conjunctive normal form (CNF) if it is in the form c1 … cm, where each ct is a disjunctive clause, that is in the form t1 … tp, where ti, i = 1,…, p are literals. An expression is in disjunctive normal form (DNF) if it is in the form c1 … cm, where each ct is a conjunctive clause, that is in the form t1 … tp, where ti, i = 1,…, p are literals. A kCNF (or kDNF) expression is a CNF (or DNF) expression in which each clause contains at most k literals.

Note that if each constraint of a satisfiability problem is represented by a CNF expression, the set of constraints of the problem can itself be represented by a CNF expression that corresponds to the conjunction of the previous expressions.

We consider various satisfiability problems according to the type of Boolean functions used to define the constraints. Let be a finite set of Boolean functions. A -set of constraints is a set of constraints that only use functions that belong to . An assignment satisfies an -set of constraints if and only if it satisfies each constraint in the constraint set.

1.2.1. Constraint satisfaction problems: decision and...