1. Introduction to SAT Solving

SAT was the first problem shown to be NP-complete.

• All NP problems can be reduced to SAT.
• FInding a polynomial time algorithm for SAT proves that $P=NP$.

A lot of problems can be translated into SAT, hence a lot of time and effort has gone into finding the most efficient algorithms for solving instances of SAT. Modern solvers can cope with formulas with millions of literals.

Greedy SAT Algorithm

This is an example of a greedy search algorithm:

1. Guess a variable assignment at random $P:=\top ,Q:=\perp ,R:=\perp$
2. Evaluate your guess by counting number of satisfied clauses.
3. Consider the effect of swapping a single variable from $\top$ to $\perp$ or vice-versa.
4. Update the assignment to the assignment that leads to the biggest increase in the number of satisfied clauses.
5. Repeat until no further improvements are possible.

We find that this algorithm runs in polynomial time:

• Selecting a random assignment and evaluating the ‘score’ of the assignment can both be done in linear time, $O(1)$.
• Each iteration involves evaluating at most $n$ assignments that different in a single variable, which requires at most a polynomial number of steps.
• We can never decrease ‘score’, so we iterate at most polynomial times.

This algorithm is not complete and may sometimes report unsatisfiable when it actually is. Despite this, it is a relatively quick algorithm and may be used as the first part of a SAT solver to help improve performance.

Naive Branching SAT Algorithm

As a precursor to the DPLL algorithm, this is a divide-and-conquer algorithm for SAT solving.

• The algorithm takes two inputs:
  1. A set of clauses $C$
  2. A partial assignment $U\subseteq \{\text{literals from }C\}$
• We branch of any variable $P$ appearing in $C$:
  • Choose to make $P:=\perp$ by adding $\neg P$ to $U$
  • Choose to make $P:=\top$ by adding $P$ to $U$
• We eliminate any satisfied clauses from $C$ and simplify any remaining clauses.
• The remaining set of clauses is self-similar to the original set of clauses but with one fewer variable.
• Hence we can continue by recursively calling this algorithm until either:
  • all clauses are satisfied and $C=\varnothing$
  • a conflict is detected in the partial assignment $U$