# Satisfiability Problems

## 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