Satisfiability Problems

Table of Contents

Boolean / Propositional Satisfiability Problem - SAT

Overview

  • Proven to be NP-Complete → verification is easy, finding solution is hard AND all NP problems are at most as difficult to solve as SAT
  • Heuristical SAT-algorithms are able to solve problem instances involving tens of thousands of variables and formulas consisting of millions of symbols.

in Conjuctive Normal Form - CNF-SAT

In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of clauses, where a clause is a disjunction of literals; otherwise put, it is an AND of ORs. 

(A + B + C)(~A + B + ~C)

Where in Boolean Logic we have + to mean OR, and "multiplication" to mean AND .

Satisfiability Modulo Theory - SMT

Overview

  • SAT problem in which the propositional variables are replacted with formulas of another mathematical theory

Algorithms

Davis–Putnam–Logemann–Loveland (DPLL)

  • Backtracking-based search algorithm for deciding the satisfiability of CNF-SAT

Algorithm

  • Enchances the basic backtracking algorithm
Splitting rule

The basic backtracking algorithm perfoms as follows:

  • Choose a literal and assign a truth value to it → simplifies the formula
  • Recursively check if the simplified formula is satisfiable