Skip to main content

Model checking

Our goal now is to decide whether $KB \models \alpha$ for some sentence $\alpha$.

Reasoning with truth tables

Reasoning with truth tables is a form of semantic reasoning, in the sense that it directly exploits the definition of entailment: 𝛼 ⊨ 𝛽 holds when 𝛽 in every model that makes 𝛼 true.

In PL, a model is an assignment of truth values (1 or 0, true or false, 𝑇 or ⊥) to every propositional symbol that appears in 𝛼 or 𝛽 (or both)

Therefore, with 𝑛 symbols we have 2𝑛 different models, which correspond to the rows of the truth table

For every model (row), we compute the truth vales of 𝛼 and 𝛽 (by recursively computing the truth values of all the subsentences of 𝛼 and 𝛽) Then we have that 𝛼 ⊨ 𝛽 if, and only if, every model (row) that assigns 1 to 𝛼 also assigns 1 to 𝛽

Properties

This reasoning procedure is sound and complete. It always terminates, making reasoning in PL decidable.

However, it is inefficient when many propositional symbols are involved, because it has to compute a table of size 2𝑛×𝑀, where 𝑛 is the number of propositional symbols and 𝑀 is the number of subsentences the appear in the premises and the conclusion

Propositional satisfiability

Certain applications of PL require an agent to establish whether a set of sentences 𝛼 is or is not satisfiable

The problem of establishing the satisfiability of a set of propositional sentences is known as SAT Many interesting problems, including establishing propositional entailment, can be reduced to SAT

A (rather inefficient) solution of SAT is given by truth tables: 𝛼 is satisfiable if, and only if, it has truth value 1 in at least one row of its truth table

DPLL

Establish whether a set of sentences 𝛼 is or is not satisfiable

Preprocessing: convert every sentence in CNF (Conjunctive Normal Form)

Body of the procedure: from an empty assignment, incrementally try to build a model of 𝛼

  • if a model is built, 𝛼 is satisfiable
  • if the algorithm terminates without being able to build a model, 𝛼 is unsatisfiable

Conjunctive normal form (CNF)

CNF (Conjunctive Normal Form) represents a sentence as a conjunction of clauses, where a clause is a disjunction of literals and a literal is either a propositional symbol or the negation of a symbol.

Every sentence of propositional logic is logically equivalent to a conjunction of clauses.

  • 𝐴 → 𝐵 ∨ 𝐶 becomes ¬𝐴 ∨ 𝐵 ∨ 𝐶
  • 𝐶 → ¬𝐷 becomes ¬𝐶 ∨ ¬𝐷
  • (𝐴 → 𝐵 ∨ 𝐶) ∧ (𝐶 → ¬𝐷) becomes ¬𝐴, 𝐵, 𝐶 , {¬𝐶, ¬𝐷}

Unit clause: clause with only one literal; e.g., ¬𝐶, 𝐶

The steps to convert to CNF are (Consider 𝐴 ↔ (𝐵 ∨ 𝐶)):

  1. Eliminate ↔, replacing α ↔ 𝛽 with α → 𝛽 ∧ 𝛽 → α
    • (𝐴 → 𝐵 ∨ 𝐶 ) ∧ ( 𝐵 ∨ 𝐶 → 𝐴)
  2. Eliminate →, replacing α → 𝛽 with ¬α ∨ 𝛽
    • (¬𝐴 ∨ 𝐵 ∨ 𝐶) ∧ (¬ 𝐵 ∨ 𝐶 ∨ 𝐴)
  3. Move ¬ inwards using de Morgan's rules (¬ 𝛼 ∧ 𝛽 is equivalent to ¬α ∨ ¬𝛽 and ¬ 𝛼 ∨ 𝛽 is equivalent to ¬α ∧ ¬𝛽) and double-negation (¬¬𝛼 is equivalent to 𝛼)
    • (¬𝐴 ∨ 𝐵 ∨ 𝐶) ∧ ((¬𝐵 ∧ ¬𝐶) ∨ 𝐴)
  4. Apply distributivity law (∧ over ∨) and flatten
    • (¬𝐴 ∨ 𝐵 ∨ 𝐶) ∧ (¬𝐵 ∨ 𝐴) ∧ (¬𝐶 ∨ 𝐴)

DPLL algorithm

Essentially a backtracking (depth-first) search over models with some extras:

  • Early termination: stop when
    • all clauses are satisfied: (𝐴 ∨ 𝐵) ∧ (𝐴 ∨ ¬𝐶) is satisfied by {𝐴 = 1}
    • any clause is falsified: (𝐴 ∨ 𝐵) ∧ (𝐴 ∨ ¬𝐶) is falsified by {𝐴 = 0, 𝐵 = 0}
  • Pure literals: if all occurrences of a symbol in yet-unsatisfied clauses have the same sign, then give the symbol that value
    • in (𝐴 ∨ 𝐵) ∧ (𝐴 ∨ ¬𝐶) ∧ (𝐶 ∨ ¬𝐵), 𝐴 is pure and positive, so set it to true
    • if there is a model, then there is a model also with {... , 𝐴 = 1, ... }
  • Unit clauses: if a clause has a single literal, set the corresponding symbol to satisfy clause
    • in (𝐴 ∨ 𝐵) ∧ ¬𝐶, ¬𝐶 must be set to true {𝐶 = 0}

DPLL Example

Check if the set of sentences 𝛼 = {𝐴 → 𝐵 ∨ 𝐶, ¬𝐶, 𝐴 ∧ 𝐵 → 𝐷, 𝐶 → ¬𝐷} is satisfiable

Convert in CNF

  • 𝐴 → 𝐵 ∨ 𝐶 becomes ¬𝐴 ∨ 𝐵 ∨ 𝐶
  • ¬𝐶 becomes ¬𝐶
  • 𝐴 ∧ 𝐵 → 𝐷 becomes ¬𝐴 ∨ ¬𝐵 ∨ 𝐷
  • 𝐶 → ¬𝐷 becomes ¬𝐶 ∨ ¬𝐷
Assignments Clauses Rule
¬A ∨ B ∨ C, ¬C, ¬A ∨ ¬B ∨ D, ¬C ∨ ¬D unit clause ¬C
¬C ¬A ∨ B T ¬A ∨ ¬B ∨ D T pure literal ¬A
¬A T T T T early termination

Conclusion: the set of sentences 𝛼 = {𝐴 → 𝐵 ∨ 𝐶, ¬𝐶, 𝐴 ∧ 𝐵 → 𝐷, 𝐶 → ¬𝐷} is satisfiable (because it is satisfied by any complete assignment extending {¬𝐶 = 1, ¬𝐴 = 1})

Exam questions

2020 02 13 Q3

Explain the purpose and functioning of the DPLL algorithm, clarifying the meaning of the technical terms of Propositional Logic that you use in your explanation. Then describe (either in pseudocode or by a clear and unambiguous description in ordinary language) how the algorithm works. For each main step of the algorithm, provide a justification based on the laws of Propositional Logic.

Back to top