Extend Clausecraft

.gitignore

@@ -1,4 +1,5 @@
 _build/
+_opam/
 *.install
 *.merlin
 *.annot
@@ -10,4 +11,4 @@ _build/
 *.a
 .opam-switch/
 .direnv/
-.DS_Store
+.DS_Store

README.md

@@ -1,27 +1,23 @@
 # Clausecraft
 
-Clausecraft is a compact OCaml SAT solver with a Sudoku encoding demo.
+Clausecraft is an OCaml SAT solver for standard DIMACS CNF files.
 
-It reads standard DIMACS CNF files and reports satisfiable or unsatisfiable results.
+It also encodes and solves standard 9 by 9 Sudoku puzzles.
 
-This supporting project shows parser design, recursive search, independent model checks, and a practical Sudoku encoding.
+## Value
 
-## First release
+Clausecraft provides a small, readable CDCL-ready solver foundation.
 
-This release implements a DIMACS parser and a DPLL solver with unit propagation.
-
-The solver selects high-occurrence variables and explores both truth values.
-
-The Sudoku encoder uses one Boolean variable for each cell and digit.
-
-The CLI reports clause counts, search statistics, and solve time.
+The project demonstrates parsing, watched-literal propagation, recursive search, model checking, and Sudoku encoding.
 
 ## Architecture
 
 - `lib/cnf.ml` parses DIMACS headers, comments, literals, and clause terminators.
-- `lib/solver.ml` performs recursive DPLL search and unit propagation.
+- `lib/solver.ml` initializes two watches per clause for each solve call.
+- The solver queues newly assigned literals and inspects only clauses watching falsified literals.
+- The solver moves watches when possible and enqueues unit literals otherwise.
 - `lib/sudoku.ml` encodes and decodes standard 9 by 9 Sudoku puzzles.
-- `bin/main.ml` exposes the `solve` and `sudoku` commands.
+- `bin/main.ml` provides the `solve` and `sudoku` commands.
 - `test/test_clausecraft.ml` checks models with an independent clause evaluator.
 
 The library keeps parsing, solving, and Sudoku concerns separate.
@@ -30,7 +26,7 @@ The library keeps parsing, solving, and Sudoku concerns separate.
 
 Use OCaml 4.14 or newer, Dune 3.14 or newer, and Opam.
 
-Install dependencies with Opam.
+Install the locked dependencies.
 
 ```sh
 opam install . --deps-only --with-test --locked
@@ -68,7 +64,7 @@ The Sudoku command prints the solved grid and solver statistics.
 
 ## Sample output
 
-The small SAT fixture produces this stable result shape:
+The SAT command prints this result shape.
 
 ```text
 variables: 3
@@ -81,38 +77,40 @@ conflicts: 0
 solve_time_ms: <machine-dependent>
 ```
 
-The time value changes with the local machine.
+The time value depends on the local machine.
 
 The Sudoku command prints nine solved rows after its result line.
 
 ## Tests and validation
 
-Each SAT test uses a separate clause evaluator.
+Tests cover parser errors, SAT, UNSAT, empty clauses, watched-literal chains, bundled files, Sudoku, and model validity.
 
-Tests cover parser errors, SAT, UNSAT, bundled files, Sudoku, and model validity.
+Each SAT test uses a separate clause evaluator.
 
 CI runs the build, test suite, and both demos on OCaml 5.2.
 
-Local status: this workspace lacks `ocamlc`, `dune`, and `opam`.
+Local validation is limited because this workspace lacks `ocamlc`, `dune`, and `opam`.
 
-No local test, typecheck, or build result is claimed.
+The available local check was `git diff --check`.
 
 ## Limitations
 
-This first release uses full clause scans during propagation.
+The solver does not yet analyze conflicts or retain learned clauses.
+
+It does not yet schedule restarts.
 
-It does not yet implement watched literals, conflict learning, or restart scheduling.
+Variable selection still scans clauses, although propagation uses watched literals.
 
 The solver targets small and educational benchmark files.
 
 The Sudoku encoder supports standard 9 by 9 puzzles only.
 
 ## Roadmap
 
-1. Add watched-literal propagation as an independent release.
-2. Add conflict analysis and learned clauses as an independent release.
-3. Add restart scheduling and a larger benchmark set as an independent release.
+1. Complete watched-literal propagation. **Complete in this release.**
+2. Add conflict analysis and learned clauses.
+3. Add restart scheduling and a larger benchmark set.
 
 ## License
 
-Clausecraft uses the MIT License.
+Clausecraft uses the MIT License.

clausecraft.opam

@@ -1,7 +1,7 @@
 opam-version: "2.0"
 synopsis: "A compact OCaml SAT solver and Sudoku encoder"
 description: """
-Clausecraft parses DIMACS CNF files, solves them with DPLL, and demonstrates Sudoku encoding.
+Clausecraft parses DIMACS CNF files, solves them with watched literals, and demonstrates Sudoku encoding.
 """
 license: "MIT"
 depends: [
@@ -12,4 +12,4 @@ depends: [
 build: [
   ["dune" "build" "-p" name "-j" jobs]
   ["dune" "runtest" "-p" name "-j" jobs] {with-test}
-]
+]

dune-project

@@ -6,8 +6,8 @@
  (name clausecraft)
  (synopsis "A compact OCaml SAT solver and Sudoku encoder")
  (description
-  "Clausecraft parses DIMACS CNF files, solves them with DPLL, and demonstrates Sudoku encoding.")
+  "Clausecraft parses DIMACS CNF files, solves them with watched literals, and demonstrates Sudoku encoding.")
  (depends
   (ocaml (>= 4.14))
   (dune (>= 3.14))
-  (alcotest :with-test)))
+  (alcotest :with-test)))

lib/solver.ml

@@ -39,6 +39,8 @@ let inspect_clause assignment clause =
     | [ literal ] -> Unit literal
     | _ -> Open
 
+(* Keep the original helper available for callers that use the inferred module interface.
+   The solver below uses watched literals for its own propagation loop. *)
 let propagate cnf assignment propagations =
   let rec pass () =
     let changed = ref false in
@@ -93,8 +95,122 @@ let solve cnf =
   let propagations = ref 0 in
   let conflicts = ref 0 in
   let statistics () = { decisions = !decisions; propagations = !propagations; conflicts = !conflicts } in
-  let rec search assignment =
-    if not (propagate cnf assignment propagations) then (
+  let clauses = Array.of_list (List.map Array.of_list cnf.Cnf.clauses) in
+  let watch_a = Array.make (Array.length clauses) 0 in
+  let watch_b = Array.make (Array.length clauses) 0 in
+  let watch_lists = Array.make (2 * cnf.Cnf.variable_count + 2) [] in
+  let initial_units = ref [] in
+  let has_empty_clause = ref false in
+  let literal_index literal =
+    let variable = abs literal in
+    (2 * variable) + if literal < 0 then 1 else 0
+  in
+  let add_watch literal clause_index =
+    let index = literal_index literal in
+    watch_lists.(index) <- clause_index :: watch_lists.(index)
+  in
+  Array.iteri
+    (fun clause_index clause ->
+      match Array.length clause with
+      | 0 -> has_empty_clause := true
+      | 1 ->
+          watch_a.(clause_index) <- 0;
+          watch_b.(clause_index) <- 0;
+          add_watch clause.(0) clause_index;
+          initial_units := clause.(0) :: !initial_units
+      | _ ->
+          watch_a.(clause_index) <- 0;
+          watch_b.(clause_index) <- 1;
+          add_watch clause.(0) clause_index;
+          add_watch clause.(1) clause_index)
+    clauses;
+  let literal_is_true assignment literal =
+    let value = assignment.(abs literal) in
+    (literal > 0 && value = 1) || (literal < 0 && value = -1)
+  in
+  let literal_is_false assignment literal =
+    let value = assignment.(abs literal) in
+    (literal > 0 && value = -1) || (literal < 0 && value = 1)
+  in
+  let propagate assignment initial_literals =
+    let pending = Queue.create () in
+    let contradiction = ref !has_empty_clause in
+    let enqueue literal =
+      let variable = abs literal in
+      let required_value = if literal > 0 then 1 else -1 in
+      match assignment.(variable) with
+      | 0 ->
+          assignment.(variable) <- required_value;
+          incr propagations;
+          Queue.add literal pending;
+          true
+      | value -> value = required_value
+    in
+    let enqueue_initial literal =
+      let variable = abs literal in
+      let required_value = if literal > 0 then 1 else -1 in
+      match assignment.(variable) with
+      | 0 ->
+          assignment.(variable) <- required_value;
+          incr propagations;
+          Queue.add literal pending
+      | value when value = required_value -> Queue.add literal pending
+      | _ -> contradiction := true
+    in
+    List.iter enqueue_initial initial_literals;
+    let process_false_literal false_literal =
+      let list_index = literal_index false_literal in
+      let rec process remaining kept =
+        match remaining with
+        | [] -> watch_lists.(list_index) <- List.rev kept
+        | clause_index :: rest ->
+            let clause = clauses.(clause_index) in
+            let first = watch_a.(clause_index) in
+            let second = watch_b.(clause_index) in
+            let false_position =
+              if clause.(first) = false_literal then Some first
+              else if clause.(second) = false_literal then Some second
+              else None
+            in
+            (match false_position with
+            | None -> process rest kept
+            | Some false_position ->
+                let other_position = if false_position = first then second else first in
+                let other_literal = clause.(other_position) in
+                if literal_is_true assignment other_literal then process rest (clause_index :: kept)
+                else
+                  let rec find_replacement position =
+                    if position >= Array.length clause then None
+                    else if position = false_position || position = other_position then
+                      find_replacement (position + 1)
+                    else if literal_is_false assignment clause.(position) then
+                      find_replacement (position + 1)
+                    else Some position
+                  in
+                  (match find_replacement 0 with
+                  | Some replacement ->
+                      if first = false_position then watch_a.(clause_index) <- replacement
+                      else watch_b.(clause_index) <- replacement;
+                      add_watch clause.(replacement) clause_index;
+                      process rest kept
+                  | None ->
+                      if literal_is_false assignment other_literal then contradiction := true
+                      else if not (enqueue other_literal) then contradiction := true;
+                      process rest (clause_index :: kept)))
+      in
+      process watch_lists.(list_index) []
+    in
+    let rec drain () =
+      if !contradiction then false
+      else if Queue.is_empty pending then true
+      else (
+        process_false_literal (- (Queue.take pending));
+        drain ())
+    in
+    drain ()
+  in
+  let rec search assignment initial_literals =
+    if not (propagate assignment initial_literals) then (
       incr conflicts;
       None)
     else
@@ -105,14 +221,15 @@ let solve cnf =
           let try_value value =
             let branch = Array.copy assignment in
             branch.(variable) <- value;
-            search branch
+            let literal = if value = 1 then variable else -variable in
+            search branch [ literal ]
           in
           match try_value 1 with
           | Some model -> Some model
           | None -> try_value (-1)
   in
   let initial = Array.make (cnf.Cnf.variable_count + 1) 0 in
-  match search initial with
+  match search initial !initial_units with
   | Some model -> Satisfiable (model, statistics ())
   | None -> Unsatisfiable (statistics ())
 
@@ -150,4 +267,4 @@ let satisfies cnf assignment =
              | Some true -> true
              | Some false | None -> false)
            clause)
-       cnf.Cnf.clauses
+       cnf.Cnf.clauses

test/test_clausecraft.ml

@@ -38,6 +38,23 @@ let test_sat_model () =
       Alcotest.(check int) "all variables receive a value" 3 (List.length model);
       Alcotest.(check bool) "statistics are available" true (stats.Solver.propagations > 0)
 
+let test_watched_literal_chain () =
+  let cnf = Cnf.parse_string "p cnf 3 3\n-1 0\n-2 0\n1 2 3 0\n" in
+  match Solver.solve cnf with
+  | Solver.Unsatisfiable _ -> Alcotest.fail "expected a satisfying assignment"
+  | Solver.Satisfiable (assignment, stats) ->
+      Alcotest.(check int) "watched propagation avoids decisions" 0 stats.Solver.decisions;
+      Alcotest.(check int) "unit chain assigns every variable" 3 stats.Solver.propagations;
+      Alcotest.(check int) "last unit receives the required value" 1 (Solver.value assignment 3);
+      Alcotest.(check bool) "watched model satisfies the CNF" true (Solver.satisfies cnf assignment)
+
+let test_empty_clause_is_unsatisfiable () =
+  let cnf = Cnf.parse_string "p cnf 0 1\n0\n" in
+  match Solver.solve cnf with
+  | Solver.Satisfiable _ -> Alcotest.fail "an empty clause cannot be satisfied"
+  | Solver.Unsatisfiable stats ->
+      Alcotest.(check bool) "empty clause reports a conflict" true (stats.Solver.conflicts > 0)
+
 let test_unsat_model () =
   let cnf = Cnf.parse_string "p cnf 1 2\n1 0\n-1 0\n" in
   match Solver.solve cnf with
@@ -93,8 +110,10 @@ let () =
           Alcotest.test_case "parses DIMACS" `Quick test_dimacs_parser;
           Alcotest.test_case "rejects malformed input" `Quick test_dimacs_errors;
           Alcotest.test_case "verifies a SAT model independently" `Quick test_sat_model;
+          Alcotest.test_case "propagates through watched literals" `Quick test_watched_literal_chain;
+          Alcotest.test_case "rejects an empty clause" `Quick test_empty_clause_is_unsatisfiable;
           Alcotest.test_case "detects UNSAT" `Quick test_unsat_model;
           Alcotest.test_case "solves bundled benchmarks" `Quick test_bundled_benchmarks;
         ] );
       ("Sudoku", [ Alcotest.test_case "encodes and solves a puzzle" `Quick test_sudoku_encoding_and_solution ]);
-    ]
+    ]