The boolean satisfiability problem (also called SAT problem) is a decision problem that asks if a proposition (in propositional logic) 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
- Convert proposition to CNF
- Brute-force resolutions by choosing any two clauses and trying to obtain a resolution from them.