Skip to article frontmatterSkip to article content
Site not loading correctly?

This may be due to an incorrect BASE_URL configuration. See the MyST Documentation for reference.

Chapter 4: Propositional Logic - Implementation

Next Steps

This notebook covers expressions, truth tables and forward chaining. The lab notebook (Chapter 4 Lab: Propositional Logic) asks you to implement CNF conversion, resolution, backward chaining, DPLL and a Wumpus World agent.

Extension: Sudoku as SAT. Once DPLL works, a Sudoku puzzle can be encoded with one Boolean symbol Xr,c,vX_{r,c,v} per cell (r,c)(r, c) and value vv (729 symbols). The clauses say that every cell has at least one value, no cell has two values, and no value repeats in a row, column or 3×3 box; the given digits are unit clauses. A model returned by the solver is a solution.