Boolean Satisfiability Problem

The boolean satisfiability problem (also called SAT problem) is a decision problem in propositional logic that asks if a proposition or its equivalent boolean expression is satisfiable. That is, it asks if there is some configuration of boolean values that can be substituted to make the expression true. It is NP-Complete. In fact, it was the first problem proven to be NP-Complete (by the Cook–Levin theorem)

Almost all propositions are expressed in conjunctive normal form (CNF) to simplify them into a consistent form.

Naïve Satisfiability Algorithm §

1. Convert formula to CNF
2. Brute-force resolutions by choosing any two clauses and trying to obtain a resolution from them.

This algorithm will always terminate.

Horn Clause Satisfiability Algorithm §

If the problem can be converted into CNF and every clause is a Horn clause, then a faster algorithm exists:

Let $\varphi$ be the formula that we are evaluating:

1. Create a list of all atoms in $\varphi$, plus $\perp$ and $\top$
2. ‘Mark’ any occurrences of $\top$ (initially, one will be marked)
3. While there exists a definite Horn clause $H=(P_1\wedge P_2\cdots \wedge P_n)\to Q$:
   1. If $P_{1\dots n}$ are all marked and $Q$ is unmarked:
      1. Mark $Q$
4. If $\perp$ is marked, return unsatisfiable, else return satisfiable