nqueens/
nqueens.rs

1use std::path::PathBuf;
2
3use clap::Parser;
4use pumpkin_solver::constraints;
5use pumpkin_solver::options::SolverOptions;
6use pumpkin_solver::proof::ProofLog;
7use pumpkin_solver::results::ProblemSolution;
8use pumpkin_solver::results::SatisfactionResult;
9use pumpkin_solver::termination::Indefinite;
10use pumpkin_solver::variables::TransformableVariable;
11use pumpkin_solver::Solver;
12
13#[derive(Parser)]
14struct Cli {
15    /// The size of the chess board.
16    n: u32,
17
18    /// The location of the proof.
19    ///
20    /// If a location is given, the full proof will be logged there.
21    #[arg(short, long)]
22    proof: Option<PathBuf>,
23}
24
25fn main() {
26    let Cli {
27        n,
28        proof: proof_path,
29    } = Cli::parse();
30
31    if n < 2 {
32        println!("Please provide an 'n > 1'");
33        return;
34    }
35
36    let Ok(proof_log) = proof_path
37        .as_ref()
38        .map(|path| ProofLog::cp(path, true))
39        .transpose()
40        .map(|proof| proof.unwrap_or_default())
41    else {
42        eprintln!(
43            "Failed to create proof file at {}",
44            proof_path.unwrap().display()
45        );
46        return;
47    };
48
49    let mut solver = Solver::with_options(SolverOptions {
50        proof_log,
51        ..Default::default()
52    });
53
54    // Create the constraint tags for the three all_different constraints.
55    let c1_tag = solver.new_constraint_tag();
56    let c2_tag = solver.new_constraint_tag();
57    let c3_tag = solver.new_constraint_tag();
58
59    let variables = (0..n)
60        .map(|i| solver.new_named_bounded_integer(0, n as i32 - 1, format!("q{i}")))
61        .collect::<Vec<_>>();
62
63    let _ = solver
64        .add_constraint(constraints::all_different(variables.clone(), c1_tag))
65        .post();
66
67    let diag1 = variables
68        .iter()
69        .cloned()
70        .enumerate()
71        .map(|(i, var)| var.offset(i as i32))
72        .collect::<Vec<_>>();
73    let diag2 = variables
74        .iter()
75        .cloned()
76        .enumerate()
77        .map(|(i, var)| var.offset(-(i as i32)))
78        .collect::<Vec<_>>();
79
80    let _ = solver
81        .add_constraint(constraints::all_different(diag1, c2_tag))
82        .post();
83    let _ = solver
84        .add_constraint(constraints::all_different(diag2, c3_tag))
85        .post();
86
87    let mut brancher = solver.default_brancher();
88    match solver.satisfy(&mut brancher, &mut Indefinite) {
89        SatisfactionResult::Satisfiable(satisfiable) => {
90            let solution = satisfiable.solution();
91
92            let row_separator = format!("{}+", "+---".repeat(n as usize));
93
94            for row in 0..n {
95                println!("{row_separator}");
96
97                let queen_col = solution.get_integer_value(variables[row as usize]) as u32;
98
99                for col in 0..n {
100                    let string = if queen_col == col { "| * " } else { "|   " };
101
102                    print!("{string}");
103                }
104
105                println!("|");
106            }
107
108            println!("{row_separator}");
109        }
110        SatisfactionResult::Unsatisfiable(_, _) => {
111            println!("{n}-queens is unsatisfiable.");
112        }
113        SatisfactionResult::Unknown(_, _) => {
114            println!("Timeout.");
115        }
116    };
117}
nqueens/nqueens.rs

nqueens/
nqueens.rs
