# 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