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

1
2
3
4
5
6

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

**TODO**