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 propositional variable from the literal
let propositional_variable = literal.get_propositional_variable();

// 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( learning_options: LearningOptions, solver_options: SolverOptions, ) -> Self

Creates a solver with the provided LearningOptions and SolverOptions.

pub fn with_solution_callback( &mut self, solution_callback: impl Fn(&Solution) + 'static, )

Adds a call-back to the Solver which is called every time that a solution is found when optimising using Solver::maximise or Solver::minimise.

Note that this will also perform the call-back on the optimal solution which is returned in OptimisationResult::Optimal.

pub fn log_statistics_with_objective(&self, objective_value: i64)

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

pub fn log_statistics(&self)

Logs the statistics currently present in the solver.

impl Solver

Methods to retrieve information about variables

pub fn get_literal(&self, predicate: Predicate) -> Literal

Get the literal corresponding to the given predicate. As the literal may need to be created, this possibly mutates the solver.

Example

let mut solver = Solver::default();

let x = solver.new_bounded_integer(0, 10);

// We can get the literal representing the predicate `[x >= 3]` via the Solver
let literal = solver.get_literal(predicate!(x >= 3));

// Note that we can also get a literal which is always true
let true_lower_bound_literal = solver.get_literal(predicate!(x >= 0));
assert_eq!(true_lower_bound_literal, solver.get_true_literal());

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 get_true_literal(&self) -> Literal

Get a literal which is globally true.

pub fn get_false_literal(&self) -> Literal

Get a literal which is globally false.

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();

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 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);

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

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<B: Brancher, T: TerminationCondition>( &mut self, brancher: &mut B, termination: &mut T, ) -> SatisfactionResult

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.

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

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

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 Literals which represent so-called assumptions (see [1] for a more detailed explanation). The Literals corresponding to Predicates over IntegerVariables (e.g. lower-bound predicates) can be retrieved from the Solver using Solver::get_literal.

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 minimise( &mut self, brancher: &mut impl Brancher, termination: &mut impl TerminationCondition, objective_variable: impl IntegerVariable, ) -> OptimisationResult

Solves the model currently in the Solver to optimality where the provided objective_variable is minimised (or is indicated to terminate by the provided TerminationCondition).

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

pub fn maximise( &mut self, brancher: &mut impl Brancher, termination: &mut impl TerminationCondition, objective_variable: impl IntegerVariable, ) -> OptimisationResult

Solves the model currently in the Solver to optimality where the provided objective_variable is maximised (or is indicated to terminate by the provided TerminationCondition).

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 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.

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);

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

pub fn add_clause( &mut self, clause: impl IntoIterator<Item = Literal>, ) -> 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.

impl Solver

Default brancher implementation

pub fn default_brancher_over_all_propositional_variables( &self, ) -> DefaultBrancher

Creates a default IndependentVariableValueBrancher which uses Vsids as VariableSelector and SolutionGuidedValueSelector (with PhaseSaving as its back-up selector) as its ValueSelector; it searches over all PropositionalVariables defined in the provided solver.

Trait Implementations

impl Debug for Solver

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

Formats the value using the given formatter.

impl Default for Solver

fn default() -> Self

Returns the “default value” for a type.