From 598bafe4217bd00887f603bf6218f19b1f779310 Mon Sep 17 00:00:00 2001 From: Ben Moss Date: Thu, 14 May 2026 15:33:12 -0400 Subject: [PATCH 1/5] feat(examples): add sudoku example with DigitSet VersionSet type --- examples/sudoku.rs | 44 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 examples/sudoku.rs diff --git a/examples/sudoku.rs b/examples/sudoku.rs new file mode 100644 index 0000000..9d0e37b --- /dev/null +++ b/examples/sudoku.rs @@ -0,0 +1,44 @@ +use std::fmt::{self, Display}; + +use resolvo::utils::{Pool, VersionSet}; + +/// A set of digits 1-9 represented as a bitmask. +#[derive(Clone, Eq, PartialEq, Hash, Debug)] +struct DigitSet(u16); + +impl DigitSet { + fn all() -> Self { + DigitSet(0b1111111110) // bits 1-9 set + } + + fn singleton(digit: u8) -> Self { + DigitSet(1 << digit) + } + + fn contains(&self, digit: u8) -> bool { + self.0 & (1 << digit) != 0 + } +} + +impl Display for DigitSet { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + let digits: Vec = (1..=9).filter(|&d| self.contains(d)).collect(); + write!( + f, + "{{{}}}", + digits + .iter() + .map(|d| d.to_string()) + .collect::>() + .join(", ") + ) + } +} + +impl VersionSet for DigitSet { + type V = u8; +} + +fn main() { + println!("sudoku example placeholder"); +} From be44052093c0e918c5e50b266be888afca2d2bdc Mon Sep 17 00:00:00 2001 From: Ben Moss Date: Thu, 14 May 2026 15:38:17 -0400 Subject: [PATCH 2/5] feat(examples): implement sudoku main with CLI args, solver, and grid output --- examples/sudoku.rs | 274 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 273 insertions(+), 1 deletion(-) diff --git a/examples/sudoku.rs b/examples/sudoku.rs index 9d0e37b..469ff5d 100644 --- a/examples/sudoku.rs +++ b/examples/sudoku.rs @@ -1,5 +1,11 @@ use std::fmt::{self, Display}; +use std::process; +use resolvo::{ + Candidates, Condition, ConditionId, ConditionalRequirement, Dependencies, DependencyProvider, + HintDependenciesAvailable, Interner, KnownDependencies, NameId, Problem, SolvableId, + Solver, SolverCache, StringId, VersionSetId, VersionSetUnionId, +}; use resolvo::utils::{Pool, VersionSet}; /// A set of digits 1-9 represented as a bitmask. @@ -39,6 +45,272 @@ impl VersionSet for DigitSet { type V = u8; } +// ---- Task 2: SudokuProvider struct and Interner impl ---- + +struct SudokuProvider { + pool: Pool, + /// Pre-filled digits indexed by cell (row * 9 + col). None = empty cell. + givens: [Option; 81], + /// Solvable IDs indexed by (cell_index * 9 + (digit - 1)) + solvables: Vec, + /// Name IDs for each cell, indexed by cell (row * 9 + col) + names: Vec, +} + +impl SudokuProvider { + fn new(givens: [Option; 81]) -> Self { + let pool = Pool::new(); + let mut names = Vec::with_capacity(81); + let mut solvables = Vec::with_capacity(81 * 9); + + for cell in 0..81 { + let row = cell / 9; + let col = cell % 9; + let name = pool.intern_package_name(format!("r{}c{}", row, col)); + names.push(name); + + for digit in 1..=9u8 { + let solvable = pool.intern_solvable(name, digit); + solvables.push(solvable); + } + } + + Self { pool, givens, solvables, names } + } + + fn solvable_id(&self, cell: usize, digit: u8) -> SolvableId { + self.solvables[cell * 9 + (digit as usize - 1)] + } + + fn cell_and_digit(&self, solvable: SolvableId) -> (usize, u8) { + let record = self.pool.resolve_solvable(solvable); + let cell = self.names.iter().position(|&n| n == record.name).unwrap(); + (cell, record.record) + } +} + +impl Interner for SudokuProvider { + fn display_solvable(&self, solvable: SolvableId) -> impl Display + '_ { + let record = self.pool.resolve_solvable(solvable); + let cell = self.names.iter().position(|&n| n == record.name).unwrap(); + let row = cell / 9; + let col = cell % 9; + format!("r{}c{}={}", row, col, record.record) + } + + fn display_merged_solvables(&self, solvables: &[SolvableId]) -> impl Display + '_ { + solvables + .iter() + .map(|&id| self.display_solvable(id).to_string()) + .collect::>() + .join(", ") + } + + fn display_name(&self, name: NameId) -> impl Display + '_ { + self.pool.resolve_package_name(name).clone() + } + + fn display_version_set(&self, version_set: VersionSetId) -> impl Display + '_ { + self.pool.resolve_version_set(version_set).to_string() + } + + fn display_string(&self, string_id: StringId) -> impl Display + '_ { + self.pool.resolve_string(string_id).to_owned() + } + + fn version_set_name(&self, version_set: VersionSetId) -> NameId { + self.pool.resolve_version_set_package_name(version_set) + } + + fn solvable_name(&self, solvable: SolvableId) -> NameId { + self.pool.resolve_solvable(solvable).name + } + + fn version_sets_in_union( + &self, + version_set_union: VersionSetUnionId, + ) -> impl Iterator { + self.pool.resolve_version_set_union(version_set_union) + } + + fn resolve_condition(&self, condition: ConditionId) -> Condition { + self.pool.resolve_condition(condition).clone() + } +} + +// ---- Task 3: DependencyProvider impl ---- + +impl SudokuProvider { + /// Returns the indices of the 20 peer cells (same row, column, or box) for a given cell. + fn peers(cell: usize) -> impl Iterator { + let row = cell / 9; + let col = cell % 9; + let box_row = (row / 3) * 3; + let box_col = (col / 3) * 3; + + let row_peers = (0..9).map(move |c| row * 9 + c); + let col_peers = (0..9).map(move |r| r * 9 + col); + let box_peers = (0..3).flat_map(move |r| (0..3).map(move |c| (box_row + r) * 9 + box_col + c)); + + row_peers + .chain(col_peers) + .chain(box_peers) + .filter(move |&peer| peer != cell) + .collect::>() + .into_iter() + } +} + +impl DependencyProvider for SudokuProvider { + async fn filter_candidates( + &self, + candidates: &[SolvableId], + version_set: VersionSetId, + inverse: bool, + ) -> Vec { + let digit_set = self.pool.resolve_version_set(version_set); + candidates + .iter() + .copied() + .filter(|&solvable| { + let record = self.pool.resolve_solvable(solvable); + let matches = digit_set.contains(record.record); + if inverse { !matches } else { matches } + }) + .collect() + } + + async fn get_candidates(&self, name: NameId) -> Option { + let cell = self.names.iter().position(|&n| n == name)?; + + let candidates: Vec = (1..=9u8) + .map(|digit| self.solvable_id(cell, digit)) + .collect(); + + let locked = self.givens[cell].map(|digit| self.solvable_id(cell, digit)); + + Some(Candidates { + candidates, + locked, + favored: None, + hint_dependencies_available: HintDependenciesAvailable::All, + excluded: Vec::new(), + }) + } + + async fn sort_candidates(&self, _solver: &SolverCache, solvables: &mut [SolvableId]) { + solvables.sort_by_key(|&solvable| self.pool.resolve_solvable(solvable).record); + } + + async fn get_dependencies(&self, solvable: SolvableId) -> Dependencies { + let (cell, digit) = self.cell_and_digit(solvable); + + let mut constrains = Vec::new(); + for peer in Self::peers(cell) { + let peer_name = self.names[peer]; + let exclusion_set = DigitSet::singleton(digit); + // Constrain the peer to NOT contain this digit + // We want to express "peer != digit", so we use the complement: + // intern a version set for the peer that represents all digits except this one. + // The constrains field means: "if the peer is selected, it must satisfy this version set". + // Since DigitSet::singleton(digit) means "only digit", we need the inverse. + // We'll use a version set that contains everything except the given digit. + let mut allowed = DigitSet::all(); + allowed.0 &= !exclusion_set.0; + let vs_id = self.pool.intern_version_set(peer_name, allowed); + constrains.push(vs_id); + } + + Dependencies::Known(KnownDependencies { + requirements: Vec::new(), + constrains, + }) + } +} + +// ---- Task 4: Parsing and pretty-print output ---- + +fn parse_puzzle(input: &str) -> Result<[Option; 81], String> { + if input.len() != 81 { + return Err(format!("Expected 81 characters, got {}", input.len())); + } + + let mut givens = [None; 81]; + for (i, ch) in input.chars().enumerate() { + match ch { + '.' | '0' => {} + '1'..='9' => givens[i] = Some(ch as u8 - b'0'), + _ => return Err(format!("Invalid character '{}' at position {}", ch, i)), + } + } + Ok(givens) +} + +fn print_grid(grid: &[u8; 81]) { + println!("┌───────┬───────┬───────┐"); + for row in 0..9 { + if row == 3 || row == 6 { + println!("├───────┼───────┼───────┤"); + } + for col in 0..9 { + if col % 3 == 0 { + print!("│ "); + } + print!("{} ", grid[row * 9 + col]); + } + println!("│"); + } + println!("└───────┴───────┴───────┘"); +} + fn main() { - println!("sudoku example placeholder"); + let input = match std::env::args().nth(1) { + Some(arg) => arg, + None => { + eprintln!("Usage: sudoku <81-character puzzle string>"); + eprintln!(" Use '.' or '0' for empty cells, '1'-'9' for givens."); + eprintln!(); + eprintln!("Example:"); + eprintln!(" cargo run --example sudoku -- \"53..7....6..195....98....6.8...6...34..8.3..17...2...6.6....28....419..5....8..79\""); + process::exit(1); + } + }; + + let givens = match parse_puzzle(&input) { + Ok(g) => g, + Err(e) => { + eprintln!("Error: {}", e); + process::exit(1); + } + }; + + let provider = SudokuProvider::new(givens); + + // Build requirements: each cell must have a digit assigned + let requirements: Vec = provider + .names + .iter() + .map(|&name| { + let version_set = provider.pool.intern_version_set(name, DigitSet::all()); + version_set.into() + }) + .collect(); + + let problem = Problem::new().requirements(requirements); + + let mut solver = Solver::new(provider); + match solver.solve(problem) { + Ok(solution) => { + let mut grid = [0u8; 81]; + for solvable_id in solution { + let (cell, digit) = solver.provider().cell_and_digit(solvable_id); + grid[cell] = digit; + } + print_grid(&grid); + } + Err(_) => { + eprintln!("No solution exists."); + process::exit(1); + } + } } From 6e03025409930a901a4f60ce2d65573161aaee0a Mon Sep 17 00:00:00 2001 From: Ben Moss Date: Thu, 14 May 2026 15:40:48 -0400 Subject: [PATCH 3/5] chore(sudoku): cleanup formatting and remove task markers Co-Authored-By: Claude Opus 4.6 (1M context) --- examples/sudoku.rs | 40 +++++++++++++++------------------------- 1 file changed, 15 insertions(+), 25 deletions(-) diff --git a/examples/sudoku.rs b/examples/sudoku.rs index 469ff5d..1563ba7 100644 --- a/examples/sudoku.rs +++ b/examples/sudoku.rs @@ -1,12 +1,12 @@ use std::fmt::{self, Display}; use std::process; +use resolvo::utils::{Pool, VersionSet}; use resolvo::{ Candidates, Condition, ConditionId, ConditionalRequirement, Dependencies, DependencyProvider, - HintDependenciesAvailable, Interner, KnownDependencies, NameId, Problem, SolvableId, - Solver, SolverCache, StringId, VersionSetId, VersionSetUnionId, + HintDependenciesAvailable, Interner, KnownDependencies, NameId, Problem, SolvableId, Solver, + SolverCache, StringId, VersionSetId, VersionSetUnionId, }; -use resolvo::utils::{Pool, VersionSet}; /// A set of digits 1-9 represented as a bitmask. #[derive(Clone, Eq, PartialEq, Hash, Debug)] @@ -45,15 +45,10 @@ impl VersionSet for DigitSet { type V = u8; } -// ---- Task 2: SudokuProvider struct and Interner impl ---- - struct SudokuProvider { pool: Pool, - /// Pre-filled digits indexed by cell (row * 9 + col). None = empty cell. givens: [Option; 81], - /// Solvable IDs indexed by (cell_index * 9 + (digit - 1)) solvables: Vec, - /// Name IDs for each cell, indexed by cell (row * 9 + col) names: Vec, } @@ -75,7 +70,12 @@ impl SudokuProvider { } } - Self { pool, givens, solvables, names } + Self { + pool, + givens, + solvables, + names, + } } fn solvable_id(&self, cell: usize, digit: u8) -> SolvableId { @@ -138,8 +138,6 @@ impl Interner for SudokuProvider { } } -// ---- Task 3: DependencyProvider impl ---- - impl SudokuProvider { /// Returns the indices of the 20 peer cells (same row, column, or box) for a given cell. fn peers(cell: usize) -> impl Iterator { @@ -150,7 +148,8 @@ impl SudokuProvider { let row_peers = (0..9).map(move |c| row * 9 + c); let col_peers = (0..9).map(move |r| r * 9 + col); - let box_peers = (0..3).flat_map(move |r| (0..3).map(move |c| (box_row + r) * 9 + box_col + c)); + let box_peers = + (0..3).flat_map(move |r| (0..3).map(move |c| (box_row + r) * 9 + box_col + c)); row_peers .chain(col_peers) @@ -208,15 +207,7 @@ impl DependencyProvider for SudokuProvider { let mut constrains = Vec::new(); for peer in Self::peers(cell) { let peer_name = self.names[peer]; - let exclusion_set = DigitSet::singleton(digit); - // Constrain the peer to NOT contain this digit - // We want to express "peer != digit", so we use the complement: - // intern a version set for the peer that represents all digits except this one. - // The constrains field means: "if the peer is selected, it must satisfy this version set". - // Since DigitSet::singleton(digit) means "only digit", we need the inverse. - // We'll use a version set that contains everything except the given digit. - let mut allowed = DigitSet::all(); - allowed.0 &= !exclusion_set.0; + let allowed = DigitSet(DigitSet::all().0 & !DigitSet::singleton(digit).0); let vs_id = self.pool.intern_version_set(peer_name, allowed); constrains.push(vs_id); } @@ -228,8 +219,6 @@ impl DependencyProvider for SudokuProvider { } } -// ---- Task 4: Parsing and pretty-print output ---- - fn parse_puzzle(input: &str) -> Result<[Option; 81], String> { if input.len() != 81 { return Err(format!("Expected 81 characters, got {}", input.len())); @@ -271,7 +260,9 @@ fn main() { eprintln!(" Use '.' or '0' for empty cells, '1'-'9' for givens."); eprintln!(); eprintln!("Example:"); - eprintln!(" cargo run --example sudoku -- \"53..7....6..195....98....6.8...6...34..8.3..17...2...6.6....28....419..5....8..79\""); + eprintln!( + " cargo run --example sudoku -- \"53..7....6..195....98....6.8...6...34..8.3..17...2...6.6....28....419..5....8..79\"" + ); process::exit(1); } }; @@ -286,7 +277,6 @@ fn main() { let provider = SudokuProvider::new(givens); - // Build requirements: each cell must have a digit assigned let requirements: Vec = provider .names .iter() From 619d7dc0054e94f5fc7c058d4d813bf58c1b808b Mon Sep 17 00:00:00 2001 From: Ben Moss Date: Thu, 14 May 2026 15:52:25 -0400 Subject: [PATCH 4/5] docs(sudoku): add comments explaining the resolvo-to-sudoku mapping Add module-level documentation with a concept mapping table, section headers, and inline comments explaining key design decisions like the complement-set constraint encoding and locked candidates. Also print the unsolved puzzle before the solution, and display empty cells as dots. Co-Authored-By: Claude Opus 4.6 (1M context) --- examples/sudoku.rs | 92 ++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 89 insertions(+), 3 deletions(-) diff --git a/examples/sudoku.rs b/examples/sudoku.rs index 1563ba7..07cc131 100644 --- a/examples/sudoku.rs +++ b/examples/sudoku.rs @@ -1,3 +1,19 @@ +//! Solves sudoku puzzles using resolvo's CDCL SAT solver. +//! +//! This example demonstrates that resolvo — a package dependency resolver — can solve +//! constraint satisfaction problems beyond package resolution. It maps sudoku concepts +//! to resolvo's domain model: +//! +//! | Sudoku | Resolvo | Example | +//! |---------------------|----------------------|---------------------| +//! | Cell (81 total) | Package (`NameId`) | `r0c0`, `r4c7` | +//! | Digit 1-9 for cell | Version (`SolvableId`)| `r0c0=5` | +//! | "Cell needs a digit"| Requirement | "install r0c0" | +//! | Row/col/box rules | Constraint | "r0c0 excludes 5 from peers" | +//! | Pre-filled cell | Locked candidate | "r0c0 must be 5" | +//! +//! Usage: `cargo run --example sudoku -- "53..7....6..195....98....6.8...6...34..8.3..17...2...6.6....28....419..5....8..79"` + use std::fmt::{self, Display}; use std::process; @@ -8,15 +24,26 @@ use resolvo::{ SolverCache, StringId, VersionSetId, VersionSetUnionId, }; -/// A set of digits 1-9 represented as a bitmask. +// -- VersionSet implementation ------------------------------------------------ +// +// Resolvo is generic over what "versions" mean. In package management, a version +// set might be a semver range like ">=1.2, <2.0". For sudoku, our "versions" are +// digits 1-9, and a "version set" is a subset of those digits. We represent this +// compactly as a bitmask. + +/// A set of digits 1-9 represented as a bitmask. Bit N set means digit N is in +/// the set. This serves as resolvo's `VersionSet` — the analog of a semver range, +/// but for sudoku digits. #[derive(Clone, Eq, PartialEq, Hash, Debug)] struct DigitSet(u16); impl DigitSet { + /// All digits 1-9. Used as the "any version" requirement for each cell. fn all() -> Self { DigitSet(0b1111111110) // bits 1-9 set } + /// A single digit. Used to build exclusion constraints between peer cells. fn singleton(digit: u8) -> Self { DigitSet(1 << digit) } @@ -45,10 +72,23 @@ impl VersionSet for DigitSet { type V = u8; } +// -- SudokuProvider ----------------------------------------------------------- +// +// The provider is the bridge between the problem domain (sudoku) and the solver. +// It tells resolvo what "packages" exist (cells), what "versions" are available +// (digits 1-9), and what constraints apply (no duplicate digits in any row, +// column, or 3x3 box). + +/// Implements resolvo's `DependencyProvider` and `Interner` traits to present a +/// sudoku puzzle as a package resolution problem. struct SudokuProvider { pool: Pool, + /// Pre-filled digits. `givens[row * 9 + col] = Some(d)` means the cell is fixed. givens: [Option; 81], + /// Flat lookup: `solvables[cell * 9 + (digit - 1)]` gives the SolvableId for + /// "cell X takes digit D". solvables: Vec, + /// One NameId per cell, indexed by `row * 9 + col`. names: Vec, } @@ -58,6 +98,7 @@ impl SudokuProvider { let mut names = Vec::with_capacity(81); let mut solvables = Vec::with_capacity(81 * 9); + // Register 81 "packages" (cells) with 9 "versions" (digits) each. for cell in 0..81 { let row = cell / 9; let col = cell % 9; @@ -82,6 +123,7 @@ impl SudokuProvider { self.solvables[cell * 9 + (digit as usize - 1)] } + /// Reverse lookup: given a solvable, return which cell and digit it represents. fn cell_and_digit(&self, solvable: SolvableId) -> (usize, u8) { let record = self.pool.resolve_solvable(solvable); let cell = self.names.iter().position(|&n| n == record.name).unwrap(); @@ -89,6 +131,11 @@ impl SudokuProvider { } } +// -- Interner impl ------------------------------------------------------------ +// +// The Interner trait provides human-readable display for solver objects. This is +// used in error messages when a puzzle is unsolvable. + impl Interner for SudokuProvider { fn display_solvable(&self, solvable: SolvableId) -> impl Display + '_ { let record = self.pool.resolve_solvable(solvable); @@ -138,8 +185,23 @@ impl Interner for SudokuProvider { } } +// -- DependencyProvider impl -------------------------------------------------- +// +// This is where the sudoku rules are encoded. The key insight: +// +// - `get_candidates` tells the solver what digits are possible for each cell. +// Pre-filled cells have a single `locked` candidate. +// +// - `get_dependencies` encodes the sudoku constraint: when a cell is assigned +// digit D, every peer cell (same row, column, or 3x3 box) is constrained to +// NOT contain digit D. This is expressed via `constrains` — resolvo's mechanism +// for saying "if package X is in the solution, it must satisfy this version set." +// +// - `filter_candidates` applies a DigitSet constraint to narrow candidates. + impl SudokuProvider { - /// Returns the indices of the 20 peer cells (same row, column, or box) for a given cell. + /// Returns the 20 peer cell indices for a given cell — all cells that share + /// the same row, column, or 3x3 box (excluding the cell itself). fn peers(cell: usize) -> impl Iterator { let row = cell / 9; let col = cell % 9; @@ -186,6 +248,7 @@ impl DependencyProvider for SudokuProvider { .map(|digit| self.solvable_id(cell, digit)) .collect(); + // If this cell has a pre-filled digit, lock the solver to that single candidate. let locked = self.givens[cell].map(|digit| self.solvable_id(cell, digit)); Some(Candidates { @@ -204,6 +267,9 @@ impl DependencyProvider for SudokuProvider { async fn get_dependencies(&self, solvable: SolvableId) -> Dependencies { let (cell, digit) = self.cell_and_digit(solvable); + // For each peer cell, add a constraint: "peer must NOT be this digit." + // In resolvo terms, `constrains` means "the peer's version must match this set", + // so we use the complement — all digits except the current one. let mut constrains = Vec::new(); for peer in Self::peers(cell) { let peer_name = self.names[peer]; @@ -219,6 +285,9 @@ impl DependencyProvider for SudokuProvider { } } +// -- Puzzle I/O --------------------------------------------------------------- + +/// Parses an 81-character string into a grid of givens. '.' or '0' means empty. fn parse_puzzle(input: &str) -> Result<[Option; 81], String> { if input.len() != 81 { return Err(format!("Expected 81 characters, got {}", input.len())); @@ -245,13 +314,19 @@ fn print_grid(grid: &[u8; 81]) { if col % 3 == 0 { print!("│ "); } - print!("{} ", grid[row * 9 + col]); + if grid[row * 9 + col] == 0 { + print!(". "); + } else { + print!("{} ", grid[row * 9 + col]); + } } println!("│"); } println!("└───────┴───────┴───────┘"); } +// -- Main --------------------------------------------------------------------- + fn main() { let input = match std::env::args().nth(1) { Some(arg) => arg, @@ -275,8 +350,18 @@ fn main() { } }; + // Print the unsolved puzzle. + let mut puzzle_grid = [0u8; 81]; + for (i, g) in givens.iter().enumerate() { + puzzle_grid[i] = g.unwrap_or(0); + } + print_grid(&puzzle_grid); + println!(); + let provider = SudokuProvider::new(givens); + // Each cell must be assigned exactly one digit. We express this as a + // requirement per cell: "pick some version (digit) from DigitSet::all()." let requirements: Vec = provider .names .iter() @@ -288,6 +373,7 @@ fn main() { let problem = Problem::new().requirements(requirements); + // Solve using resolvo's CDCL SAT solver. let mut solver = Solver::new(provider); match solver.solve(problem) { Ok(solution) => { From 4802e8df057bf7e3170db2f03238d342bc46e4f3 Mon Sep 17 00:00:00 2001 From: Ben Moss Date: Thu, 14 May 2026 15:56:31 -0400 Subject: [PATCH 5/5] feat(sudoku): show resolvo conflict explanation for unsolvable puzzles Co-Authored-By: Claude Opus 4.6 (1M context) --- examples/sudoku.rs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/examples/sudoku.rs b/examples/sudoku.rs index 07cc131..f8c698b 100644 --- a/examples/sudoku.rs +++ b/examples/sudoku.rs @@ -384,6 +384,11 @@ fn main() { } print_grid(&grid); } + Err(resolvo::UnsolvableOrCancelled::Unsolvable(conflict)) => { + eprintln!("No solution exists. The solver found these conflicts:\n"); + eprintln!("{}", conflict.display_user_friendly(&solver)); + process::exit(1); + } Err(_) => { eprintln!("No solution exists."); process::exit(1);