Struct ProofLog 

pub struct ProofLog { /* private fields */ }

A proof log which logs the proof steps necessary to prove unsatisfiability or optimality. We allow the following types of proofs:

• A CP proof log - This can be created using ProofLog::cp.
• A DIMACS proof log - This can be created using ProofLog::dimacs.

When a proof log should not be generated, use the implementation of Default.

Implementations

impl ProofLog

pub fn cp(file_path: &Path, log_hints: bool) -> Result<ProofLog, Error>

Create a CP proof logger.

Examples found in repository

examples/nqueens.rs (line 38)

fn main() {
    let Cli {
        n,
        proof: proof_path,
    } = Cli::parse();

    if n < 2 {
        println!("Please provide an 'n > 1'");
        return;
    }

    let Ok(proof_log) = proof_path
        .as_ref()
        .map(|path| ProofLog::cp(path, true))
        .transpose()
        .map(|proof| proof.unwrap_or_default())
    else {
        eprintln!(
            "Failed to create proof file at {}",
            proof_path.unwrap().display()
        );
        return;
    };

    let mut solver = Solver::with_options(SolverOptions {
        proof_log,
        ..Default::default()
    });

    // Create the constraint tags for the three all_different constraints.
    let c1_tag = solver.new_constraint_tag();
    let c2_tag = solver.new_constraint_tag();
    let c3_tag = solver.new_constraint_tag();

    let variables = (0..n)
        .map(|i| solver.new_named_bounded_integer(0, n as i32 - 1, format!("q{i}")))
        .collect::<Vec<_>>();

    let _ = solver
        .add_constraint(constraints::all_different(variables.clone(), c1_tag))
        .post();

    let diag1 = variables
        .iter()
        .cloned()
        .enumerate()
        .map(|(i, var)| var.offset(i as i32))
        .collect::<Vec<_>>();
    let diag2 = variables
        .iter()
        .cloned()
        .enumerate()
        .map(|(i, var)| var.offset(-(i as i32)))
        .collect::<Vec<_>>();

    let _ = solver
        .add_constraint(constraints::all_different(diag1, c2_tag))
        .post();
    let _ = solver
        .add_constraint(constraints::all_different(diag2, c3_tag))
        .post();

    let mut brancher = solver.default_brancher();
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(satisfiable) => {
            let solution = satisfiable.solution();

            let row_separator = format!("{}+", "+---".repeat(n as usize));

            for row in 0..n {
                println!("{row_separator}");

                let queen_col = solution.get_integer_value(variables[row as usize]) as u32;

                for col in 0..n {
                    let string = if queen_col == col { "| * " } else { "|   " };

                    print!("{string}");
                }

                println!("|");
            }

            println!("{row_separator}");
        }
        SatisfactionResult::Unsatisfiable(_, _) => {
            println!("{n}-queens is unsatisfiable.");
        }
        SatisfactionResult::Unknown(_, _) => {
            println!("Timeout.");
        }
    };
}

pub fn dimacs(file_path: &Path) -> Result<ProofLog, Error>

Create a dimacs proof logger.

Trait Implementations

impl Debug for ProofLog

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl Default for ProofLog

fn default() -> ProofLog

Returns the “default value” for a type.