1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
//! # Demystify
//!
//! A constraint satisfaction solver that provides human-readable explanations
//! for puzzle solutions. Demystify uses MUS (Minimal Unsatisfiable Subset)
//! computation to find the smallest set of constraints that justify each
//! deduction step.
//!
//! ## Overview
//!
//! Demystify works by:
//! 1. Converting puzzle definitions (in Essence Prime format) to CNF (SAT) formulas
//! 2. Finding which variable assignments can be logically deduced
//! 3. Computing minimal explanations for each deduction using MUS algorithms
//! 4. Presenting step-by-step solutions with human-readable constraint names
//!
//! ## Architecture
//!
//! The library is organised into several modules:
//!
//! - [`problem`] - Core data structures and solving logic
//! - [`problem::parse`] - Parsing Essence Prime and DIMACS files
//! - [`problem::solver`] - SAT solving and MUS computation
//! - [`problem::planner`] - Step-by-step solution planning
//! - [`problem::serialize`] - JSON serialisation for pre-parsed puzzles
//! - [`satcore`] - Low-level SAT solver wrapper (rustsat-glucose, rustsat-cadical, rustsat-batsat; wasm32 uses BatSat only)
//! - [`json`] - JSON puzzle representation utilities
//! - [`web`] - SVG/HTML output generation
//!
//! ## Basic Usage
//!
//! ```rust,no_run
//! use demystify::problem::parse::PuzzleParse;
//! use demystify::problem::solver::PuzzleSolver;
//! use demystify::problem::planner::PuzzlePlanner;
//! use std::sync::Arc;
//!
//! // Load a pre-parsed puzzle from JSON
//! let puzzle = PuzzleParse::load_from_json("sudoku.json".as_ref()).unwrap();
//! let puzzle = Arc::new(puzzle);
//!
//! // Create a solver and planner
//! let solver = PuzzleSolver::new(puzzle).unwrap();
//! let mut planner = PuzzlePlanner::new(solver);
//!
//! // Solve step by step
//! let solution = planner.quick_solve();
//! for (step_num, step) in solution.iter().enumerate() {
//! println!("Step {}:", step_num + 1);
//! for um in step {
//! println!(" Deduced: {:?}", um.lits);
//! println!(" Using: {:?}", um.constraints);
//! if let Some(name) = &um.name {
//! println!(" Technique: {}", name);
//! }
//! }
//! }
//! ```
//!
//! ## Puzzle Preparation
//!
//! Before using this library, puzzles must be prepared using the `demystify` CLI
//! with the `--save-parsed` option:
//!
//! ```bash
//! demystify --model puzzle.eprime --param instance.param --save-parsed puzzle.json
//! ```
//!
//! This converts the Essence Prime definition to a pre-parsed JSON format that
//! can be loaded quickly without requiring the Conjure toolchain.
//!
//! ## Key Types
//!
//! - [`problem::PuzVar`] - A puzzle variable (e.g., `grid[1,2]`)
//! - [`problem::PuzLit`] - A literal (variable assignment like `grid[1,2]=5`)
//! - [`problem::parse::PuzzleParse`] - A fully parsed puzzle ready for solving
//! - [`problem::solver::PuzzleSolver`] - The SAT-based constraint solver
//! - [`problem::planner::PuzzlePlanner`] - Plans solution steps with explanations
//!
//! ## Supported Puzzle Types
//!
//! Demystify supports any puzzle that can be expressed in Essence Prime, including:
//! - Sudoku and variants (Killer, Miracle, X-Sudoku)
//! - Binairo (binary puzzles)
//! - Minesweeper
//! - Star Battle
//! - Kakuro
//! - Futoshiki
//! - And many more...
//!
//! ## Example: Analysing Solution Difficulty
//!
//! ```rust,no_run
//! use demystify::problem::parse::PuzzleParse;
//! use demystify::problem::solver::PuzzleSolver;
//! use demystify::problem::planner::PuzzlePlanner;
//! use std::sync::Arc;
//!
//! let puzzle = PuzzleParse::load_from_json("puzzle.json".as_ref()).unwrap();
//! let solver = PuzzleSolver::new(Arc::new(puzzle)).unwrap();
//! let mut planner = PuzzlePlanner::new(solver);
//!
//! // Get difficulty ratings for all deductions
//! let muses = planner.all_muses_with_larger();
//! for (lit, mus_set) in muses.muses() {
//! if let Some(min_len) = mus_set.iter().map(|mc| mc.mus_len()).min() {
//! println!("Deduction requires {} constraints", min_len);
//! }
//! }
//! ```
//!
//! ## Features
//!
//! - **Incremental solving**: Efficiently reuses SAT solver state
//! - **Parallel MUS computation**: Uses rayon for parallel constraint analysis
//! - **Multiple MUS algorithms**: `Quick`, `Slice`, `Cake`, and `Dynamic` (the default); see [`problem::solver::Strategy`]
//! - **Serialisation**: Save/load parsed puzzles as JSON for fast startup
//! - **HTML/SVG output**: Generate visual step-by-step explanations
// The Conjure/Savile-Row parsing pipeline is compiled out on wasm32 (which
// loads pre-parsed JSON instead), so its helper functions are uncalled there.
// Exempt only the wasm build from dead-code checking; native builds — the
// primary target — keep full dead-code analysis.