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
//! # 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 organized 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 serialization for pre-parsed puzzles
//! - [`satcore`] - Low-level SAT solver wrapper (rustsat-glucose)
//! - [`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 (literals, constraints) in step {
//! println!(" Deduced: {:?}", literals);
//! println!(" Using: {:?}", constraints);
//! }
//! }
//! ```
//!
//! ## 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: Analyzing 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(mus) = mus_set.iter().next() {
//! println!("Deduction requires {} constraints", mus.mus_len());
//! }
//! }
//! ```
//!
//! ## Features
//!
//! - **Incremental solving**: Efficiently reuses SAT solver state
//! - **Parallel MUS computation**: Uses rayon for parallel constraint analysis
//! - **Multiple MUS algorithms**: Supports both "slice" and "cake cutting" methods
//! - **Serialization**: Save/load parsed puzzles as JSON for fast startup
//! - **HTML/SVG output**: Generate visual step-by-step explanations