huub 100.0.0

CP+SAT solver framework built to be reliable, performant, and extensible
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100

//! Model (and solver) construction from external formats.

#[cfg(feature = "flatzinc")]
pub mod flatzinc;

use pindakaas::solver::propagation::ExternalPropagation;

use crate::{
	IntVal,
	lower::LoweringMap,
	model::View,
	solver::{
		Solver,
		branchers::{
			BoolBrancher, DecisionSelection, DomainSelection, IntBrancher, WarmStartBrancher,
		},
	},
};

/// Reference to a decision in a [`Model`](crate::model::Model).
#[derive(Clone, Debug, Eq, Hash, PartialEq)]
#[non_exhaustive]
pub enum AnyView {
	/// Reference to a Boolean decision.
	Bool(View<bool>),
	/// Reference to an integer decision.
	Int(View<IntVal>),
}

/// Specification of a search strategy that can lowered into
/// [`Brancher`](crate::solver::branchers::Brancher) implementations added to a
/// [`Solver`] instance.
///
/// Note that a [`Branching`] might be ignored (or used as only a suggestion) in
/// [`Solver`] depending on the configuration.
#[derive(Clone, Debug, Eq, Hash, PartialEq)]
#[non_exhaustive]
pub enum Branching {
	/// Make a search decision by using the [`DecisionSelection`] to select a
	/// Boolean decision variable, and then set its value by using the
	/// [`DomainSelection`].
	Bool(Vec<View<bool>>, DecisionSelection, DomainSelection),
	/// Make a search decision by using the [`DecisionSelection`] to select a
	/// integer decision variable, and then limit the domain of the variable by
	/// using the [`DomainSelection`].
	Int(Vec<View<IntVal>>, DecisionSelection, DomainSelection),
	/// Search by sequentially applying the given branching strategies.
	Seq(Vec<Branching>),
	/// Search by enforcing the given Boolean expressions, but abandon the
	/// search when finding a conflict.
	WarmStart(Vec<View<bool>>),
}

/// Type of an optimization goal found during model or solver deserialization.
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
#[non_exhaustive]
pub enum Goal<V> {
	/// Search for a solution that minimizes the given objective.
	Minimize(V),
	/// Search for a solution that maximizes the given objective.
	Maximize(V),
}

impl From<View<IntVal>> for AnyView {
	fn from(value: View<IntVal>) -> Self {
		Self::Int(value)
	}
}

impl From<View<bool>> for AnyView {
	fn from(value: View<bool>) -> Self {
		Self::Bool(value)
	}
}

impl Branching {
	/// Add a [`Brancher`](crate::solver::branchers::Brancher) implementation to
	/// the solver that matches the branching strategy of the [`Branching`].
	pub fn to_solver<Sat: ExternalPropagation>(&self, slv: &mut Solver<Sat>, map: &LoweringMap) {
		match self {
			Branching::Bool(vars, var_sel, val_sel) => {
				let vars = vars.iter().map(|v| map.get(slv, *v)).collect();
				BoolBrancher::new_in(slv, vars, *var_sel, *val_sel);
			}
			Branching::Int(v, var_sel, val_sel) => {
				let vars: Vec<_> = v.iter().map(|v| map.get(slv, *v)).collect();
				IntBrancher::new_in(slv, vars, *var_sel, *val_sel);
			}
			Branching::Seq(branchings) => {
				for b in branchings {
					b.to_solver(slv, map);
				}
			}
			Branching::WarmStart(exprs) => {
				let decisions = exprs.iter().map(|v| map.get(slv, *v)).collect();
				WarmStartBrancher::new_in(slv, decisions);
			}
		}
	}
}