Struct Solver 

pub struct Solver { /* private fields */ }

The main interaction point which allows the creation of variables, the addition of constraints, and solving problems.

Creating Variables

As stated in crate::variables, we can create two types of variables: propositional variables and integer variables.

let mut solver = Solver::default();

// Integer Variables

// We can create an integer variable with a domain in the range [0, 10]
let integer_between_bounds = solver.new_bounded_integer(0, 10);

// We can also create such a variable with a name
let named_integer_between_bounds = solver.new_named_bounded_integer(0, 10, "x");

// We can also create an integer variable with a non-continuous domain in the follow way
let mut sparse_integer = solver.new_sparse_integer(vec![0, 3, 5]);

// We can also create such a variable with a name
let named_sparse_integer = solver.new_named_sparse_integer(vec![0, 3, 5], "y");

// Additionally, we can also create an affine view over a variable with both a scale and an offset (or either)
let view_over_integer = integer_between_bounds.scaled(-1).offset(15);


// Propositional Variable

// We can create a literal
let literal = solver.new_literal();

// We can also create such a variable with a name
let named_literal = solver.new_named_literal("z");

// We can also get the predicate from the literal
let true_predicate = literal.get_true_predicate();

// We can also create an iterator of new literals and get a number of them at once
let list_of_5_literals = solver.new_literals().take(5).collect::<Vec<_>>();
assert_eq!(list_of_5_literals.len(), 5);

Using the Solver

For examples on how to use the solver, see the root-level crate documentation or one of these examples.

Implementations

impl Solver

pub fn with_options(solver_options: SatisfactionSolverOptions) -> Solver

Creates a solver with the provided SolverOptions.

Examples found in repository

examples/nqueens.rs (lines 49-52)

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 log_statistics_with_objective( &self, brancher: Option<&impl Brancher>, objective_value: i64, verbose: bool, )

Logs the statistics currently present in the solver with the provided objective value.

pub fn log_statistics(&self, brancher: Option<&impl Brancher>, verbose: bool)

Logs the statistics currently present in the solver.

pub fn get_solution_reference(&self) -> SolutionReference<'_>

impl Solver

Methods to retrieve information about variables

pub fn get_literal_value(&self, literal: Literal) -> Option<bool>

Get the value of the given Literal at the root level (after propagation), which could be unassigned.

pub fn lower_bound(&self, variable: &impl IntegerVariable) -> i32

Get the lower-bound of the given IntegerVariable at the root level (after propagation).

pub fn upper_bound(&self, variable: &impl IntegerVariable) -> i32

Get the upper-bound of the given IntegerVariable at the root level (after propagation).

impl Solver

Functions to create and retrieve integer and propositional variables.

pub fn new_literals(&mut self) -> impl Iterator<Item = Literal>

Returns an infinite iterator of positive literals of new variables. The new variables will be unnamed.

Example

let mut solver = Solver::default();
let literals: Vec<Literal> = solver.new_literals().take(5).collect();

// `literals` contains 5 positive literals of newly created propositional variables.
assert_eq!(literals.len(), 5);

Note that this method captures the lifetime of the immutable reference to self.

pub fn new_literal(&mut self) -> Literal

Create a fresh propositional variable and return the literal with positive polarity.

Example

let mut solver = Solver::default();

// We can create a literal
let literal = solver.new_literal();

Examples found in repository

examples/disjunctive_scheduling.rs (line 56)

fn main() {
    let mut args = std::env::args();

    let n_tasks = args
        .nth(1)
        .expect("Please provide a number of tasks")
        .parse::<usize>()
        .expect("Not a valid usized");
    let processing_times = args
        .take(n_tasks)
        .map(|arg| arg.parse::<usize>())
        .collect::<Result<Vec<_>, _>>()
        .expect("The provided processing times are not valid unsigned integers");
    assert_eq!(
        processing_times.len(),
        n_tasks,
        "Provided fewer than `n_tasks` processing times."
    );

    let horizon = processing_times.iter().sum::<usize>();

    let mut solver = Solver::default();

    // Creates a dummy constraint tag; since this example does not support proof logging the
    // constraint tag does not matter.
    let constraint_tag = solver.new_constraint_tag();

    let start_variables = (0..n_tasks)
        .map(|i| solver.new_bounded_integer(0, (horizon - processing_times[i]) as i32))
        .collect::<Vec<_>>();

    // Literal which indicates precedence (i.e. precedence_literals[x][y] <=> x ends before y
    // starts)
    let precedence_literals = (0..n_tasks)
        .map(|_| {
            (0..n_tasks)
                .map(|_| solver.new_literal())
                .collect::<Vec<_>>()
        })
        .collect::<Vec<_>>();

    for x in 0..n_tasks {
        for y in 0..n_tasks {
            if x == y {
                continue;
            }
            // precedence_literals[x][y] <=> x ends before y starts
            let literal = precedence_literals[x][y];
            // literal <=> (s_x + p_x <= s_y)
            // equivelent to literal <=> (s_x - s_y <= -p_x)
            // So the variables are -s_y and s_x, and the rhs is -p_x
            let variables = vec![start_variables[y].scaled(-1), start_variables[x].scaled(1)];
            let _ = constraints::less_than_or_equals(
                variables,
                -(processing_times[x] as i32),
                constraint_tag,
            )
            .reify(&mut solver, literal);

            // Either x starts before y or y start before x
            let _ = solver.add_clause(
                [
                    literal.get_true_predicate(),
                    precedence_literals[y][x].get_true_predicate(),
                ],
                constraint_tag,
            );
        }
    }

    let mut brancher = solver.default_brancher();
    if matches!(
        solver.satisfy(&mut brancher, &mut Indefinite),
        SatisfactionResult::Unsatisfiable(_, _),
    ) {
        panic!("Infeasibility Detected")
    }
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(satisfiable) => {
            let solution = satisfiable.solution();

            let mut start_variables_and_processing_times = start_variables
                .iter()
                .zip(processing_times)
                .collect::<Vec<_>>();
            start_variables_and_processing_times.sort_by(|(s1, _), (s2, _)| {
                solution
                    .get_integer_value(**s1)
                    .cmp(&solution.get_integer_value(**s2))
            });

            println!(
                "{}",
                start_variables_and_processing_times
                    .iter()
                    .map(|(var, processing_time)| format!(
                        "[{}, {}]",
                        solution.get_integer_value(**var),
                        solution.get_integer_value(**var) + *processing_time as i32
                    ))
                    .collect::<Vec<_>>()
                    .join(" - ")
            );
        }
        SatisfactionResult::Unsatisfiable(_, _) => panic!("Infeasibility Detected"),
        SatisfactionResult::Unknown(_, _) => println!("Timeout."),
    };
}

pub fn new_literal_for_predicate( &mut self, predicate: Predicate, constraint_tag: ConstraintTag, ) -> Literal

pub fn new_named_literal(&mut self, name: impl Into<String>) -> Literal

Create a fresh propositional variable with a given name and return the literal with positive polarity.

Example

let mut solver = Solver::default();

// We can also create such a variable with a name
let named_literal = solver.new_named_literal("z");

pub fn get_true_literal(&self) -> Literal

Get a literal which is always true.

pub fn get_false_literal(&self) -> Literal

Get a literal which is always false.

pub fn new_bounded_integer( &mut self, lower_bound: i32, upper_bound: i32, ) -> DomainId

Create a new integer variable with the given bounds.

Example

let mut solver = Solver::default();

// We can create an integer variable with a domain in the range [0, 10]
let integer_between_bounds = solver.new_bounded_integer(0, 10);

Examples found in repository

examples/bibd.rs (line 69)

fn create_matrix(solver: &mut Solver, bibd: &Bibd) -> Vec<Vec<DomainId>> {
    (0..bibd.rows)
        .map(|_| {
            (0..bibd.columns)
                .map(|_| solver.new_bounded_integer(0, 1))
                .collect::<Vec<_>>()
        })
        .collect::<Vec<_>>()
}

examples/disjunctive_scheduling.rs (line 48)

fn main() {
    let mut args = std::env::args();

    let n_tasks = args
        .nth(1)
        .expect("Please provide a number of tasks")
        .parse::<usize>()
        .expect("Not a valid usized");
    let processing_times = args
        .take(n_tasks)
        .map(|arg| arg.parse::<usize>())
        .collect::<Result<Vec<_>, _>>()
        .expect("The provided processing times are not valid unsigned integers");
    assert_eq!(
        processing_times.len(),
        n_tasks,
        "Provided fewer than `n_tasks` processing times."
    );

    let horizon = processing_times.iter().sum::<usize>();

    let mut solver = Solver::default();

    // Creates a dummy constraint tag; since this example does not support proof logging the
    // constraint tag does not matter.
    let constraint_tag = solver.new_constraint_tag();

    let start_variables = (0..n_tasks)
        .map(|i| solver.new_bounded_integer(0, (horizon - processing_times[i]) as i32))
        .collect::<Vec<_>>();

    // Literal which indicates precedence (i.e. precedence_literals[x][y] <=> x ends before y
    // starts)
    let precedence_literals = (0..n_tasks)
        .map(|_| {
            (0..n_tasks)
                .map(|_| solver.new_literal())
                .collect::<Vec<_>>()
        })
        .collect::<Vec<_>>();

    for x in 0..n_tasks {
        for y in 0..n_tasks {
            if x == y {
                continue;
            }
            // precedence_literals[x][y] <=> x ends before y starts
            let literal = precedence_literals[x][y];
            // literal <=> (s_x + p_x <= s_y)
            // equivelent to literal <=> (s_x - s_y <= -p_x)
            // So the variables are -s_y and s_x, and the rhs is -p_x
            let variables = vec![start_variables[y].scaled(-1), start_variables[x].scaled(1)];
            let _ = constraints::less_than_or_equals(
                variables,
                -(processing_times[x] as i32),
                constraint_tag,
            )
            .reify(&mut solver, literal);

            // Either x starts before y or y start before x
            let _ = solver.add_clause(
                [
                    literal.get_true_predicate(),
                    precedence_literals[y][x].get_true_predicate(),
                ],
                constraint_tag,
            );
        }
    }

    let mut brancher = solver.default_brancher();
    if matches!(
        solver.satisfy(&mut brancher, &mut Indefinite),
        SatisfactionResult::Unsatisfiable(_, _),
    ) {
        panic!("Infeasibility Detected")
    }
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(satisfiable) => {
            let solution = satisfiable.solution();

            let mut start_variables_and_processing_times = start_variables
                .iter()
                .zip(processing_times)
                .collect::<Vec<_>>();
            start_variables_and_processing_times.sort_by(|(s1, _), (s2, _)| {
                solution
                    .get_integer_value(**s1)
                    .cmp(&solution.get_integer_value(**s2))
            });

            println!(
                "{}",
                start_variables_and_processing_times
                    .iter()
                    .map(|(var, processing_time)| format!(
                        "[{}, {}]",
                        solution.get_integer_value(**var),
                        solution.get_integer_value(**var) + *processing_time as i32
                    ))
                    .collect::<Vec<_>>()
                    .join(" - ")
            );
        }
        SatisfactionResult::Unsatisfiable(_, _) => panic!("Infeasibility Detected"),
        SatisfactionResult::Unknown(_, _) => println!("Timeout."),
    };
}

pub fn new_named_bounded_integer( &mut self, lower_bound: i32, upper_bound: i32, name: impl Into<String>, ) -> DomainId

Create a new named integer variable with the given bounds.

Example

let mut solver = Solver::default();

// We can also create such a variable with a name
let named_integer_between_bounds = solver.new_named_bounded_integer(0, 10, "x");

Examples found in repository

examples/nqueens.rs (line 60)

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 new_sparse_integer(&mut self, values: impl Into<Vec<i32>>) -> DomainId

Create a new integer variable which has a domain of predefined values. We remove duplicates by converting to a hash set

Example

let mut solver = Solver::default();

// We can also create an integer variable with a non-continuous domain in the follow way
let mut sparse_integer = solver.new_sparse_integer(vec![0, 3, 5]);

pub fn new_named_sparse_integer( &mut self, values: impl Into<Vec<i32>>, name: impl Into<String>, ) -> DomainId

Create a new named integer variable which has a domain of predefined values.

Example

let mut solver = Solver::default();

// We can also create such a variable with a name
let named_sparse_integer = solver.new_named_sparse_integer(vec![0, 3, 5], "y");

impl Solver

Functions for solving with the constraints that have been added to the Solver.

pub fn satisfy<'this, 'brancher, B, T>( &'this mut self, brancher: &'brancher mut B, termination: &mut T, ) -> SatisfactionResult<'this, 'brancher, B>

where B: Brancher, T: TerminationCondition,

Solves the current model in the Solver until it finds a solution (or is indicated to terminate by the provided TerminationCondition) and returns a SatisfactionResult which can be used to obtain the found solution or find other solutions.

Examples found in repository

examples/nqueens.rs (line 88)

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.");
        }
    };
}

examples/bibd.rs (line 149)

fn main() {
    env_logger::init();

    let Some(bibd) = Bibd::from_args() else {
        eprintln!("Usage: {} <v> <k> <l>", std::env::args().next().unwrap());
        return;
    };

    println!(
        "bibd: (v = {}, b = {}, r = {}, k = {}, l = {})",
        bibd.rows, bibd.columns, bibd.row_sum, bibd.column_sum, bibd.max_dot_product
    );

    let mut solver = Solver::default();

    // Creates a dummy constraint tag; since this example does not support proof logging the
    // constraint tag does not matter.
    let constraint_tag = solver.new_constraint_tag();

    // Create 0-1 integer variables that make up the matrix.
    let matrix = create_matrix(&mut solver, &bibd);

    // Enforce the row sum.
    for row in matrix.iter() {
        let _ = solver
            .add_constraint(constraints::equals(
                row.clone(),
                bibd.row_sum as i32,
                constraint_tag,
            ))
            .post();
    }

    // Enforce the column sum.
    for row in transpose(&matrix) {
        let _ = solver
            .add_constraint(constraints::equals(
                row,
                bibd.column_sum as i32,
                constraint_tag,
            ))
            .post();
    }

    // Enforce the dot product constraint.
    // pairwise_product[r1][r2][col] = matrix[r1][col] * matrix[r2][col]
    let pairwise_product = (0..bibd.rows)
        .map(|_| create_matrix(&mut solver, &bibd))
        .collect::<Vec<_>>();

    for r1 in 0..bibd.rows as usize {
        for r2 in r1 + 1..bibd.rows as usize {
            for col in 0..bibd.columns as usize {
                let _ = solver
                    .add_constraint(constraints::times(
                        matrix[r1][col],
                        matrix[r2][col],
                        pairwise_product[r1][r2][col],
                        constraint_tag,
                    ))
                    .post();
            }

            let _ = solver
                .add_constraint(constraints::less_than_or_equals(
                    pairwise_product[r1][r2].clone(),
                    bibd.max_dot_product as i32,
                    constraint_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(bibd.columns as usize));

            for row in matrix.iter() {
                let line = row
                    .iter()
                    .map(|var| {
                        if solution.get_integer_value(*var) == 1 {
                            String::from("| * ")
                        } else {
                            String::from("|   ")
                        }
                    })
                    .collect::<String>();

                println!("{row_separator}\n{line}|");
            }

            println!("{row_separator}");
        }
        SatisfactionResult::Unsatisfiable(_, _) => {
            println!("UNSATISFIABLE")
        }
        SatisfactionResult::Unknown(_, _) => {
            println!("UNKNOWN")
        }
    };
}

examples/disjunctive_scheduling.rs (line 92)

fn main() {
    let mut args = std::env::args();

    let n_tasks = args
        .nth(1)
        .expect("Please provide a number of tasks")
        .parse::<usize>()
        .expect("Not a valid usized");
    let processing_times = args
        .take(n_tasks)
        .map(|arg| arg.parse::<usize>())
        .collect::<Result<Vec<_>, _>>()
        .expect("The provided processing times are not valid unsigned integers");
    assert_eq!(
        processing_times.len(),
        n_tasks,
        "Provided fewer than `n_tasks` processing times."
    );

    let horizon = processing_times.iter().sum::<usize>();

    let mut solver = Solver::default();

    // Creates a dummy constraint tag; since this example does not support proof logging the
    // constraint tag does not matter.
    let constraint_tag = solver.new_constraint_tag();

    let start_variables = (0..n_tasks)
        .map(|i| solver.new_bounded_integer(0, (horizon - processing_times[i]) as i32))
        .collect::<Vec<_>>();

    // Literal which indicates precedence (i.e. precedence_literals[x][y] <=> x ends before y
    // starts)
    let precedence_literals = (0..n_tasks)
        .map(|_| {
            (0..n_tasks)
                .map(|_| solver.new_literal())
                .collect::<Vec<_>>()
        })
        .collect::<Vec<_>>();

    for x in 0..n_tasks {
        for y in 0..n_tasks {
            if x == y {
                continue;
            }
            // precedence_literals[x][y] <=> x ends before y starts
            let literal = precedence_literals[x][y];
            // literal <=> (s_x + p_x <= s_y)
            // equivelent to literal <=> (s_x - s_y <= -p_x)
            // So the variables are -s_y and s_x, and the rhs is -p_x
            let variables = vec![start_variables[y].scaled(-1), start_variables[x].scaled(1)];
            let _ = constraints::less_than_or_equals(
                variables,
                -(processing_times[x] as i32),
                constraint_tag,
            )
            .reify(&mut solver, literal);

            // Either x starts before y or y start before x
            let _ = solver.add_clause(
                [
                    literal.get_true_predicate(),
                    precedence_literals[y][x].get_true_predicate(),
                ],
                constraint_tag,
            );
        }
    }

    let mut brancher = solver.default_brancher();
    if matches!(
        solver.satisfy(&mut brancher, &mut Indefinite),
        SatisfactionResult::Unsatisfiable(_, _),
    ) {
        panic!("Infeasibility Detected")
    }
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(satisfiable) => {
            let solution = satisfiable.solution();

            let mut start_variables_and_processing_times = start_variables
                .iter()
                .zip(processing_times)
                .collect::<Vec<_>>();
            start_variables_and_processing_times.sort_by(|(s1, _), (s2, _)| {
                solution
                    .get_integer_value(**s1)
                    .cmp(&solution.get_integer_value(**s2))
            });

            println!(
                "{}",
                start_variables_and_processing_times
                    .iter()
                    .map(|(var, processing_time)| format!(
                        "[{}, {}]",
                        solution.get_integer_value(**var),
                        solution.get_integer_value(**var) + *processing_time as i32
                    ))
                    .collect::<Vec<_>>()
                    .join(" - ")
            );
        }
        SatisfactionResult::Unsatisfiable(_, _) => panic!("Infeasibility Detected"),
        SatisfactionResult::Unknown(_, _) => println!("Timeout."),
    };
}

pub fn get_solution_iterator<'this, 'brancher, 'termination, B, T>( &'this mut self, brancher: &'brancher mut B, termination: &'termination mut T, ) -> SolutionIterator<'this, 'brancher, 'termination, B, T>

where B: Brancher, T: TerminationCondition,

pub fn satisfy_under_assumptions<'this, 'brancher, B, T>( &'this mut self, brancher: &'brancher mut B, termination: &mut T, assumptions: &[Predicate], ) -> SatisfactionResultUnderAssumptions<'this, 'brancher, B>

where B: Brancher, T: TerminationCondition,

Solves the current model in the Solver until it finds a solution (or is indicated to terminate by the provided TerminationCondition) and returns a SatisfactionResult which can be used to obtain the found solution or find other solutions.

This method takes as input a list of Predicates which represent so-called assumptions (see [1] for a more detailed explanation). See the [predicates] documentation for how to construct these predicates.

Bibliography

[1] N. Eén and N. Sörensson, ‘Temporal induction by incremental SAT solving’, Electronic Notes in Theoretical Computer Science, vol. 89, no. 4, pp. 543–560, 2003.

pub fn optimise<B, Callback>( &mut self, brancher: &mut B, termination: &mut impl TerminationCondition, optimisation_procedure: impl OptimisationProcedure<B, Callback>, ) -> OptimisationResult

where B: Brancher, Callback: SolutionCallback<B>,

Solves the model currently in the Solver to optimality where the provided objective_variable is optimised as indicated by the direction (or is indicated to terminate by the provided TerminationCondition). Uses a search strategy based on the provided OptimisationProcedure, currently [LinearSatUnsat] and [LinearUnsatSat] are supported.

It returns an OptimisationResult which can be used to retrieve the optimal solution if it exists.

impl Solver

Functions for adding new constraints to the solver.

pub fn new_constraint_tag(&mut self) -> ConstraintTag

Creates a new ConstraintTag that can be used to add constraints to the solver.

See the ConstraintTag documentation for information on how the tags are used.

Examples found in repository

examples/nqueens.rs (line 55)

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.");
        }
    };
}

examples/bibd.rs (line 92)

fn main() {
    env_logger::init();

    let Some(bibd) = Bibd::from_args() else {
        eprintln!("Usage: {} <v> <k> <l>", std::env::args().next().unwrap());
        return;
    };

    println!(
        "bibd: (v = {}, b = {}, r = {}, k = {}, l = {})",
        bibd.rows, bibd.columns, bibd.row_sum, bibd.column_sum, bibd.max_dot_product
    );

    let mut solver = Solver::default();

    // Creates a dummy constraint tag; since this example does not support proof logging the
    // constraint tag does not matter.
    let constraint_tag = solver.new_constraint_tag();

    // Create 0-1 integer variables that make up the matrix.
    let matrix = create_matrix(&mut solver, &bibd);

    // Enforce the row sum.
    for row in matrix.iter() {
        let _ = solver
            .add_constraint(constraints::equals(
                row.clone(),
                bibd.row_sum as i32,
                constraint_tag,
            ))
            .post();
    }

    // Enforce the column sum.
    for row in transpose(&matrix) {
        let _ = solver
            .add_constraint(constraints::equals(
                row,
                bibd.column_sum as i32,
                constraint_tag,
            ))
            .post();
    }

    // Enforce the dot product constraint.
    // pairwise_product[r1][r2][col] = matrix[r1][col] * matrix[r2][col]
    let pairwise_product = (0..bibd.rows)
        .map(|_| create_matrix(&mut solver, &bibd))
        .collect::<Vec<_>>();

    for r1 in 0..bibd.rows as usize {
        for r2 in r1 + 1..bibd.rows as usize {
            for col in 0..bibd.columns as usize {
                let _ = solver
                    .add_constraint(constraints::times(
                        matrix[r1][col],
                        matrix[r2][col],
                        pairwise_product[r1][r2][col],
                        constraint_tag,
                    ))
                    .post();
            }

            let _ = solver
                .add_constraint(constraints::less_than_or_equals(
                    pairwise_product[r1][r2].clone(),
                    bibd.max_dot_product as i32,
                    constraint_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(bibd.columns as usize));

            for row in matrix.iter() {
                let line = row
                    .iter()
                    .map(|var| {
                        if solution.get_integer_value(*var) == 1 {
                            String::from("| * ")
                        } else {
                            String::from("|   ")
                        }
                    })
                    .collect::<String>();

                println!("{row_separator}\n{line}|");
            }

            println!("{row_separator}");
        }
        SatisfactionResult::Unsatisfiable(_, _) => {
            println!("UNSATISFIABLE")
        }
        SatisfactionResult::Unknown(_, _) => {
            println!("UNKNOWN")
        }
    };
}

examples/disjunctive_scheduling.rs (line 45)

fn main() {
    let mut args = std::env::args();

    let n_tasks = args
        .nth(1)
        .expect("Please provide a number of tasks")
        .parse::<usize>()
        .expect("Not a valid usized");
    let processing_times = args
        .take(n_tasks)
        .map(|arg| arg.parse::<usize>())
        .collect::<Result<Vec<_>, _>>()
        .expect("The provided processing times are not valid unsigned integers");
    assert_eq!(
        processing_times.len(),
        n_tasks,
        "Provided fewer than `n_tasks` processing times."
    );

    let horizon = processing_times.iter().sum::<usize>();

    let mut solver = Solver::default();

    // Creates a dummy constraint tag; since this example does not support proof logging the
    // constraint tag does not matter.
    let constraint_tag = solver.new_constraint_tag();

    let start_variables = (0..n_tasks)
        .map(|i| solver.new_bounded_integer(0, (horizon - processing_times[i]) as i32))
        .collect::<Vec<_>>();

    // Literal which indicates precedence (i.e. precedence_literals[x][y] <=> x ends before y
    // starts)
    let precedence_literals = (0..n_tasks)
        .map(|_| {
            (0..n_tasks)
                .map(|_| solver.new_literal())
                .collect::<Vec<_>>()
        })
        .collect::<Vec<_>>();

    for x in 0..n_tasks {
        for y in 0..n_tasks {
            if x == y {
                continue;
            }
            // precedence_literals[x][y] <=> x ends before y starts
            let literal = precedence_literals[x][y];
            // literal <=> (s_x + p_x <= s_y)
            // equivelent to literal <=> (s_x - s_y <= -p_x)
            // So the variables are -s_y and s_x, and the rhs is -p_x
            let variables = vec![start_variables[y].scaled(-1), start_variables[x].scaled(1)];
            let _ = constraints::less_than_or_equals(
                variables,
                -(processing_times[x] as i32),
                constraint_tag,
            )
            .reify(&mut solver, literal);

            // Either x starts before y or y start before x
            let _ = solver.add_clause(
                [
                    literal.get_true_predicate(),
                    precedence_literals[y][x].get_true_predicate(),
                ],
                constraint_tag,
            );
        }
    }

    let mut brancher = solver.default_brancher();
    if matches!(
        solver.satisfy(&mut brancher, &mut Indefinite),
        SatisfactionResult::Unsatisfiable(_, _),
    ) {
        panic!("Infeasibility Detected")
    }
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(satisfiable) => {
            let solution = satisfiable.solution();

            let mut start_variables_and_processing_times = start_variables
                .iter()
                .zip(processing_times)
                .collect::<Vec<_>>();
            start_variables_and_processing_times.sort_by(|(s1, _), (s2, _)| {
                solution
                    .get_integer_value(**s1)
                    .cmp(&solution.get_integer_value(**s2))
            });

            println!(
                "{}",
                start_variables_and_processing_times
                    .iter()
                    .map(|(var, processing_time)| format!(
                        "[{}, {}]",
                        solution.get_integer_value(**var),
                        solution.get_integer_value(**var) + *processing_time as i32
                    ))
                    .collect::<Vec<_>>()
                    .join(" - ")
            );
        }
        SatisfactionResult::Unsatisfiable(_, _) => panic!("Infeasibility Detected"),
        SatisfactionResult::Unknown(_, _) => println!("Timeout."),
    };
}

pub fn add_constraint<Constraint>( &mut self, constraint: Constraint, ) -> ConstraintPoster<'_, Constraint>

Add a constraint to the solver. This returns a ConstraintPoster which enables control on whether to add the constraint as-is, or whether to (half) reify it.

All constraints require a ConstraintTag to be supplied. See its documentation for more information.

If none of the methods on ConstraintPoster are used, the constraint is not actually added to the solver. In this case, a warning is emitted.

Example

let mut solver = Solver::default();

let a = solver.new_bounded_integer(0, 3);
let b = solver.new_bounded_integer(0, 3);

let constraint_tag = solver.new_constraint_tag();

solver
    .add_constraint(constraints::equals([a, b], 0, constraint_tag))
    .post();

Examples found in repository

examples/nqueens.rs (line 64)

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.");
        }
    };
}

examples/bibd.rs (lines 100-104)

fn main() {
    env_logger::init();

    let Some(bibd) = Bibd::from_args() else {
        eprintln!("Usage: {} <v> <k> <l>", std::env::args().next().unwrap());
        return;
    };

    println!(
        "bibd: (v = {}, b = {}, r = {}, k = {}, l = {})",
        bibd.rows, bibd.columns, bibd.row_sum, bibd.column_sum, bibd.max_dot_product
    );

    let mut solver = Solver::default();

    // Creates a dummy constraint tag; since this example does not support proof logging the
    // constraint tag does not matter.
    let constraint_tag = solver.new_constraint_tag();

    // Create 0-1 integer variables that make up the matrix.
    let matrix = create_matrix(&mut solver, &bibd);

    // Enforce the row sum.
    for row in matrix.iter() {
        let _ = solver
            .add_constraint(constraints::equals(
                row.clone(),
                bibd.row_sum as i32,
                constraint_tag,
            ))
            .post();
    }

    // Enforce the column sum.
    for row in transpose(&matrix) {
        let _ = solver
            .add_constraint(constraints::equals(
                row,
                bibd.column_sum as i32,
                constraint_tag,
            ))
            .post();
    }

    // Enforce the dot product constraint.
    // pairwise_product[r1][r2][col] = matrix[r1][col] * matrix[r2][col]
    let pairwise_product = (0..bibd.rows)
        .map(|_| create_matrix(&mut solver, &bibd))
        .collect::<Vec<_>>();

    for r1 in 0..bibd.rows as usize {
        for r2 in r1 + 1..bibd.rows as usize {
            for col in 0..bibd.columns as usize {
                let _ = solver
                    .add_constraint(constraints::times(
                        matrix[r1][col],
                        matrix[r2][col],
                        pairwise_product[r1][r2][col],
                        constraint_tag,
                    ))
                    .post();
            }

            let _ = solver
                .add_constraint(constraints::less_than_or_equals(
                    pairwise_product[r1][r2].clone(),
                    bibd.max_dot_product as i32,
                    constraint_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(bibd.columns as usize));

            for row in matrix.iter() {
                let line = row
                    .iter()
                    .map(|var| {
                        if solution.get_integer_value(*var) == 1 {
                            String::from("| * ")
                        } else {
                            String::from("|   ")
                        }
                    })
                    .collect::<String>();

                println!("{row_separator}\n{line}|");
            }

            println!("{row_separator}");
        }
        SatisfactionResult::Unsatisfiable(_, _) => {
            println!("UNSATISFIABLE")
        }
        SatisfactionResult::Unknown(_, _) => {
            println!("UNKNOWN")
        }
    };
}

pub fn add_clause( &mut self, clause: impl IntoIterator<Item = Predicate>, constraint_tag: ConstraintTag, ) -> Result<(), ConstraintOperationError>

Creates a clause from literals and adds it to the current formula.

If the formula becomes trivially unsatisfiable, a ConstraintOperationError will be returned. Subsequent calls to this method will always return an error, and no modification of the solver will take place.

Examples found in repository

examples/disjunctive_scheduling.rs (lines 80-86)

fn main() {
    let mut args = std::env::args();

    let n_tasks = args
        .nth(1)
        .expect("Please provide a number of tasks")
        .parse::<usize>()
        .expect("Not a valid usized");
    let processing_times = args
        .take(n_tasks)
        .map(|arg| arg.parse::<usize>())
        .collect::<Result<Vec<_>, _>>()
        .expect("The provided processing times are not valid unsigned integers");
    assert_eq!(
        processing_times.len(),
        n_tasks,
        "Provided fewer than `n_tasks` processing times."
    );

    let horizon = processing_times.iter().sum::<usize>();

    let mut solver = Solver::default();

    // Creates a dummy constraint tag; since this example does not support proof logging the
    // constraint tag does not matter.
    let constraint_tag = solver.new_constraint_tag();

    let start_variables = (0..n_tasks)
        .map(|i| solver.new_bounded_integer(0, (horizon - processing_times[i]) as i32))
        .collect::<Vec<_>>();

    // Literal which indicates precedence (i.e. precedence_literals[x][y] <=> x ends before y
    // starts)
    let precedence_literals = (0..n_tasks)
        .map(|_| {
            (0..n_tasks)
                .map(|_| solver.new_literal())
                .collect::<Vec<_>>()
        })
        .collect::<Vec<_>>();

    for x in 0..n_tasks {
        for y in 0..n_tasks {
            if x == y {
                continue;
            }
            // precedence_literals[x][y] <=> x ends before y starts
            let literal = precedence_literals[x][y];
            // literal <=> (s_x + p_x <= s_y)
            // equivelent to literal <=> (s_x - s_y <= -p_x)
            // So the variables are -s_y and s_x, and the rhs is -p_x
            let variables = vec![start_variables[y].scaled(-1), start_variables[x].scaled(1)];
            let _ = constraints::less_than_or_equals(
                variables,
                -(processing_times[x] as i32),
                constraint_tag,
            )
            .reify(&mut solver, literal);

            // Either x starts before y or y start before x
            let _ = solver.add_clause(
                [
                    literal.get_true_predicate(),
                    precedence_literals[y][x].get_true_predicate(),
                ],
                constraint_tag,
            );
        }
    }

    let mut brancher = solver.default_brancher();
    if matches!(
        solver.satisfy(&mut brancher, &mut Indefinite),
        SatisfactionResult::Unsatisfiable(_, _),
    ) {
        panic!("Infeasibility Detected")
    }
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(satisfiable) => {
            let solution = satisfiable.solution();

            let mut start_variables_and_processing_times = start_variables
                .iter()
                .zip(processing_times)
                .collect::<Vec<_>>();
            start_variables_and_processing_times.sort_by(|(s1, _), (s2, _)| {
                solution
                    .get_integer_value(**s1)
                    .cmp(&solution.get_integer_value(**s2))
            });

            println!(
                "{}",
                start_variables_and_processing_times
                    .iter()
                    .map(|(var, processing_time)| format!(
                        "[{}, {}]",
                        solution.get_integer_value(**var),
                        solution.get_integer_value(**var) + *processing_time as i32
                    ))
                    .collect::<Vec<_>>()
                    .join(" - ")
            );
        }
        SatisfactionResult::Unsatisfiable(_, _) => panic!("Infeasibility Detected"),
        SatisfactionResult::Unknown(_, _) => println!("Timeout."),
    };
}

impl Solver

Default brancher implementation

pub fn default_brancher( &self, ) -> AutonomousSearch<IndependentVariableValueBrancher<DomainId, RandomSelector, RandomSplitter>>

Creates an instance of the DefaultBrancher.

Examples found in repository

examples/nqueens.rs (line 87)

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.");
        }
    };
}

examples/bibd.rs (line 148)

fn main() {
    env_logger::init();

    let Some(bibd) = Bibd::from_args() else {
        eprintln!("Usage: {} <v> <k> <l>", std::env::args().next().unwrap());
        return;
    };

    println!(
        "bibd: (v = {}, b = {}, r = {}, k = {}, l = {})",
        bibd.rows, bibd.columns, bibd.row_sum, bibd.column_sum, bibd.max_dot_product
    );

    let mut solver = Solver::default();

    // Creates a dummy constraint tag; since this example does not support proof logging the
    // constraint tag does not matter.
    let constraint_tag = solver.new_constraint_tag();

    // Create 0-1 integer variables that make up the matrix.
    let matrix = create_matrix(&mut solver, &bibd);

    // Enforce the row sum.
    for row in matrix.iter() {
        let _ = solver
            .add_constraint(constraints::equals(
                row.clone(),
                bibd.row_sum as i32,
                constraint_tag,
            ))
            .post();
    }

    // Enforce the column sum.
    for row in transpose(&matrix) {
        let _ = solver
            .add_constraint(constraints::equals(
                row,
                bibd.column_sum as i32,
                constraint_tag,
            ))
            .post();
    }

    // Enforce the dot product constraint.
    // pairwise_product[r1][r2][col] = matrix[r1][col] * matrix[r2][col]
    let pairwise_product = (0..bibd.rows)
        .map(|_| create_matrix(&mut solver, &bibd))
        .collect::<Vec<_>>();

    for r1 in 0..bibd.rows as usize {
        for r2 in r1 + 1..bibd.rows as usize {
            for col in 0..bibd.columns as usize {
                let _ = solver
                    .add_constraint(constraints::times(
                        matrix[r1][col],
                        matrix[r2][col],
                        pairwise_product[r1][r2][col],
                        constraint_tag,
                    ))
                    .post();
            }

            let _ = solver
                .add_constraint(constraints::less_than_or_equals(
                    pairwise_product[r1][r2].clone(),
                    bibd.max_dot_product as i32,
                    constraint_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(bibd.columns as usize));

            for row in matrix.iter() {
                let line = row
                    .iter()
                    .map(|var| {
                        if solution.get_integer_value(*var) == 1 {
                            String::from("| * ")
                        } else {
                            String::from("|   ")
                        }
                    })
                    .collect::<String>();

                println!("{row_separator}\n{line}|");
            }

            println!("{row_separator}");
        }
        SatisfactionResult::Unsatisfiable(_, _) => {
            println!("UNSATISFIABLE")
        }
        SatisfactionResult::Unknown(_, _) => {
            println!("UNKNOWN")
        }
    };
}

examples/disjunctive_scheduling.rs (line 90)

fn main() {
    let mut args = std::env::args();

    let n_tasks = args
        .nth(1)
        .expect("Please provide a number of tasks")
        .parse::<usize>()
        .expect("Not a valid usized");
    let processing_times = args
        .take(n_tasks)
        .map(|arg| arg.parse::<usize>())
        .collect::<Result<Vec<_>, _>>()
        .expect("The provided processing times are not valid unsigned integers");
    assert_eq!(
        processing_times.len(),
        n_tasks,
        "Provided fewer than `n_tasks` processing times."
    );

    let horizon = processing_times.iter().sum::<usize>();

    let mut solver = Solver::default();

    // Creates a dummy constraint tag; since this example does not support proof logging the
    // constraint tag does not matter.
    let constraint_tag = solver.new_constraint_tag();

    let start_variables = (0..n_tasks)
        .map(|i| solver.new_bounded_integer(0, (horizon - processing_times[i]) as i32))
        .collect::<Vec<_>>();

    // Literal which indicates precedence (i.e. precedence_literals[x][y] <=> x ends before y
    // starts)
    let precedence_literals = (0..n_tasks)
        .map(|_| {
            (0..n_tasks)
                .map(|_| solver.new_literal())
                .collect::<Vec<_>>()
        })
        .collect::<Vec<_>>();

    for x in 0..n_tasks {
        for y in 0..n_tasks {
            if x == y {
                continue;
            }
            // precedence_literals[x][y] <=> x ends before y starts
            let literal = precedence_literals[x][y];
            // literal <=> (s_x + p_x <= s_y)
            // equivelent to literal <=> (s_x - s_y <= -p_x)
            // So the variables are -s_y and s_x, and the rhs is -p_x
            let variables = vec![start_variables[y].scaled(-1), start_variables[x].scaled(1)];
            let _ = constraints::less_than_or_equals(
                variables,
                -(processing_times[x] as i32),
                constraint_tag,
            )
            .reify(&mut solver, literal);

            // Either x starts before y or y start before x
            let _ = solver.add_clause(
                [
                    literal.get_true_predicate(),
                    precedence_literals[y][x].get_true_predicate(),
                ],
                constraint_tag,
            );
        }
    }

    let mut brancher = solver.default_brancher();
    if matches!(
        solver.satisfy(&mut brancher, &mut Indefinite),
        SatisfactionResult::Unsatisfiable(_, _),
    ) {
        panic!("Infeasibility Detected")
    }
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(satisfiable) => {
            let solution = satisfiable.solution();

            let mut start_variables_and_processing_times = start_variables
                .iter()
                .zip(processing_times)
                .collect::<Vec<_>>();
            start_variables_and_processing_times.sort_by(|(s1, _), (s2, _)| {
                solution
                    .get_integer_value(**s1)
                    .cmp(&solution.get_integer_value(**s2))
            });

            println!(
                "{}",
                start_variables_and_processing_times
                    .iter()
                    .map(|(var, processing_time)| format!(
                        "[{}, {}]",
                        solution.get_integer_value(**var),
                        solution.get_integer_value(**var) + *processing_time as i32
                    ))
                    .collect::<Vec<_>>()
                    .join(" - ")
            );
        }
        SatisfactionResult::Unsatisfiable(_, _) => panic!("Infeasibility Detected"),
        SatisfactionResult::Unknown(_, _) => println!("Timeout."),
    };
}

impl Solver

Proof logging methods

pub fn conclude_proof_dual_bound(&mut self, bound: Predicate)

Conclude the proof with the optimality claim.

This method will finish the proof. Any new operation will not be logged to the proof.

Trait Implementations

impl Debug for Solver

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

Formats the value using the given formatter.

impl Default for Solver

fn default() -> Solver

Returns the “default value” for a type.