Boolean Satisfiability Problem (SAT) is a well-known example of NP-complete problem. It is concerned with determining the satisfiability of a given boolean formula through assigning each of its component variables a truth value that would turn the formula true. Such mapping of variables to truth values is called an interpretation of a formula. As stated by the Cook-Levin theorem, the SAT problem is NP-complete, meaning that it has no known polynomial time solutions. Since it has many real-life applications, in digital circuit design testing, cryptanalysis, resource allocation among others, several optimizations have been found, aimed at providing a reasonable computing times for average cases, though worst case scenario still runs in polynomial time. Such optimization is the Davis–Putnam–Logemann–Loveland (DPLL) algorithm.
The Boolean Satisfiability Problem (SAT) is a classic example of an NP-complete problem. It involves determining the satisiabilty of a given Boolean formula through assigning truth values to its variables. Such an assignment, which maps variables to truth values, is called an interpretation of the formula.
According to the Cook–Levin theorem, SAT is NP-complete, meaning that no polynomial-time solution is currently known. Moreover, any problem part of NP-complete class is reducible to SAT, meaning that finding an optimal solution for SAT is equivalent to finding an efficient solution to any such problem. SAT has numerous practical applications, such as in digital circuit testing, cryptanalysis, and resource allocation. Several optimization techniques have been developed, which aim at providing reasonable time performance in average scenarios, even though the worst-case complexity remains exponential. Such algorithms are Davis–Putnam–Logemann–Loveland (DPLL) and conflict-driven clause learning (CDCL). This project consists of a SAT solver based on the two aforementioned algorithms.
The Davis–Putnam–Logemann–Loveland (DPLL) algorithm is based on backtracking to decide the satisfiability of Boolean formulas. It extends simple backtracking with key techniques:
- Unit clause: If a clause contains only one literal, that literal must be true.
- Pure literal elimination: If a variable appears with only one polarity (always positive or always negative), it can be assigned the same truth value and therefore satisfying all clauses containing it.
- Backtracking search: The algorithm assigns truth values to variables and backtracks when a contradiction is found.
The Conflict-Driven Clause Learning (CDCL) algorithm is an advanced version of the DPLL algorithm. Like DPLL, it assigns truth values to variables and uses unit propagation to simplify the formula. However, CDCL uses conflicts to generate new clauses (called "learned clauses") to ensure that the same conflict won't be reached again. Also, CDCL backtracks more efficiently, exactly to the point which generated the conflict.
This project represents an SAT solver, exemplified on instances of the classic 3-coloring problem. Combining both previously mentioned algorithms, this SAT solver yields much better running time compared to a simple brute force search. Though worst-case complexity remains O(2n), average cases are optimised by substantialy reducing the search space and eliminating redundant searches.