use crate::config::{Csp, OptimizationMode, PropagationStrategy, Pruning, SolveConfig, SolveStats};
use crate::constraint::VarId;
use crate::domain::{self, Domain};
use crate::solver::search::{self, SearchParams};
use crate::solver::{self, Solution, optimize};
impl<D: Domain> Csp<D> {
pub fn propagate(&mut self) -> Result<(), Unsatisfiable>
where
D::Value: PartialEq + 'static,
{
self.propagate_with(PropagationStrategy::Auto)
}
pub fn propagate_with(&mut self, strategy: PropagationStrategy) -> Result<(), Unsatisfiable>
where
D::Value: PartialEq + 'static,
{
match strategy {
PropagationStrategy::Auto => {
if self.adjacency.is_some() {
self.propagate_with(PropagationStrategy::Ac3)
} else {
self.propagate_with(PropagationStrategy::Sweep)
}
}
PropagationStrategy::Ac3 => {
let adjacency = self.adjacency.as_ref().ok_or(Unsatisfiable)?;
let mut worklist = solver::ac3::BitsetWorklist::new(self.constraints.len());
solver::ac3::ac3_full(
&mut self.variables,
&self.constraints,
adjacency,
&mut self.stats,
&mut worklist,
search::PERMANENT_DEPTH,
)
}
PropagationStrategy::Sweep => solver::monotonic::propagate_monotonic(
&mut self.variables,
&self.constraints,
&mut self.stats,
),
}
}
pub fn solve(&mut self, config: &SolveConfig) -> Vec<Solution<D>>
where
D::Value: PartialEq + 'static,
{
assert!(self.adjacency.is_some(), "call finalize() before solve()");
self.stats = SolveStats::default();
for v in &mut self.variables {
v.reset();
}
if config.pruning == Pruning::Ac3 {
let adjacency = self.adjacency.as_ref().unwrap();
let mut worklist = solver::ac3::BitsetWorklist::new(self.constraints.len());
let _ = solver::ac3::ac3_full(
&mut self.variables,
&self.constraints,
adjacency,
&mut self.stats,
&mut worklist,
search::PERMANENT_DEPTH,
);
}
let params = SearchParams {
pruning: config.pruning,
ordering: config.ordering,
max_solutions: config.max_solutions,
node_budget: config.node_budget,
cancel: config.cancel.clone(),
};
let adjacency = self.adjacency.as_ref().unwrap();
match config.optimization_mode {
OptimizationMode::Feasibility => search::feasibility_search(
&mut self.variables,
&self.constraints,
adjacency,
&mut self.constraint_weights,
&self.var_constraint_ids,
¶ms,
&mut self.stats,
None,
),
mode @ (OptimizationMode::MinimizeCost | OptimizationMode::MaximizeCost) => {
search::branch_and_bound(
&mut self.variables,
&self.constraints,
adjacency,
&mut self.constraint_weights,
&self.var_constraint_ids,
¶ms,
&mut self.stats,
mode == OptimizationMode::MaximizeCost,
&optimize::ZeroCost,
)
}
}
}
pub fn solve_with_given(
&mut self,
config: &SolveConfig,
given: &[(VarId, D::Value)],
) -> Vec<Solution<D>>
where
D::Value: PartialEq + 'static,
{
assert!(
self.adjacency.is_some(),
"call finalize() before solve_with_given()"
);
self.stats = SolveStats::default();
for v in &mut self.variables {
v.reset();
}
for (var, val) in given {
let _ = self.variables[*var as usize].domain.restrict_to(val);
}
{
let adjacency = self.adjacency.as_ref().unwrap();
for (var, val) in given {
for &neighbor in adjacency.neighbors_of_var(*var) {
let is_given = given.iter().any(|(gv, _)| *gv == neighbor);
if !is_given {
self.variables[neighbor as usize].domain.remove(val);
}
}
}
}
{
let adjacency = self.adjacency.as_ref().unwrap();
let mut worklist = solver::ac3::BitsetWorklist::new(self.constraints.len());
let _ = solver::ac3::ac3_full(
&mut self.variables,
&self.constraints,
adjacency,
&mut self.stats,
&mut worklist,
search::PERMANENT_DEPTH,
);
}
let params = SearchParams {
pruning: config.pruning,
ordering: config.ordering,
max_solutions: config.max_solutions,
node_budget: config.node_budget,
cancel: config.cancel.clone(),
};
let adjacency = self.adjacency.as_ref().unwrap();
search::feasibility_search(
&mut self.variables,
&self.constraints,
adjacency,
&mut self.constraint_weights,
&self.var_constraint_ids,
¶ms,
&mut self.stats,
Some(given),
)
}
pub fn solve_with_cost_eval(
&mut self,
config: &SolveConfig,
cost_eval: &dyn optimize::DomainCostEval<D>,
) -> Vec<Solution<D>>
where
D::Value: PartialEq + 'static,
{
assert!(
self.adjacency.is_some(),
"call finalize() before solve_with_cost_eval()"
);
self.stats = SolveStats::default();
for v in &mut self.variables {
v.reset();
}
let params = SearchParams {
pruning: config.pruning,
ordering: config.ordering,
max_solutions: config.max_solutions,
node_budget: config.node_budget,
cancel: config.cancel.clone(),
};
let adjacency = self.adjacency.as_ref().unwrap();
search::branch_and_bound(
&mut self.variables,
&self.constraints,
adjacency,
&mut self.constraint_weights,
&self.var_constraint_ids,
¶ms,
&mut self.stats,
config.optimization_mode == OptimizationMode::MaximizeCost,
cost_eval,
)
}
pub fn stats(&self) -> &SolveStats {
&self.stats
}
pub fn adjacency(&self) -> Option<&crate::adjacency::Adjacency> {
self.adjacency.as_ref()
}
}
impl<D: Domain> Default for Csp<D> {
fn default() -> Self {
Self::new()
}
}
impl<D: domain::CostDomain> Csp<D> {
pub fn solve_optimized(&mut self, config: &SolveConfig) -> Vec<Solution<D>>
where
D::Value: PartialEq + 'static,
{
self.solve_with_cost_eval(config, &optimize::CostDomainEval)
}
}
#[derive(Debug, Clone)]
pub struct Unsatisfiable;
impl std::fmt::Display for Unsatisfiable {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
write!(f, "CSP is unsatisfiable")
}
}
impl std::error::Error for Unsatisfiable {}