chore(cp): Simplify linear constraint interface by removing literals.

plaans · Sep 15, 2024 · 2390174 · 2390174
1 parent 799c3e7
commit 2390174
Show file tree

Hide file tree

Showing 8 changed files with 178 additions and 632 deletions.
diff --git a/examples/knapsack/main.rs b/examples/knapsack/main.rs
@@ -142,76 +142,6 @@ fn solve(pb: &Pb) -> Sol {
     }
 }
 
-/// Alternate solver where each value/weight is encoded as an optional variable.
-#[allow(unused)]
-fn solve_optional(pb: &Pb) -> Sol {
-    let mut model = Model::new();
-
-    let presence_vars: Vec<Lit> = pb
-        .items
-        .iter()
-        .map(|item| model.new_presence_variable(Lit::TRUE, &item.name).true_lit())
-        .collect();
-    let weight_vars: Vec<_> = presence_vars
-        .iter()
-        .copied()
-        .enumerate()
-        .map(|(i, prez)| {
-            model
-                .new_optional_ivar(
-                    pb.items[i].weight,
-                    pb.items[i].weight,
-                    prez,
-                    format!("{}_weight", pb.items[i].name),
-                )
-                .or_zero(prez)
-        })
-        .collect();
-    let value_vars: Vec<_> = presence_vars
-        .iter()
-        .copied()
-        .enumerate()
-        .map(|(i, prez)| {
-            model
-                .new_optional_ivar(
-                    pb.items[i].value,
-                    pb.items[i].value,
-                    prez,
-                    format!("{}_value", pb.items[i].name),
-                )
-                .or_zero(prez)
-        })
-        .collect();
-
-    let objective = model.new_ivar(0, 1000, "objective");
-
-    let total_weight = LinearSum::of(weight_vars);
-    let total_value = LinearSum::of(value_vars);
-
-    // model.enforce(total_weight.clone().geq(1));
-    model.enforce(total_weight.leq(pb.capacity), []);
-    model.enforce(total_value.clone().leq(objective), []);
-    model.enforce(total_value.geq(objective), []);
-
-    let mut solver = Solver::new(model);
-    if let Some(sol) = solver.maximize(objective).unwrap() {
-        let model = solver.model.clone().with_domains(sol.1.as_ref().clone());
-        model.print_state();
-        let items: Vec<Item> = presence_vars
-            .iter()
-            .zip(pb.items.iter())
-            .filter(|(&prez, _)| model.entails(prez))
-            .map(|(_, item)| item.clone())
-            .collect();
-        let solution = Sol { items };
-        assert_eq!(solution.value(), sol.0);
-        assert!(pb.is_valid(&solution));
-        solution
-    } else {
-        panic!("NO SOLUTION");
-    }
-}
-
 fn main() {
     let args: Vec<String> = env::args().collect();
     println!("{args:?}");
@@ -226,7 +156,7 @@ fn main() {
 
 #[cfg(test)]
 mod tests {
-    use crate::{solve, solve_optional, Pb};
+    use crate::{solve, Pb};
 
     static PROBLEMS: &[&str] = &[
         "cap 10 ; opt 6 ; a 1 1 ; b 5 6 ; c 3 6",
@@ -244,7 +174,6 @@ mod tests {
             println!("{pb}");
 
             assert!(pb.is_valid(&solve(&pb)));
-            assert!(pb.is_valid(&solve_optional(&pb)));
         }
     }
 }
diff --git a/examples/scheduling/src/problem.rs b/examples/scheduling/src/problem.rs
@@ -1,7 +1,7 @@
 use crate::search::{Model, Var};
 use aries::core::Lit;
 use aries::model::lang::expr::{alternative, eq, leq, or};
-use aries::model::lang::linear::{LinearSum, LinearTerm};
+use aries::model::lang::linear::LinearSum;
 use aries::model::lang::max::{EqMax, EqMin};
 use aries::model::lang::{IAtom, IVar};
 use itertools::Itertools;
@@ -358,7 +358,8 @@ pub(crate) fn encode(pb: &Problem, lower_bound: u32, upper_bound: u32) -> (Model
         // sum of the duration of all tasks executing on the machine
         let mut dur_sum = LinearSum::zero();
         for alt in &alts {
-            dur_sum += LinearTerm::constant_int(alt.duration, alt.presence)
+            let i_prez = IVar::new(alt.presence.variable());
+            dur_sum += i_prez * alt.duration;
         }
 
         m.enforce((dur_sum + start_first).leq(end_last), []);

diff --git a/solver/src/model/lang/int.rs b/solver/src/model/lang/int.rs
@@ -37,11 +37,6 @@ impl IVar {
     pub fn gt(self, i: IntCst) -> Lit {
         Lit::gt(self, i)
     }
-
-    /// Transforms the given integer variable into a LinearTerm that is zero if the given literal is false.
-    pub fn or_zero(self, lit: Lit) -> LinearTerm {
-        LinearTerm::int(1, self, lit)
-    }
 }
 
 impl From<IVar> for VarRef {
@@ -205,6 +200,6 @@ impl std::ops::Mul<IntCst> for IVar {
     type Output = LinearTerm;
 
     fn mul(self, rhs: IntCst) -> Self::Output {
-        LinearTerm::int(rhs, self, Lit::TRUE)
+        LinearTerm::int(rhs, self)
     }
 }