From cc3a9e8fc710afa9aa8b479cc2fb66a2fa0ed17c Mon Sep 17 00:00:00 2001 From: DanieCuevas <43822444+DanielCuevas1208@users.noreply.github.com> Date: Sun, 2 Aug 2026 05:37:40 -0700 Subject: [PATCH] feat: extend clausecraft --- .gitignore | 3 +- README.md | 50 ++++++++------- clausecraft.opam | 4 +- dune-project | 4 +- lib/solver.ml | 127 +++++++++++++++++++++++++++++++++++++-- test/test_clausecraft.ml | 21 ++++++- 6 files changed, 172 insertions(+), 37 deletions(-) diff --git a/.gitignore b/.gitignore index 60d5380..996df34 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ _build/ +_opam/ *.install *.merlin *.annot @@ -10,4 +11,4 @@ _build/ *.a .opam-switch/ .direnv/ -.DS_Store \ No newline at end of file +.DS_Store diff --git a/README.md b/README.md index 2391c69..3738446 100644 --- a/README.md +++ b/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,27 +77,29 @@ conflicts: 0 solve_time_ms: ``` -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. @@ -109,10 +107,10 @@ 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. \ No newline at end of file +Clausecraft uses the MIT License. diff --git a/clausecraft.opam b/clausecraft.opam index 5f8d0e8..6fadad1 100644 --- a/clausecraft.opam +++ b/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} -] \ No newline at end of file +] diff --git a/dune-project b/dune-project index d5755fd..519ef46 100644 --- a/dune-project +++ b/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))) \ No newline at end of file + (alcotest :with-test))) diff --git a/lib/solver.ml b/lib/solver.ml index cebc44a..0be165c 100644 --- a/lib/solver.ml +++ b/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 \ No newline at end of file + cnf.Cnf.clauses diff --git a/test/test_clausecraft.ml b/test/test_clausecraft.ml index 2f5a376..0fecc31 100644 --- a/test/test_clausecraft.ml +++ b/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 ]); - ] \ No newline at end of file + ]