Builder first iteration: bool constraints
This commit is contained in:
committed by
Guillaume P
parent
adcc1d638b
commit
86cca97c1e
@@ -1,40 +1,19 @@
|
|||||||
use cp_sat::proto::{
|
|
||||||
constraint_proto::Constraint, AllDifferentConstraintProto, ConstraintProto, CpModelProto,
|
|
||||||
IntegerVariableProto,
|
|
||||||
};
|
|
||||||
|
|
||||||
fn main() {
|
fn main() {
|
||||||
let model = CpModelProto {
|
let mut model = cp_sat::builder::CpModelBuilder::default();
|
||||||
variables: vec![
|
let x = model.new_int_var_with_name([(0, 2)], "x");
|
||||||
IntegerVariableProto {
|
let y = model.new_int_var_with_name([(0, 2)], "y");
|
||||||
name: "x".into(),
|
let z = model.new_int_var_with_name([(0, 2)], "z");
|
||||||
domain: vec![0, 2],
|
model.add_all_different([x, y, z]);
|
||||||
},
|
|
||||||
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()
|
|
||||||
};
|
|
||||||
println!("{:#?}", model);
|
println!("{:#?}", model);
|
||||||
|
println!("model stats: {}", model.stats());
|
||||||
println!("model stats: {}", cp_sat::cp_model_stats(&model));
|
let response = model.solve();
|
||||||
|
|
||||||
let response = cp_sat::solve(&model);
|
|
||||||
println!("{:#?}", response);
|
println!("{:#?}", response);
|
||||||
println!(
|
println!(
|
||||||
"response stats: {}",
|
"response stats: {}",
|
||||||
cp_sat::cp_solver_response_stats(&response, false)
|
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));
|
||||||
}
|
}
|
||||||
|
|||||||
+173
@@ -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<String>) -> 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<Item = (i64, i64)>) -> IntVar {
|
||||||
|
self.new_int_var_with_name(domain, "")
|
||||||
|
}
|
||||||
|
pub fn new_int_var_with_name(
|
||||||
|
&mut self,
|
||||||
|
domain: impl IntoIterator<Item = (i64, i64)>,
|
||||||
|
name: impl Into<String>,
|
||||||
|
) -> 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<IntVar>) -> &str {
|
||||||
|
&self.proto.variables[var.into().0 as usize].name
|
||||||
|
}
|
||||||
|
pub fn set_var_name(&mut self, var: impl Into<IntVar>, name: &str) {
|
||||||
|
self.proto.variables[var.into().0 as usize].name = name.into();
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn add_or(&mut self, vars: impl IntoIterator<Item = BoolVar>) -> 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<Item = BoolVar>) -> 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<Item = BoolVar>) -> 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<Item = BoolVar>) -> 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<Item = BoolVar>) -> 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<Item = IntVar>) -> 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<BoolVar> 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);
|
||||||
@@ -5,6 +5,7 @@ use std::ffi::CStr;
|
|||||||
pub mod proto {
|
pub mod proto {
|
||||||
include!(concat!(env!("OUT_DIR"), "/operations_research.sat.rs"));
|
include!(concat!(env!("OUT_DIR"), "/operations_research.sat.rs"));
|
||||||
}
|
}
|
||||||
|
pub mod builder;
|
||||||
|
|
||||||
extern "C" {
|
extern "C" {
|
||||||
fn cp_sat_wrapper_solve(
|
fn cp_sat_wrapper_solve(
|
||||||
|
|||||||
@@ -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::<u32>()
|
||||||
|
<= 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::<u32>()
|
||||||
|
== 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::<u32>()
|
||||||
|
% 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));
|
||||||
|
}
|
||||||
Reference in New Issue
Block a user