Skip to content

Commit

Permalink
no deactivation for functional constraints
Browse files Browse the repository at this point in the history
  • Loading branch information
@AllenZzw
AllenZzw committed Oct 7, 2024
1 parent 615895b commit 05595fe
Show file tree
Hide file tree
Showing 15 changed files with 123 additions and 96 deletions.
6 changes: 4 additions & 2 deletions crates/huub/src/model.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ pub struct Model {
pub(crate) cnf: Cnf,
branchings: Vec<Branching>,
constraints: Vec<Constraint>,
functional: Vec<bool>,
int_vars: Vec<IntVarDef>,
prop_queue: VecDeque<usize>,
enqueued: Vec<bool>,
Expand Down Expand Up @@ -140,8 +141,8 @@ impl Model {
}

// Create constraint data structures within the solver
for c in self.constraints.iter() {
c.to_solver(&mut slv, &mut map)?;
for (i, c) in self.constraints.iter().enumerate() {
c.to_solver(&mut slv, &mut map, self.functional[i])?;
}
// Add branching data structures to the solver
for b in self.branchings.iter() {
Expand All @@ -163,6 +164,7 @@ impl AddAssign<Constraint> for Model {
fn add_assign(&mut self, rhs: Constraint) {
self.constraints.push(rhs);
self.enqueued.push(false);
self.functional.push(false);
self.enqueue(self.constraints.len() - 1);
self.subscribe(self.constraints.len() - 1);
}
Expand Down
77 changes: 39 additions & 38 deletions crates/huub/src/model/constraint.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,7 @@ impl Constraint {
&self,
slv: &mut Solver<Sat>,
map: &mut VariableMap,
functional: bool,
) -> Result<(), ReformulationError>
where
Sol: PropagatorAccess + SatValuation,
Expand All @@ -69,7 +70,7 @@ impl Constraint {
match self {
Constraint::AllDifferentInt(v) => {
let vars: Vec<_> = v.iter().map(|v| v.to_arg(slv, map)).collect();
slv.add_propagator(AllDifferentIntValue::prepare(vars))?;
slv.add_propagator(AllDifferentIntValue::prepare(vars), functional)?;
Ok(())
}
Constraint::ArrayIntElement(arr, idx, y) => {
Expand Down Expand Up @@ -101,21 +102,21 @@ impl Constraint {
Constraint::ArrayIntMinimum(vars, y) => {
let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect();
let y = y.to_arg(slv, map);
slv.add_propagator(ArrayIntMinimumBounds::prepare(vars, y))?;
slv.add_propagator(ArrayIntMinimumBounds::prepare(vars, y), functional)?;
Ok(())
}
Constraint::ArrayIntMaximum(vars, y) => {
let vars: Vec<_> = vars.iter().map(|v| -v.to_arg(slv, map)).collect();
let y = -y.to_arg(slv, map);
slv.add_propagator(ArrayIntMinimumBounds::prepare(vars, y))?;
slv.add_propagator(ArrayIntMinimumBounds::prepare(vars, y), functional)?;
Ok(())
}
Constraint::ArrayVarIntElement(vars, idx, y) => {
let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect();
let y = y.to_arg(slv, map);
let idx = idx.to_arg(slv, map);
// tranform 1-based index into 0-based index array
slv.add_propagator(ArrayVarIntElementBounds::prepare(vars, y, idx + (-1)))?;
slv.add_propagator(ArrayVarIntElementBounds::prepare(vars, y, idx + (-1)), functional)?;
Ok(())
}
Constraint::ArrayVarBoolElement(vars, idx, y) => {
Expand Down Expand Up @@ -165,7 +166,7 @@ impl Constraint {
slv.add_propagator(DisjunctiveStrictEdgeFinding::prepare(
vars.clone(),
durs.clone(),
))?;
), functional)?;

// Add symmetric propagator for upper bound propagation
let horizon = vars
Expand All @@ -181,52 +182,52 @@ impl Constraint {
slv.add_propagator(DisjunctiveStrictEdgeFinding::prepare(
symmetric_vars,
durs.clone(),
))?;
), functional)?;
Ok(())
}
Constraint::IntAbs(origin, abs) => {
let origin = origin.to_arg(slv, map);
let abs = abs.to_arg(slv, map);
slv.add_propagator(IntAbsBounds::prepare(origin, abs))?;
slv.add_propagator(IntAbsBounds::prepare(origin, abs), functional)?;
Ok(())
}
Constraint::IntDiv(numerator, denominator, result) => {
let numerator = numerator.to_arg(slv, map);
let denominator = denominator.to_arg(slv, map);
let result = result.to_arg(slv, map);
slv.add_propagator(IntDivBounds::prepare(numerator, denominator, result))?;
slv.add_propagator(IntDivBounds::prepare(numerator, denominator, result), functional)?;
Ok(())
}
Constraint::IntLinEq(vars, c) => {
let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect();
// coeffs * vars <= c
slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c))?;
slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c), functional)?;
// coeffs * vars >= c <=> -coeffs * vars <= -c
slv.add_propagator(IntLinearLessEqBounds::prepare(
vars.into_iter().map(|v| -v),
-c,
))?;
), functional)?;
Ok(())
}
Constraint::IntLinEqImp(vars, c, r) => {
let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect();
let r = r.to_arg(slv, map, None)?;
match r.0 {
BoolViewInner::Const(true) => {
slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c))?;
slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c), functional)?;
slv.add_propagator(IntLinearLessEqBounds::prepare(
vars.into_iter().map(|v| -v),
-c,
))?;
), functional)?;
}
BoolViewInner::Const(false) => {}
BoolViewInner::Lit(r) => {
slv.add_propagator(IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r))?;
slv.add_propagator(IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r), functional)?;
slv.add_propagator(IntLinearLessEqImpBounds::prepare(
vars.into_iter().map(|v| -v),
-c,
r,
))?;
), functional)?;
}
}
Ok(())
Expand All @@ -236,42 +237,42 @@ impl Constraint {
let r = r.to_arg(slv, map, None)?;
match r.0 {
BoolViewInner::Const(true) => {
slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c))?;
slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c), functional)?;
slv.add_propagator(IntLinearLessEqBounds::prepare(
vars.into_iter().map(|v| -v),
-c,
))?;
), functional)?;
}
BoolViewInner::Const(false) => {
slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c))?;
slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c), functional)?;
}
BoolViewInner::Lit(r) => {
slv.add_propagator(IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r))?;
slv.add_propagator(IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r), functional)?;
slv.add_propagator(IntLinearLessEqImpBounds::prepare(
vars.iter().map(|v| -(*v)),
-c,
r,
))?;
slv.add_propagator(IntLinearNotEqImpValue::prepare(vars, *c, !r))?;
), functional)?;
slv.add_propagator(IntLinearNotEqImpValue::prepare(vars, *c, !r), functional)?;
}
}
Ok(())
}
Constraint::IntLinLessEq(vars, c) => {
let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect();
slv.add_propagator(IntLinearLessEqBounds::prepare(vars, *c))?;
slv.add_propagator(IntLinearLessEqBounds::prepare(vars, *c), functional)?;
Ok(())
}
Constraint::IntLinLessEqImp(vars, c, r) => {
let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect();
let r = r.to_arg(slv, map, None)?;
match r.0 {
BoolViewInner::Const(true) => {
slv.add_propagator(IntLinearLessEqBounds::prepare(vars, *c))?;
slv.add_propagator(IntLinearLessEqBounds::prepare(vars, *c), functional)?;
}
BoolViewInner::Const(false) => {}
BoolViewInner::Lit(r) => {
slv.add_propagator(IntLinearLessEqImpBounds::prepare(vars, *c, r))?;
slv.add_propagator(IntLinearLessEqImpBounds::prepare(vars, *c, r), functional)?;
}
}
Ok(())
Expand All @@ -281,40 +282,40 @@ impl Constraint {
let r = r.to_arg(slv, map, None)?;
match r.0 {
BoolViewInner::Const(true) => {
slv.add_propagator(IntLinearLessEqBounds::prepare(vars, *c))?;
slv.add_propagator(IntLinearLessEqBounds::prepare(vars, *c), functional)?;
}
BoolViewInner::Const(false) => {
slv.add_propagator(IntLinearLessEqBounds::prepare(
vars.into_iter().map(|v| -v),
-(c + 1),
))?;
), functional)?;
}
BoolViewInner::Lit(r) => {
slv.add_propagator(IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r))?;
slv.add_propagator(IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r), functional)?;
slv.add_propagator(IntLinearLessEqImpBounds::prepare(
vars.into_iter().map(|v| -v),
-(c + 1),
!r,
))?;
), functional)?;
}
}
Ok(())
}
Constraint::IntLinNotEq(vars, c) => {
let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect();
slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c))?;
slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c), functional)?;
Ok(())
}
Constraint::IntLinNotEqImp(vars, c, r) => {
let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect();
let r = r.to_arg(slv, map, None)?;
match r.0 {
BoolViewInner::Const(true) => {
slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c))?;
slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c), functional)?;
}
BoolViewInner::Const(false) => {}
BoolViewInner::Lit(r) => {
slv.add_propagator(IntLinearNotEqImpValue::prepare(vars, *c, r))?;
slv.add_propagator(IntLinearNotEqImpValue::prepare(vars, *c, r), functional)?;
}
}
Ok(())
Expand All @@ -324,27 +325,27 @@ impl Constraint {
let r = r.to_arg(slv, map, None)?;
match r.0 {
BoolViewInner::Const(true) => {
slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c))?;
slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c), functional)?;
}
BoolViewInner::Const(false) => {
slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c))?;
slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c), functional)?;
slv.add_propagator(IntLinearLessEqBounds::prepare(
vars.into_iter().map(|v| -v),
-c,
))?;
), functional)?;
}
BoolViewInner::Lit(r) => {
slv.add_propagator(IntLinearNotEqImpValue::prepare(vars.clone(), *c, r))?;
slv.add_propagator(IntLinearNotEqImpValue::prepare(vars.clone(), *c, r), functional)?;
slv.add_propagator(IntLinearLessEqImpBounds::prepare(
vars.clone(),
*c,
!r,
))?;
), functional)?;
slv.add_propagator(IntLinearLessEqImpBounds::prepare(
vars.iter().map(|v| -(*v)),
-c,
!r,
))?;
), functional)?;
}
}
Ok(())
Expand All @@ -353,14 +354,14 @@ impl Constraint {
let base = base.to_arg(slv, map);
let exponent = exponent.to_arg(slv, map);
let result = res.to_arg(slv, map);
slv.add_propagator(IntPowBounds::prepare(base, exponent, result))?;
slv.add_propagator(IntPowBounds::prepare(base, exponent, result), functional)?;
Ok(())
}
Constraint::IntTimes(x, y, z) => {
let x = x.to_arg(slv, map);
let y = y.to_arg(slv, map);
let z = z.to_arg(slv, map);
slv.add_propagator(IntTimesBounds::prepare(x, y, z))?;
slv.add_propagator(IntTimesBounds::prepare(x, y, z), functional)?;
Ok(())
}
Constraint::PropLogic(exp) => exp.constrain(slv, map),
Expand Down
3 changes: 3 additions & 0 deletions crates/huub/src/model/flatzinc.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1028,6 +1028,9 @@ where
}
_ => return Err(FlatZincError::UnknownConstraint(c.id.to_string())),
}

let n = self.prb.functional.len() - 1;
self.prb.functional[n] = c.defines.is_some();
}

Ok(())
Expand Down
10 changes: 5 additions & 5 deletions crates/huub/src/propagator/all_different_int.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,7 @@ mod tests {
EncodingType::Eager,
);

slv.add_propagator(AllDifferentIntValue::prepare(vec![a, b, c]))
slv.add_propagator(AllDifferentIntValue::prepare(vec![a, b, c]), false)
.unwrap();
slv.assert_all_solutions(&[a, b, c], |sol| sol.iter().all_unique());
}
Expand Down Expand Up @@ -145,7 +145,7 @@ mod tests {
EncodingType::Eager,
);

slv.add_propagator(AllDifferentIntValue::prepare(vec![a, b, c]))
slv.add_propagator(AllDifferentIntValue::prepare(vec![a, b, c]), false)
.unwrap();
slv.assert_unsatisfiable();
}
Expand All @@ -169,14 +169,14 @@ mod tests {
));
}
}
slv.add_propagator(AllDifferentIntValue::prepare(vars.clone()))
slv.add_propagator(AllDifferentIntValue::prepare(vars.clone()), false)
.unwrap();
all_vars.push(vars);
});
// add all different propagator for each column
for i in 0..9 {
let col_vars: Vec<IntView> = (0..9).map(|j| all_vars[j][i]).collect();
slv.add_propagator(AllDifferentIntValue::prepare(col_vars))
slv.add_propagator(AllDifferentIntValue::prepare(col_vars), false)
.unwrap();
}
// add all different propagator for each 3 by 3 grid
Expand All @@ -188,7 +188,7 @@ mod tests {
block_vars.push(all_vars[3 * i + x][3 * j + y]);
}
}
slv.add_propagator(AllDifferentIntValue::prepare(block_vars))
slv.add_propagator(AllDifferentIntValue::prepare(block_vars), false)
.unwrap();
}
}
Expand Down
4 changes: 2 additions & 2 deletions crates/huub/src/propagator/array_var_int_element.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -284,7 +284,7 @@ mod tests {
EncodingType::Lazy,
);

slv.add_propagator(ArrayVarIntElementBounds::prepare(vec![a, b, c], y, index))
slv.add_propagator(ArrayVarIntElementBounds::prepare(vec![a, b, c], y, index), false)
.unwrap();
slv.expect_solutions(
&[index, y, a, b, c],
Expand Down Expand Up @@ -351,7 +351,7 @@ mod tests {
EncodingType::Lazy,
);

slv.add_propagator(ArrayVarIntElementBounds::prepare(vec![a, b], y, index))
slv.add_propagator(ArrayVarIntElementBounds::prepare(vec![a, b], y, index), false)
.unwrap();
slv.expect_solutions(
&[index, y, a, b],
Expand Down
25 changes: 14 additions & 11 deletions crates/huub/src/propagator/disjunctive_strict.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -602,18 +602,21 @@ mod tests {
EncodingType::Lazy,
);
let durations = vec![2, 3, 1];
slv.add_propagator(DisjunctiveStrictEdgeFinding::prepare(
[a, b, c],
durations.clone(),
))
slv.add_propagator(
DisjunctiveStrictEdgeFinding::prepare([a, b, c], durations.clone()),
false,
)
.unwrap();
slv.add_propagator(DisjunctiveStrictEdgeFinding::prepare(
[a, b, c]
.iter()
.zip(durations.iter())
.map(|(v, d)| -*v + (7 - d)),
durations.clone(),
))
slv.add_propagator(
DisjunctiveStrictEdgeFinding::prepare(
[a, b, c]
.iter()
.zip(durations.iter())
.map(|(v, d)| -*v + (7 - d)),
durations.clone(),
),
false,
)
.unwrap();

slv.expect_solutions(
Expand Down
Loading

0 comments on commit 05595fe

Please sign in to comment.