From 86cca97c1e6918d07587c185175720ed267374bc Mon Sep 17 00:00:00 2001 From: Guillaume Pinot Date: Wed, 8 Sep 2021 16:59:20 +0200 Subject: [PATCH] Builder first iteration: bool constraints --- examples/simple_sat_program.rs | 43 +++----- src/builder.rs | 173 +++++++++++++++++++++++++++++++++ src/lib.rs | 1 + tests/bool_cst.rs | 94 ++++++++++++++++++ 4 files changed, 279 insertions(+), 32 deletions(-) create mode 100644 src/builder.rs create mode 100644 tests/bool_cst.rs diff --git a/examples/simple_sat_program.rs b/examples/simple_sat_program.rs index 5c74c62..2872c54 100644 --- a/examples/simple_sat_program.rs +++ b/examples/simple_sat_program.rs @@ -1,40 +1,19 @@ -use cp_sat::proto::{ - constraint_proto::Constraint, AllDifferentConstraintProto, ConstraintProto, CpModelProto, - IntegerVariableProto, -}; - fn main() { - let model = CpModelProto { - variables: vec![ - IntegerVariableProto { - name: "x".into(), - domain: vec![0, 2], - }, - IntegerVariableProto { - name: "y".into(), - domain: vec![0, 2], - }, - IntegerVariableProto { - name: "z".into(), - domain: vec![0, 2], - }, - ], - constraints: vec![ConstraintProto { - constraint: Some(Constraint::AllDiff(AllDifferentConstraintProto { - vars: vec![0, 1, 2], - })), - ..Default::default() - }], - ..Default::default() - }; + let mut model = cp_sat::builder::CpModelBuilder::default(); + let x = model.new_int_var_with_name([(0, 2)], "x"); + let y = model.new_int_var_with_name([(0, 2)], "y"); + let z = model.new_int_var_with_name([(0, 2)], "z"); + model.add_all_different([x, y, z]); println!("{:#?}", model); - - println!("model stats: {}", cp_sat::cp_model_stats(&model)); - - let response = cp_sat::solve(&model); + println!("model stats: {}", model.stats()); + let response = model.solve(); println!("{:#?}", response); println!( "response stats: {}", cp_sat::cp_solver_response_stats(&response, false) ); + assert_eq!(response.status(), cp_sat::proto::CpSolverStatus::Optimal); + assert!(x.solution_value(&response) != y.solution_value(&response)); + assert!(x.solution_value(&response) != z.solution_value(&response)); + assert!(y.solution_value(&response) != z.solution_value(&response)); } diff --git a/src/builder.rs b/src/builder.rs new file mode 100644 index 0000000..773a4e1 --- /dev/null +++ b/src/builder.rs @@ -0,0 +1,173 @@ +use crate::proto; + +#[derive(Default, Debug)] +pub struct CpModelBuilder { + proto: proto::CpModelProto, +} + +impl CpModelBuilder { + pub fn proto(&self) -> &proto::CpModelProto { + &self.proto + } + pub fn new_bool_var(&mut self) -> BoolVar { + self.new_bool_var_with_name("") + } + pub fn new_bool_var_with_name(&mut self, name: impl Into) -> BoolVar { + let index = self.proto.variables.len() as i32; + self.proto.variables.push(proto::IntegerVariableProto { + name: name.into(), + domain: vec![0, 1], + }); + BoolVar(index) + } + pub fn new_int_var(&mut self, domain: impl IntoIterator) -> IntVar { + self.new_int_var_with_name(domain, "") + } + pub fn new_int_var_with_name( + &mut self, + domain: impl IntoIterator, + name: impl Into, + ) -> IntVar { + let index = self.proto.variables.len() as i32; + self.proto.variables.push(proto::IntegerVariableProto { + name: name.into(), + domain: domain.into_iter().flat_map(|(b, e)| [b, e]).collect(), + }); + IntVar(index) + } + pub fn var_name(&self, var: impl Into) -> &str { + &self.proto.variables[var.into().0 as usize].name + } + pub fn set_var_name(&mut self, var: impl Into, name: &str) { + self.proto.variables[var.into().0 as usize].name = name.into(); + } + + pub fn add_or(&mut self, vars: impl IntoIterator) -> Constraint { + let index = self.proto.constraints.len(); + self.proto.constraints.push(proto::ConstraintProto { + constraint: Some(proto::constraint_proto::Constraint::BoolOr( + proto::BoolArgumentProto { + literals: vars.into_iter().map(|v| v.0).collect(), + }, + )), + ..Default::default() + }); + Constraint(index) + } + pub fn add_and(&mut self, vars: impl IntoIterator) -> Constraint { + let index = self.proto.constraints.len(); + self.proto.constraints.push(proto::ConstraintProto { + constraint: Some(proto::constraint_proto::Constraint::BoolAnd( + proto::BoolArgumentProto { + literals: vars.into_iter().map(|v| v.0).collect(), + }, + )), + ..Default::default() + }); + Constraint(index) + } + pub fn add_at_most_one(&mut self, vars: impl IntoIterator) -> Constraint { + let index = self.proto.constraints.len(); + self.proto.constraints.push(proto::ConstraintProto { + constraint: Some(proto::constraint_proto::Constraint::AtMostOne( + proto::BoolArgumentProto { + literals: vars.into_iter().map(|v| v.0).collect(), + }, + )), + ..Default::default() + }); + Constraint(index) + } + pub fn add_exactly_one(&mut self, vars: impl IntoIterator) -> Constraint { + let index = self.proto.constraints.len(); + self.proto.constraints.push(proto::ConstraintProto { + constraint: Some(proto::constraint_proto::Constraint::ExactlyOne( + proto::BoolArgumentProto { + literals: vars.into_iter().map(|v| v.0).collect(), + }, + )), + ..Default::default() + }); + Constraint(index) + } + pub fn add_xor(&mut self, vars: impl IntoIterator) -> Constraint { + let index = self.proto.constraints.len(); + self.proto.constraints.push(proto::ConstraintProto { + constraint: Some(proto::constraint_proto::Constraint::BoolXor( + proto::BoolArgumentProto { + literals: vars.into_iter().map(|v| v.0).collect(), + }, + )), + ..Default::default() + }); + Constraint(index) + } + pub fn add_all_different(&mut self, vars: impl IntoIterator) -> Constraint { + let index = self.proto.constraints.len(); + self.proto.constraints.push(proto::ConstraintProto { + constraint: Some(proto::constraint_proto::Constraint::AllDiff( + proto::AllDifferentConstraintProto { + vars: vars.into_iter().map(|v| v.0).collect(), + }, + )), + ..Default::default() + }); + Constraint(index) + } + + pub fn stats(&self) -> String { + crate::cp_model_stats(self.proto()) + } + pub fn solve(&self) -> proto::CpSolverResponse { + crate::solve(self.proto()) + } +} + +#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct BoolVar(i32); +impl BoolVar { + pub fn solution_value(self, response: &proto::CpSolverResponse) -> bool { + if self.0 < 0 { + use std::ops::Not; + !self.not().solution_value(response) + } else { + response.solution[self.0 as usize] != 0 + } + } +} +impl std::ops::Not for BoolVar { + type Output = Self; + fn not(self) -> Self { + Self(-self.0 - 1) + } +} +impl std::fmt::Debug for BoolVar { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> Result<(), std::fmt::Error> { + if self.0 < 0 { + write!(f, "Not({:?})", !*self) + } else { + write!(f, "BoolVar({})", self.0) + } + } +} + +#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct IntVar(i32); +impl From for IntVar { + fn from(bool_var: BoolVar) -> IntVar { + IntVar(bool_var.0) + } +} +impl IntVar { + pub fn solution_value(self, response: &proto::CpSolverResponse) -> i64 { + if self.0 < 0 { + use std::ops::Not; + 1 - IntVar::from(BoolVar(self.0).not()).solution_value(response) + } else { + response.solution[self.0 as usize] + } + } +} + +#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct Constraint(usize); diff --git a/src/lib.rs b/src/lib.rs index 6d4e950..b5f8bf6 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -5,6 +5,7 @@ use std::ffi::CStr; pub mod proto { include!(concat!(env!("OUT_DIR"), "/operations_research.sat.rs")); } +pub mod builder; extern "C" { fn cp_sat_wrapper_solve( diff --git a/tests/bool_cst.rs b/tests/bool_cst.rs new file mode 100644 index 0000000..6d2ea47 --- /dev/null +++ b/tests/bool_cst.rs @@ -0,0 +1,94 @@ +use cp_sat::builder::CpModelBuilder; +use cp_sat::proto::CpSolverStatus; + +#[test] +fn or() { + let mut model = CpModelBuilder::default(); + let x = model.new_bool_var(); + let y = model.new_bool_var(); + model.add_or([x, y]); + let response = model.solve(); + assert_eq!(response.status(), CpSolverStatus::Optimal); + assert!(x.solution_value(&response) || y.solution_value(&response)); +} + +#[test] +fn and() { + let mut model = CpModelBuilder::default(); + let x = model.new_bool_var(); + let y = model.new_bool_var(); + model.add_and([x, y]); + let response = model.solve(); + assert_eq!(response.status(), CpSolverStatus::Optimal); + assert!(x.solution_value(&response)); + assert!(y.solution_value(&response)); +} + +#[test] +fn at_most_one() { + let mut model = CpModelBuilder::default(); + let vars: Vec<_> = (0..10).map(|_| model.new_bool_var()).collect(); + model.add_at_most_one(vars.iter().copied()); + let response = model.solve(); + assert_eq!(response.status(), CpSolverStatus::Optimal); + assert!( + vars.iter() + .map(|v| v.solution_value(&response) as u32) + .sum::() + <= 1 + ); +} + +#[test] +fn exactly_one() { + let mut model = CpModelBuilder::default(); + let vars: Vec<_> = (0..10).map(|_| model.new_bool_var()).collect(); + model.add_exactly_one(vars.iter().copied()); + let response = model.solve(); + assert_eq!(response.status(), CpSolverStatus::Optimal); + assert!( + vars.iter() + .map(|v| v.solution_value(&response) as u32) + .sum::() + == 1 + ); +} + +#[test] +fn xor() { + let mut model = CpModelBuilder::default(); + let vars: Vec<_> = (0..10).map(|_| model.new_bool_var()).collect(); + model.add_xor(vars.iter().copied()); + let response = model.solve(); + assert_eq!(response.status(), CpSolverStatus::Optimal); + assert!( + vars.iter() + .map(|v| v.solution_value(&response) as u32) + .sum::() + % 2 + == 1 + ); +} + +#[test] +fn not_infeasible() { + let mut model = CpModelBuilder::default(); + let x = model.new_bool_var(); + model.add_and([x, !x]); + let response = model.solve(); + assert_eq!(response.status(), CpSolverStatus::Infeasible); +} + +#[test] +fn not_feasible() { + let mut model = CpModelBuilder::default(); + let x = model.new_bool_var(); + let y = model.new_bool_var(); + model.add_and([x, !y]); + let response = model.solve(); + assert_eq!(response.status(), CpSolverStatus::Optimal); + assert!(x.solution_value(&response)); + assert!(!(!x).solution_value(&response)); + assert!(!y.solution_value(&response)); + assert!((!y).solution_value(&response)); +}