SAT visualiser: CNF conversion and DPLL

The exercise exam asks you to produce two written artefacts: (1) the four numbered rewriting lines that carry a sentence into conjunctive normal form, one line per step in the fixed order, and (2) a DPLL search tree with the surviving clause set written beside every node, every move labelled, and all satisfying models listed at the leaves. This tool steps both, one move at a time.

Chapter: part10.html (SAT solving and beyond)  |  Pack index: index.html

0 / 0
mode 1 toggles
mode 2 toggles
ready

Mode 1: conversion to conjunctive normal form

A literal (a symbol or a negated symbol) sits inside a clause (a disjunction of literals), and a sentence is in CNF (a conjunction of clauses) when ∧ is on the outside, ∨ on the inside, and every ¬ sits on a symbol. What earns the marks: writing the intermediate line for each step rather than jumping to the answer, because the steps are what is being assessed.

the answer as you would write it, one numbered line per step

clauses collected so far

the sentences

    the four steps, in this order and no other

    1. Eliminate ⇔: α ⇔ β becomes (α ⇒ β) ∧ (β ⇒ α)
    2. Eliminate ⇒: α ⇒ β becomes ¬α ∨ β
    3. Push ¬ inwards: ¬¬α to α; ¬(α ∨ β) to ¬α ∧ ¬β; ¬(α ∧ β) to ¬α ∨ ¬β
    4. Distribute ∨ over ∧: α ∨ (β ∧ γ) becomes (α ∨ β) ∧ (α ∨ γ)

    Step 3 cannot finish while an implication is still present, because ⇒ hides a negation you have not written down yet. Step 4 cannot start until every negation already sits on a symbol, because distribution assumes its operands are pure disjunctions and conjunctions.

    Only sentence 2 and sentence 3 of the session problem need step 3, and only sentence 4 needs step 4. A conversion in which every sentence uses every step is a sign that something has gone wrong.

    History: one row per step, which is what a full-mark answer looks like

    #sentencestepruleresult

    Mode 2: DPLL as a search tree, finding every model

    A model (a world in which every clause is true) is what a leaf reports; a symbol still unassigned at a satisfied leaf is free, and that leaf stands for two models, not one. What earns the marks: the surviving clause set beside every node with the unit clause marked. A tree of bare assignments with no clause sets is not a trace of DPLL, it is a guess that happens to be right.

    Search tree (green leaf: all clauses satisfied. red leaf: a clause is falsified)

    clause set at the current node

    Satisfied clauses are greyed (they can be ignored from here on). A literal struck through in red is dead under the current assignment: hover it for the reason. The shrinking clause is what you write beside the node in the exam.

    #clausewhat is leftstate

    Published style, unsatisfied clauses only:

    models found

    0

      rules, applied in this order at every node

      1. Early termination. All clauses satisfied: report a model, even with symbols still unassigned. Any clause falsified: dead end.
      2. PURE LITERAL (only when the toggle is on, deck p.24 puts it before the unit rule): a symbol whose occurrences in the as-yet-unsatisfied clauses all have the same sign takes that value. Ties go to the alphabetically first symbol.
      3. UNIT PROPAGATION: a clause down to one literal forces that symbol. Ties go to the first such clause in the printed order.
      4. BRANCH: no rule fires, so guess. Variable chosen alphabetically, true branch first, then false. Both children are explored.

      History: one row per node, in the order you would draw them

      #nodemovewhyclause set aftermodels

      Traces are precomputed at load and machine checked against a Python reference implementation of the same two algorithms. Sources: FAI Part 10 deck, exercise session 7 assignment and its published solutions. Every number here is the source's number.