sat_solver/command_line/
cli.rs

1#![allow(dead_code, clippy::cast_precision_loss)]
2
3use crate::sat::assignment::{AssignmentImpls, AssignmentType};
4use crate::sat::cdcl::Cdcl;
5use crate::sat::clause_management::{
6    ClauseManagement, ClauseManagementImpls, LbdClauseManagement, NoClauseManagement,
7};
8use crate::sat::clause_storage::{LiteralStorage, LiteralStorageImpls, LiteralStorageType};
9use crate::sat::cnf::Cnf;
10use crate::sat::dimacs::parse_file;
11use crate::sat::dpll::Dpll;
12use crate::sat::literal::{Literal, LiteralImpls, LiteralType};
13use crate::sat::propagation::{PropagatorImpls, PropagatorType};
14use crate::sat::restarter::{RestarterImpls, RestarterType};
15use crate::sat::solver::{
16    DynamicConfig, SolutionStats, Solutions, Solver, SolverImpls, SolverType,
17};
18use crate::sat::variable_selection::{VariableSelectionImpls, VariableSelectionType};
19use crate::{nonogram, sudoku};
20use clap::{Args, Parser, Subcommand};
21use std::path::PathBuf;
22use std::time::Duration;
23use tikv_jemalloc_ctl::{epoch, stats};
24
25/// Defines the command-line interface for the sat solver application.
26///
27/// Uses `clap` for parsing arguments.
28#[derive(Parser, Debug)]
29#[command(name = "sat_solver", version, about = "A configurable SAT solver")]
30pub(crate) struct Cli {
31    /// An optional global path argument. If provided without a subcommand,
32    /// it's treated as the path to a DIMACS .cnf file to solve.
33    /// value hint for directory or file path ending with `.cnf`.
34    #[arg(global = true)]
35    pub path: Option<PathBuf>,
36
37    /// Specifies the subcommand to execute (e.g. `file`, `text`, `sudoku`, `nonogram`).
38    #[clap(subcommand)]
39    pub command: Option<Commands>,
40
41    /// Common options applicable to all commands.
42    #[command(flatten)]
43    pub common: CommonOptions,
44}
45
46/// Enumerates the available subcommands for the sat solver.
47#[derive(Subcommand, Debug)]
48pub(crate) enum Commands {
49    /// Solve a CNF file in DIMACS format.
50    File {
51        /// Path to the DIMACS .cnf file.
52        #[arg(long)]
53        path: PathBuf,
54
55        /// Common options for this subcommand.
56        #[command(flatten)]
57        common: CommonOptions,
58    },
59
60    /// Solve a CNF formula provided as plain text.
61    Text {
62        /// Literal CNF input as a string (e.g. "1 -2 0\n2 3 0").
63        /// Each line represents a clause, literals are space-separated, and 0 terminates a clause.
64        #[arg(short, long)]
65        input: String,
66
67        /// Common options for this subcommand.
68        #[command(flatten)]
69        common: CommonOptions,
70    },
71
72    /// Solve a Sudoku puzzle.
73    /// The Sudoku puzzle is converted into a CNF formula, which is then solved.
74    Sudoku {
75        /// Path to the Sudoku file. The format of this file is defined by the `sudoku::solver::parse_sudoku_file` function.
76        #[arg(long)]
77        path: PathBuf,
78
79        /// If true, the generated DIMACS CNF representation of the Sudoku puzzle will be printed and saved to a file.
80        #[arg(short, long, default_value_t = false)]
81        export_dimacs: bool,
82
83        /// Common options for this subcommand.
84        #[command(flatten)]
85        common: CommonOptions,
86    },
87
88    /// Solve a Nonogram puzzle.
89    /// The Nonogram puzzle is converted into a CNF formula, which is then solved.
90    Nonogram {
91        /// Path to the Nonogram file. The format of this file is defined by the `nonogram::solver::parse_nonogram_file` function.
92        #[arg(long)]
93        path: PathBuf,
94
95        /// Common options for this subcommand.
96        #[command(flatten)]
97        common: CommonOptions,
98    },
99
100    /// Generate shell completion scripts.
101    Completions {
102        /// The shell to generate completions for.
103        #[arg(value_enum)]
104        shell: clap_complete::Shell,
105    },
106}
107
108/// Defines common command-line options shared across different subcommands.
109#[derive(Args, Debug, Default, Clone)]
110#[allow(clippy::struct_excessive_bools)]
111pub(crate) struct CommonOptions {
112    /// Enable debug output, providing more verbose logging during the solving process.
113    #[arg(short, long, default_value_t = false)]
114    pub(crate) debug: bool,
115
116    /// Enable verification of the found solution. If a solution is found, it's checked against the original CNF.
117    #[arg(short, long, default_value_t = true)]
118    pub(crate) verify: bool,
119
120    /// Enable printing of performance and problem statistics after solving.
121    #[arg(short, long, default_value_t = true)]
122    pub(crate) stats: bool,
123
124    /// Enable printing of the satisfying assignment (model) if the formula is satisfiable.
125    #[arg(short, long, default_value_t = false)]
126    pub(crate) print_solution: bool,
127
128    /// Specifies the SAT solver algorithm to use.
129    /// Supported values are "cdcl" (Conflict-Driven Clause Learning) and "dpll" (Davis-Putnam-Logemann-Loveland).
130    #[arg(long, default_value_t = SolverType::Cdcl)]
131    solver: SolverType,
132
133    /// Disable clause management, which may affect the solver's performance and memory usage.
134    #[arg(long, default_value_t = false)]
135    no_clause_management: bool,
136
137    #[arg(long, default_value_t = RestarterType::Luby)]
138    restart_strategy: RestarterType,
139
140    #[arg(long, default_value_t = VariableSelectionType::Vsids)]
141    variable_selection: VariableSelectionType,
142
143    #[arg(long, default_value_t = LiteralStorageType::SmallVec)]
144    literal_storage: LiteralStorageType,
145
146    #[arg(long, default_value_t = AssignmentType::Vec)]
147    assignment: AssignmentType,
148
149    #[arg(long, default_value_t = PropagatorType::WatchedLiterals)]
150    propagator: PropagatorType,
151
152    #[arg(long, default_value_t = LiteralType::Double)]
153    literals: LiteralType,
154}
155
156/// Converts the `CommonOptions` into the specific implementations required by the solver.
157pub(crate) fn get_solver_parts<L: Literal, S: LiteralStorage<L>>(
158    common: &CommonOptions,
159    cnf: &Cnf<L, S>,
160) -> (
161    AssignmentImpls,
162    ClauseManagementImpls<10>,
163    PropagatorImpls<LiteralImpls, LiteralStorageImpls<LiteralImpls, 12>, AssignmentImpls>,
164    VariableSelectionImpls,
165    RestarterImpls<3>,
166) {
167    let manager = if common.no_clause_management {
168        ClauseManagementImpls::NoClauseManagement(NoClauseManagement::new(&cnf.clauses))
169    } else {
170        ClauseManagementImpls::LbdActivityClauseManagement(LbdClauseManagement::new(&cnf.clauses))
171    };
172    let cnf1: Cnf<LiteralImpls, LiteralStorageImpls<LiteralImpls, 12>> = cnf.convert();
173    let propagator = common.propagator.to_impl(&cnf1);
174
175    (
176        common.assignment.to_impl(cnf.num_vars),
177        manager,
178        propagator,
179        common
180            .variable_selection
181            .to_impl(cnf.num_vars, &cnf.lits, &cnf.clauses),
182        common.restart_strategy.to_impl(),
183    )
184}
185
186pub(crate) fn get_solver<L: Literal, S: LiteralStorage<L>>(
187    common: &CommonOptions,
188    cnf: &Cnf<L, S>,
189) -> SolverImpls<DynamicConfig> {
190    let (assignment, manager, propagator, selector, restarter) = get_solver_parts(common, cnf);
191
192    match common.solver {
193        SolverType::Cdcl => SolverImpls::Cdcl(Box::from(Cdcl::<DynamicConfig>::from_parts(
194            cnf.clone(),
195            assignment,
196            manager,
197            propagator,
198            restarter,
199            selector,
200        ))),
201        SolverType::Dpll => SolverImpls::Dpll(Box::from(Dpll::<DynamicConfig>::from_parts(
202            cnf.clone(),
203            assignment,
204            manager,
205            propagator,
206            restarter,
207            selector,
208        ))),
209    }
210}
211
212/// Solves a directory of CNF files.
213/// This function iterates over all `.cnf` files in the directory, parses each file,
214/// solves it, and reports the results.
215///
216/// # Arguments
217/// * `path` - The path to the directory containing CNF files.
218/// * `common` - Common options for the solver, such as debug mode, verification, and statistics.
219///
220/// # Panics
221/// If the provided path is not a directory or if any file cannot be read or parsed.
222pub(crate) fn solve_dir(path: &PathBuf, common: &CommonOptions) -> Result<(), String> {
223    if !path.is_dir() {
224        eprintln!("Provided path is not a directory: {}", path.display());
225        std::process::exit(1);
226    }
227
228    for entry in walkdir::WalkDir::new(path)
229        .into_iter()
230        .filter_map(Result::ok)
231    {
232        let file_path = entry.path().to_path_buf();
233        if file_path.extension().is_some_and(|ext| ext == "sudoku") {
234            solve_sudoku(&file_path, false, common)?;
235            continue;
236        }
237
238        if file_path.extension().is_none_or(|ext| ext != "cnf") {
239            eprintln!("Skipping non-CNF file: {}", file_path.display());
240            continue;
241        }
242
243        if !file_path.is_file() {
244            eprintln!("Skipping non-file entry: {}", file_path.display());
245            continue;
246        }
247
248        if !file_path.exists() {
249            eprintln!("File does not exist: {}", file_path.display());
250            continue;
251        }
252
253        let time = std::time::Instant::now();
254        let result = parse_file(&file_path);
255        if let Err(e) = result {
256            return Err(e.to_string());
257        }
258        let cnf = result.unwrap();
259        let elapsed = time.elapsed();
260
261        solve_and_report(&cnf, common, Some(&file_path), elapsed);
262    }
263
264    Ok(())
265}
266
267/// Verifies a given solution (`sol`) against a CNF formula (`cnf`).
268///
269/// Prints whether the verification was successful. If verification fails, it panics.
270/// If `sol` is `None` (indicating UNSAT), it prints "UNSAT".
271///
272/// # Arguments
273/// * `cnf` - The CNF formula to verify against.
274/// * `sol` - An `Option<Solutions>` representing the model found by the solver.
275pub(crate) fn verify_solution(cnf: &Cnf, sol: Option<&Solutions>) {
276    if let Some(sol_values) = sol {
277        let ok = cnf.verify(sol_values);
278        println!("Verified: {ok:?}");
279        assert!(ok, "Solution failed verification!");
280    } else {
281        println!("UNSAT");
282    }
283}
284
285/// Solves a CNF formula using the specified solver.
286///
287/// # Arguments
288/// * `cnf` - The CNF formula to solve.
289/// * `debug` - Boolean flag to enable debug printing.
290/// * `label` - An optional label for the problem (e.g. file path), used in debug output.
291/// * `solver_name` - The name of the solver to use ("dpll" or "cdcl").
292///
293/// # Returns
294/// A tuple containing:
295/// * `Option<Solutions>`: The solution (model) if found, otherwise `None`.
296/// * `Duration`: The time taken to solve the formula.
297/// * `SolutionStats`: Statistics collected during the solving process.
298///
299/// # Panics
300/// If `solver_name` is not "dpll" or "cdcl".
301pub(crate) fn solve(
302    cnf: &Cnf,
303    debug: bool,
304    label: Option<&PathBuf>,
305    common_options: &CommonOptions,
306) -> (Option<Solutions>, Duration, SolutionStats) {
307    if let Some(name) = label {
308        println!("Solving: {}", name.display());
309    }
310
311    if debug {
312        println!("CNF: {cnf}");
313        println!("Variables: {}", cnf.num_vars);
314        println!("Clauses: {}", cnf.clauses.len());
315        println!("Literals: {}", cnf.lits.len());
316    }
317
318    solve_impl(cnf, common_options)
319}
320
321/// Solves a CNF formula using the CDCL solver.
322///
323/// # Arguments
324/// * `cnf` - The CNF formula to solve.
325/// * `debug` - Boolean flag to enable debug printing.
326///
327/// # Returns
328/// See `solve` function return type.
329pub(crate) fn solve_impl(
330    cnf: &Cnf,
331    common_options: &CommonOptions,
332) -> (Option<Solutions>, Duration, SolutionStats) {
333    epoch::advance().unwrap();
334
335    let time = std::time::Instant::now();
336
337    let mut solver = get_solver(common_options, cnf);
338    let sol = solver.solve();
339
340    let elapsed = time.elapsed();
341
342    if common_options.debug {
343        println!("Solution: {sol:?}");
344        println!("Time: {elapsed:?}");
345    }
346
347    (sol, elapsed, solver.stats())
348}
349
350/// Parses a CNF file, solves it, and reports results including stats and verification.
351///
352/// This function is a convenience wrapper around `solve`, `verify_solution`, and `print_stats`.
353///
354/// # Arguments
355/// * `cnf` - The CNF formula, typically parsed from a file or text.
356/// * `common` - `CommonOptions` providing solver configuration (debug, verify, stats, solver type).
357/// * `label` - An optional label for the problem (e.g. file path).
358/// * `parse_time` - The time taken to parse the CNF input.
359pub(crate) fn solve_and_report(
360    cnf: &Cnf,
361    common: &CommonOptions,
362    label: Option<&PathBuf>,
363    parse_time: Duration,
364) {
365    epoch::advance().unwrap();
366
367    let (sol, elapsed, solver_stats) = solve(cnf, common.debug, label, common);
368
369    epoch::advance().unwrap();
370
371    let allocated_bytes = stats::allocated::mib().unwrap().read().unwrap();
372    let resident_bytes = stats::resident::mib().unwrap().read().unwrap();
373
374    let allocated_mib = allocated_bytes as f64 / (1024.0 * 1024.0);
375    let resident_mib = resident_bytes as f64 / (1024.0 * 1024.0);
376
377    if common.verify {
378        verify_solution(cnf, Option::from(&sol));
379    }
380
381    if common.stats {
382        print_stats(
383            parse_time,
384            elapsed,
385            cnf,
386            &solver_stats,
387            allocated_mib,
388            resident_mib,
389            common.print_solution,
390            Option::from(&sol),
391        );
392    }
393}
394
395/// Helper function to print a single statistic line in a formatted table row.
396///
397/// # Arguments
398/// * `label` - The description of the statistic.
399/// * `value` - The value of the statistic, implementing `std::fmt::Display`.
400pub(crate) fn stat_line(label: &str, value: impl std::fmt::Display) {
401    println!("|  {label:<28} {value:>18}  |");
402}
403
404/// Helper function to print a statistic line that includes a rate (value/second).
405///
406/// # Arguments
407/// * `label` - The description of the statistic.
408/// * `value` - The raw count for the statistic.
409/// * `elapsed` - The elapsed time in seconds, used to calculate the rate.
410pub(crate) fn stat_line_with_rate(label: &str, value: usize, elapsed: f64) {
411    let rate = if elapsed > 0.0 {
412        value as f64 / elapsed
413    } else {
414        0.0
415    };
416    println!("|  {label:<20} {value:>12} ({rate:>9.0}/sec)  |");
417}
418
419/// Prints a summary of problem and search statistics.
420///
421/// # Arguments
422/// * `parse_time` - Duration spent parsing the input.
423/// * `elapsed` - Duration spent by the solver.
424/// * `cnf` - The CNF formula.
425/// * `s` - `SolutionStats` collected by the solver.
426/// * `allocated` - Allocated memory in MiB.
427/// * `resident` - Resident memory in MiB.
428/// * `print_solution` - Flag indicating whether to print the solution model.
429/// * `solutions` - The `Option<Solutions>` found by the solver.
430#[allow(clippy::too_many_arguments)]
431pub(crate) fn print_stats(
432    parse_time: Duration,
433    elapsed: Duration,
434    cnf: &Cnf,
435    s: &SolutionStats,
436    allocated: f64,
437    resident: f64,
438    print_solution: bool,
439    solutions: Option<&Solutions>,
440) {
441    let elapsed_secs = elapsed.as_secs_f64();
442
443    println!("\n=======================[ Problem Statistics ]=========================");
444    stat_line("Parse time (s)", format!("{:.3}", parse_time.as_secs_f64()));
445    stat_line(
446        "Variables",
447        if cnf.num_vars > 0 {
448            cnf.num_vars - 1
449        } else {
450            0
451        },
452    );
453    stat_line("Clauses (original)", cnf.non_learnt_idx);
454    stat_line("Literals (original)", cnf.lits.len());
455
456    println!("========================[ Search Statistics ]========================");
457    stat_line("Learnt clauses", s.learnt_clauses);
458    stat_line("Total clauses (incl. learnt)", cnf.clauses.len());
459    stat_line_with_rate("Conflicts", s.conflicts, elapsed_secs);
460    stat_line_with_rate("Decisions", s.decisions, elapsed_secs);
461    stat_line_with_rate("Propagations", s.propagations, elapsed_secs);
462    stat_line_with_rate("Restarts", s.restarts, elapsed_secs);
463    stat_line("Memory usage (MiB)", format!("{allocated:.2}"));
464    stat_line("Resident memory (MiB)", format!("{resident:.2}"));
465    stat_line("CPU time (s)", format!("{elapsed_secs:.3}"));
466    println!("=====================================================================");
467
468    if let Some(solutions_values) = solutions {
469        if print_solution {
470            println!("Solutions: {solutions_values}");
471        }
472    }
473
474    if solutions.is_some() {
475        println!("\nSATISFIABLE");
476    } else {
477        println!("\nUNSATISFIABLE");
478    }
479}
480
481/// Solve a sudoku file.
482///
483/// # Errors
484///
485/// If the sudoku doesn't exist.
486pub(crate) fn solve_sudoku(
487    path: &PathBuf,
488    export_dimacs: bool,
489    common: &CommonOptions,
490) -> Result<(), String> {
491    if !path.exists() {
492        return Err(format!("Sudoku file does not exist: {}", path.display()));
493    }
494
495    if !path.is_file() {
496        return Err(format!("Provided path is not a file: {}", path.display()));
497    }
498
499    let time = std::time::Instant::now();
500    let sudoku = sudoku::solver::parse_sudoku_file(path);
501
502    match sudoku {
503        Ok(sudoku) => {
504            println!("Parsed Sudoku:\n{sudoku}");
505
506            let cnf = sudoku.to_cnf();
507
508            if export_dimacs {
509                let dimacs = cnf.to_string();
510                println!("DIMACS:\n{dimacs}");
511
512                let path_name = path.display().to_string();
513                let dimacs_path = format!("{path_name}.cnf");
514                if let Err(e) = std::fs::write(&dimacs_path, dimacs) {
515                    return Err(format!("Unable to write {dimacs_path}: {e}"));
516                }
517                println!("DIMACS written to: {dimacs_path}");
518            }
519
520            let parse_time = time.elapsed();
521            let (sol, elapsed, solver_stats) = solve(&cnf, common.debug, Some(path), common);
522
523            epoch::advance().unwrap();
524
525            let allocated_bytes = stats::allocated::mib().unwrap().read().unwrap();
526            let resident_bytes = stats::resident::mib().unwrap().read().unwrap();
527            let allocated_mib = allocated_bytes as f64 / (1024.0 * 1024.0);
528            let resident_mib = resident_bytes as f64 / (1024.0 * 1024.0);
529
530            if common.verify {
531                verify_solution(&cnf, Option::from(&sol));
532            }
533
534            if common.stats {
535                print_stats(
536                    parse_time,
537                    elapsed,
538                    &cnf,
539                    &solver_stats,
540                    allocated_mib,
541                    resident_mib,
542                    common.print_solution,
543                    Option::from(&sol),
544                );
545            }
546
547            if let Some(sol_values) = sol {
548                let solution_grid = sudoku.decode(&sol_values);
549                println!("Solution: {solution_grid}");
550            } else {
551                println!("No solution found");
552            }
553        }
554        Err(e) => {
555            return Err(format!("Error parsing Sudoku file: {e}"));
556        }
557    }
558    Ok(())
559}
560
561/// Solve a nonogram file.
562///
563/// # Errors
564///
565/// If the nonogram doesn't exist.
566pub(crate) fn solve_nonogram(path: &PathBuf, common: &CommonOptions) -> Result<(), String> {
567    if !path.exists() {
568        return Err(format!("Nonogram file does not exist: {}", path.display()));
569    }
570
571    if !path.is_file() {
572        return Err(format!("Provided path is not a file: {}", path.display()));
573    }
574
575    let time = std::time::Instant::now();
576    let nonogram = nonogram::solver::parse_nonogram_file(path);
577    match nonogram {
578        Ok(nonogram) => {
579            println!("Parsed Nonogram:\n{nonogram}");
580
581            let cnf = nonogram.to_cnf();
582
583            let parse_time = time.elapsed();
584            let (sol, elapsed, solver_stats) = solve(&cnf, common.debug, Some(path), common);
585
586            epoch::advance().unwrap();
587            let allocated_bytes = stats::allocated::mib().unwrap().read().unwrap();
588            let resident_bytes = stats::resident::mib().unwrap().read().unwrap();
589            let allocated_mib = allocated_bytes as f64 / (1024.0 * 1024.0);
590            let resident_mib = resident_bytes as f64 / (1024.0 * 1024.0);
591
592            if common.verify {
593                verify_solution(&cnf, Option::from(&sol));
594            }
595
596            if common.stats {
597                print_stats(
598                    parse_time,
599                    elapsed,
600                    &cnf,
601                    &solver_stats,
602                    allocated_mib,
603                    resident_mib,
604                    common.print_solution,
605                    Option::from(&sol),
606                );
607            }
608
609            if let Some(sol_values) = sol {
610                let solution_grid = nonogram.decode(&sol_values);
611                for row in solution_grid {
612                    println!("{row:?}");
613                }
614            } else {
615                println!("No solution found");
616            }
617        }
618        Err(e) => {
619            return Err(format!("Error parsing nonogram file: {e}"));
620        }
621    }
622    Ok(())
623}
sat_solver/command_line/cli.rs

sat_solver/command_line/
cli.rs
