Boolean satisfiability problem

Introduction

The Boolean satisfiability problem (often abbreviated as SAT) is a decision problem regarding Boolean logic. It asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable.

A detailed visual representation of a Boolean satisfiability problem

History

The Boolean satisfiability problem has a rich history dating back to the work of George Boole in the mid-19th century. The problem was first proposed in a formal sense by Stephen Cook in his 1971 paper "The Complexity of Theorem-Proving Procedures". Cook's paper is also notable for introducing the concept of NP-completeness, and the Boolean satisfiability problem is the canonical example of an NP-complete problem.

Definition

In the Boolean satisfiability problem, the input is a Boolean expression E, which is composed of Boolean variables (x1, x2, ..., xn) combined using Boolean operators (AND, OR, NOT). The problem is to determine whether there is an assignment of TRUE or FALSE to the variables such that E evaluates to TRUE.

Complexity

The Boolean satisfiability problem is NP-complete, which means that it is among the most difficult problems in the class NP. Informally, this means that while a solution to a given instance of the problem can be checked quickly, there is no known algorithm that can solve all instances of the problem quickly (that is, in polynomial time). This is the essence of the P vs NP problem, one of the most important open questions in computer science.

Variants

There are many variants of the Boolean satisfiability problem, which differ in the types of Boolean expressions considered, and the restrictions placed on the allowed assignments. Some of the most well-known variants include:

3-SAT: In this variant, the Boolean expression is in conjunctive normal form (CNF), and each clause contains exactly three literals. Despite these restrictions, 3-SAT is still NP-complete.
MAX-SAT: In this variant, the goal is to find an assignment that maximizes the number of satisfied clauses. This problem is NP-hard, meaning that it is at least as hard as the hardest problems in NP.
XOR-SAT: In this variant, the Boolean expression is a system of XOR equations. Unlike the other variants, XOR-SAT can be solved in polynomial time.

Algorithms

Over the years, many algorithms have been proposed for solving the Boolean satisfiability problem. These algorithms can be broadly divided into two categories: exact algorithms, which find a satisfying assignment if one exists, and heuristic algorithms, which attempt to find a satisfying assignment but may fail to do so even if one exists. Some of the most well-known algorithms include:

DPLL algorithm: This is a backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form.
WalkSAT: This is a local search algorithm that starts with a random assignment and iteratively flips the value of a variable to minimize the number of unsatisfied clauses.
Survey propagation: This is a message-passing algorithm inspired by techniques from statistical physics.

Applications

The Boolean satisfiability problem has many applications in computer science and beyond. Some of the most notable applications include:

Hardware and software verification: SAT solvers are used to check the correctness of hardware and software designs.
Artificial intelligence: SAT solvers are used in planning, scheduling, and constraint satisfaction problems.
Cryptography: SAT solvers are used to attack cryptographic systems by finding satisfying assignments that correspond to cryptographic keys.