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: SolverOptions) -> Self

Creates a solver with the provided SolverOptions.

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

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

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

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: &[Predicate], ) -> 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 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.

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

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.

impl Solver

Default brancher implementation

pub fn default_brancher(&self) -> DefaultBrancher

Creates an instance of the DefaultBrancher.

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

Formats the value using the given formatter.

impl Default for Solver

fn default() -> Self

Returns the “default value” for a type.