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.

Table of contents

• Differences between DNF and CNF
• Tseytin transformation
  • Equisatisfiability
• Decision procedures
  • Truth-Table reconstruction
  • Propositional Resolution
  • Davis-Putnam-Logemann-Loveland algorithm (DPLL)
  • Boolean constraint propagation (or Unit propagation)

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).

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\))

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

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.