DPLL (Propositional Logic) Sodoku Solver                            Febuary 2025

    I wrote then to help me internalise concepts I'm learning in a course on logic
    and proof (Cambridge IB 2425) and to help me learn OCaml.

    Davis-Putnam-Logeman-Loveland DPLL is a propositional logic algorithm to find
    an interpretation that satisfies an expression. For example, you might ask it to
    find an interpretation for
      (X OR Y) AND (NOT (X AND Y))
    and it might tell you that
      {X=true, Y=false} entails (X OR Y) AND (NOT (X AND Y)).

    We express a sodoku problem as a propositional logic statement of 9*9*9=729
    variables where proposition P(i,j,n) is true iff the cell with coordinates (i,j)
    holds the number n in the solution. Here i,j,n are elements of {1..9}. Then we
    ask DPLL to find a solution.

    Github

       6 . 9 | . . . | . 2 3                      6 5 9 | 7 8 1 | 4 2 3
       . . 3 | 9 6 . | . . 1                      4 2 3 | 9 6 5 | 7 8 1
       7 1 . | . . . | . 6 .                      7 1 8 | 4 3 2 | 9 6 5
       ------+-------+------                      ------+-------+------
       5 8 . | 1 . 7 | . . 4                      5 8 2 | 1 9 7 | 6 3 4
       . 4 . | . . 8 | 2 . 9      --------->      3 4 1 | 6 5 8 | 2 7 9
       9 . 6 | 3 . . | 5 . .                      9 7 6 | 3 2 4 | 5 1 8
       ------+-------+------                      ------+-------+------
       . . 4 | . 7 3 | 8 9 .                      1 6 4 | 5 7 3 | 8 9 2
       . . 5 | . . . | 3 . 7                      8 9 5 | 2 1 6 | 3 4 7
       2 . . | . 4 . | . . .                      2 3 7 | 8 4 9 | 1 5 6