test(solver): Add solution witnesses to be able to detect invalid cla…

…uses.

examples/scheduling/src/main.rs

@@ -171,34 +171,50 @@ mod test {
     use crate::problem::ProblemKind;
     use crate::search::Var;
     use crate::{parser, problem};
+    use aries::core::state::witness;
     use aries::core::IntCst;
     use aries::model::lang::IVar;
     use aries::model::{Label, Model};
     use aries::solver::search::random::RandomChoice;
     use aries::solver::Solver;
 
-    fn random_solves<S: Label>(
-        model: &Model<S>,
-        objective: IVar,
-        num_solves: u32,
-        mut expected_result: Option<Option<IntCst>>,
-    ) {
+    /// Solve the problem multiple with different random variable ordering, ensuring that all results are as expected.
+    /// It also set up solution witness to check that no learned clause prune valid solutions.
+    fn random_solves<S: Label>(model: &Model<S>, objective: IVar, num_solves: u32, expected_result: Option<IntCst>) {
+        // when this object goes out of scope, any witness solution for the current thread will be removed
+        let _clean_up = witness::on_drop_witness_cleaner();
         for seed in 0..num_solves {
             let model = model.clone();
             let solver = &mut Solver::new(model);
             solver.set_brancher(RandomChoice::new(seed as u64));
-            let solution = solver.minimize(objective).unwrap().map(|(makespan, _)| makespan);
-            println!("SOL: {solution:?}");
-            if let Some(expected_sat) = expected_result {
-                assert_eq!(solution, expected_sat)
-            }
-            // ensure that the next run has the same output
-            expected_result = Some(solution);
-            solver.print_stats();
+            let result = if let Some((makespan, assignment)) = solver
+                .minimize_with(objective, |makespan, _| {
+                    if expected_result == Some(makespan) {
+                        // we have found the expected solution, remove the witness because the current solution
+                        // will be disallowed to force an improvement
+                        witness::remove_solution_witness()
+                    }
+                })
+                .unwrap()
+            {
+                println!("[{seed}] SOL: {makespan:?}");
+
+                if expected_result == Some(makespan) {
+                    // we have the expected solution, save it to be checked against
+                    // when this is set, solver for the current thread will check that any learned clause does not
+                    // forbid this solution
+                    witness::set_solution_witness(assignment.as_ref())
+                }
+
+                Some(makespan)
+            } else {
+                None
+            };
+            assert_eq!(expected_result, result);
         }
     }
 
-    fn test_grill(kind: ProblemKind, instance: &str, opt: u32, num_reps: u32) {
+    fn run_tests(kind: ProblemKind, instance: &str, opt: u32, num_reps: u32, use_constraints: bool) {
         let filecontent = std::fs::read_to_string(instance).expect("Cannot read file");
         let pb = match kind {
             ProblemKind::OpenShop => parser::openshop(&filecontent),
@@ -209,16 +225,65 @@ mod test {
 
         let lower_bound = pb.makespan_lower_bound() as u32;
 
-        // do not use advanced constraint in this first iteration of the tests
-        let (model, _encoding) = problem::encode(&pb, lower_bound, opt * 2, false);
+        // prodice a model for this problem
+        let (model, _encoding) = problem::encode(&pb, lower_bound, opt * 2, use_constraints);
         let makespan: IVar = IVar::new(model.shape.get_variable(&Var::Makespan).unwrap());
 
-        random_solves(&model, makespan, num_reps, Some(Some(opt as IntCst)))
+        // run several random solvers on the problem to assert the coherency of the results
+        random_solves(&model, makespan, num_reps, Some(opt as IntCst))
+    }
+
+    #[test]
+    fn test_ft06_basic() {
+        run_tests(ProblemKind::JobShop, "instances/jobshop/ft06.jsp", 55, 50, false);
+    }
+
+    #[test]
+    fn test_ft06_constraints() {
+        run_tests(ProblemKind::JobShop, "instances/jobshop/ft06.jsp", 55, 50, true);
+    }
+
+    #[test]
+    fn test_fjs_edata_mt06_basic() {
+        run_tests(
+            ProblemKind::FlexibleShop,
+            "instances/flexible/hu/edata/mt06.fjs",
+            55,
+            50,
+            false,
+        );
+    }
+
+    #[test]
+    fn test_fjs_edata_mt06_constraints() {
+        run_tests(
+            ProblemKind::FlexibleShop,
+            "instances/flexible/hu/edata/mt06.fjs",
+            55,
+            50,
+            true,
+        );
+    }
+
+    #[test]
+    fn test_fjs_rdata_mt06_basic() {
+        run_tests(
+            ProblemKind::FlexibleShop,
+            "instances/flexible/hu/rdata/mt06.fjs",
+            47,
+            10,
+            false,
+        );
     }
 
     #[test]
-    fn test_ft06() {
-        test_grill(ProblemKind::JobShop, "instances/jobshop/ft06.jsp", 55, 400);
-        // test_grill(ProblemKind::JobShop, "instances/jobshop/la01.jsp", 666, 2);
+    fn test_fjs_rdata_mt06_constraints() {
+        run_tests(
+            ProblemKind::FlexibleShop,
+            "instances/flexible/hu/rdata/mt06.fjs",
+            47,
+            10,
+            true,
+        );
     }
 }

solver/src/core/state/domains.rs

@@ -8,6 +8,9 @@ use crate::core::state::{Cause, DomainsSnapshot, Explainer, Explanation, Explana
 use crate::core::*;
 use std::fmt::{Debug, Formatter};
 
+#[cfg(debug_assertions)]
+pub mod witness;
+
 /// Structure that contains the domains of optional variable.
 ///
 /// Internally an optional variable is split between
@@ -510,9 +513,11 @@ impl Domains {
             // in the explanation, add a set of literal whose conjunction implies `l.lit`
             self.add_implying_literals_to_explanation(l, cause, &mut explanation, explainer);
         };
-
+        debug_assert!(!witness::pruned_by_clause(&clause), "Pre minimization: {clause:?}");
         // minimize the learned clause (removal of redundant literals)
         // let clause = self.minimize_clause(clause, explainer);
+        debug_assert!(!witness::pruned_by_clause(&clause), "Post minimization: {clause:?}");
+
         Conflict { clause, resolved }
     }
 

solver/src/core/state/domains/witness.rs

@@ -0,0 +1,46 @@
+use crate::core::state::Domains;
+use std::cell::RefCell;
+
+use crate::core::literals::Disjunction;
+
+thread_local! {
+    /// Represent a valid solution to the problem attempted on the current thread
+    static SOLUTION_WITNESS: RefCell<Option<Domains>> = const { RefCell::new(None) };
+}
+
+/// Records a solution witness for the current thread
+pub fn set_solution_witness(sol: &Domains) {
+    SOLUTION_WITNESS.with(|w| *w.borrow_mut() = Some(sol.clone()));
+}
+
+/// Remove the solution witness for the current thread
+pub fn remove_solution_witness() {
+    SOLUTION_WITNESS.with(|w| *w.borrow_mut() = None);
+}
+
+pub fn on_drop_witness_cleaner() -> WitnessCleaner {
+    WitnessCleaner
+}
+
+pub struct WitnessCleaner;
+impl Drop for WitnessCleaner {
+    fn drop(&mut self) {
+        remove_solution_witness()
+    }
+}
+
+/// Returns true if the witness solution was to be pruned by the clause
+pub fn pruned_by_clause(clause: &Disjunction) -> bool {
+    SOLUTION_WITNESS.with(|witness| {
+        if let Some(sol) = witness.borrow().as_ref() {
+            for l in clause {
+                if sol.entails(l) {
+                    return false;
+                }
+            }
+            true
+        } else {
+            false
+        }
+    })
+}