Module branching 

Contains structures and traits to define the decision making procedure of the [Solver].

In general, it provides 3 traits:

• The Brancher which defines how a branching procedure (which selects an unfixed variable and splits the domain in some way, see Section 4.3.1 of [1] for more information) should operate; the main method of this trait is the Brancher::next_decision method. An example implementation of this trait is the [IndependentVariableValueBrancher].
• The [VariableSelector] which defines the method required of a variable selector (including the hooks into the solver); the main method of this trait is the [VariableSelector::select_variable] method. An example implementation of this trait is the [AntiFirstFail] strategy.
• The [ValueSelector] which defines the method required of a value selector (including the hooks into the solver); the main method of this trait is the [ValueSelector::select_value] method.

A Brancher is expected to be passed to [Solver::satisfy], and [Solver::optimise]:

let mut solver = Solver::default();

let variables = vec![solver.new_literal()];

let mut termination = Indefinite;
let mut brancher = solver.default_brancher();
let result = solver.satisfy(&mut brancher, &mut termination);
if let SatisfactionResult::Satisfiable(satisfiable) = result {
    // Getting the value of the literal in the solution should not panic
    variables.into_iter().for_each(|variable| {
        satisfiable.solution().get_literal_value(variable);
    });
} else {
    panic!("Solving should have returned satsifiable")
}

A default implementation of a Brancher is provided using the method [Solver::default_brancher].

let mut solver = Solver::default();

let literals = vec![solver.new_literal()];

let mut termination = Indefinite;
let mut brancher = solver.default_brancher();
let result = solver.satisfy(&mut brancher, &mut termination);
if let SatisfactionResult::Satisfiable(satisfiable) = result {
    // Getting the value of the literal in the solution should not panic
    literals.into_iter().for_each(|literal| {
        satisfiable.solution().get_literal_value(literal);
    })
} else {
    panic!("Solving should have returned satsifiable")
}

[1] F. Rossi, P. Van Beek, and T. Walsh, Handbook of constraint programming. Elsevier, 2006.

Modules

branchers

Provides several implementations of [Brancher]s.

tie_breaking

Contains structures for tie-breaking.

value_selection

Provides the ValueSelector trait which is required for value selectors to implement; the main method in this trait relies on ValueSelector::select_value.

variable_selection

Provides the VariableSelector trait which is required for variable selectors to implement; the main method in this trait relies on VariableSelector::select_variable.

Structs

SelectionContext

The context provided to the [Brancher], it allows the retrieval of domain values of variables and access to methods from a Random generator.

Enums

BrancherEvent

The events which can occur for a Brancher. Used for returning which events are relevant in Brancher::subscribe_to_events, [VariableSelector::subscribe_to_events], and [ValueSelector::subscribe_to_events].

Traits

Brancher

A trait for definining a branching strategy (oftentimes utilising a [VariableSelector] and a [ValueSelector]).