# On logic, formal verification and decision procedures - Part II

This entry aims to introduce the concept of what it means for a program to “decide” or what a decision procedure is. After that, there will be an introduction to first order logic, one of the most, if not the most, fundamental theoretical concepts necessary.

# Differences between DNF and CNF

Satisfiability for a DNF formula can be verified in linear time (at least one of its conjunctions evaluates to true).

$(A \land B) \lor (C \land D); \text{satisfiable}$

Validity for a CNF formula can be verified in linear time if and only if every conjunction is valid. Given an atomic formula $$A$$, every disjunction contains both $$\neg A$$ and $$A$$ (recall that a formula is valid if and only if it is satisfiable for every interpretation $$I$$)

$(\neg A \lor A) \land (\neg C \lor C); \text{ satisfiable}$

# Tseytin transformation

One may be interested in proving $$F$$ is satisfiable by analysing $$F'$$: a possibly smaller, equisatisfiable formula. The procedures produces CNF formula at most a constant factor larger than the starting one (which has to be NNF).

## Equisatisfiability

Two formulae $$F$$ and $$F'$$ are equisatisfiable if both are satisfiable or if both are not satisfiable.

Note that equisatisfiability is a much weaker property than equivalence, two formulaes can be satisfiable for two different interpretations

# Decision procedures

Given a formula representing a scenario, one major problem of interest is to determine under which condition a formula is satisfied (i.e. evaluates to true for a given interpretation $$I$$).

## Truth-Table reconstruction

A simple algorithm is consists in reconstructing the entire truth table in a space-efficient, recursive manner:

let rec SAT F =
if F = ⊤ then true
else if F = ⊥ then false
else
let P = CHOOSE vars(F) in
(SAT F{P ↦ ⊤}) ∨ (SAT F{P ↦ ⊥})


## Propositional Resolution

This is a rule of inference, as the name suggests it is used to deduce clauses starting from a given set of premises. It works by leveraging a relatively simple property all CNF formulas in PL have:

Suppose we have

$\underbrace{(A \lor B)}_{C_1} \land \overbrace{(\neg A \lor C)}^{C_2}$

In order to satisfy both clauses $$A$$ and $$\neg A$$ can’t be taken into account (and shouldn’t), $$C_1 \setminus \{A\}$$ and $$C_2 \setminus \{\neg A\}$$ must be satisfied.

## Davis-Putnam-Logemann-Loveland algorithm (DPLL)

This algorithm is the basis of modern satisfiability procedures, it extends the algorithm illustrated before by adding optimizations

## Boolean constraint propagation (or Unit propagation)

Boolean Constraing Propagation is one of the optimizations used at each step of DPLL.