Change SolvingContext::set_bool to not trail literals early

Changes to the trail now all stem from the `Engine::notify_assignment`
method, called by the SAT oracle. The only exception is the
`Engine::propagate` method, which will call this method early in debug
mode to make literal assignments available when checking that all
literals in the reason are known `true`.

Cargo.toml

@@ -91,8 +91,6 @@ strip = "none"
 # The profile that 'cargo dist' will build with
 [profile.dist]
 inherits = "release"
-strip = "symbols"
-debug = false
 
 [profile.release]
 lto = "fat"

crates/fzn-huub/corpus/jobshop_la02.sol

@@ -1,2 +1,2 @@
 objective = 655;
-start = [0,20,394,481,572,0,25,94,135,155,0,72,166,229,315,156,260,336,460,510,25,52,107,242,348,193,287,433,483,510,138,336,464,505,589,72,135,259,414,557,52,385,460,510,600,66,138,156,236,585];
+start = [0,20,345,453,572,0,25,94,135,155,0,72,95,123,255,95,232,308,448,510,25,52,107,181,376,165,275,405,483,510,52,153,236,493,589,72,181,275,433,529,80,373,448,498,600,123,198,308,354,573];

crates/fzn-huub/corpus/jobshop_la03.sol

@@ -1,2 +1,2 @@
 objective = 597;
-start = [0,79,376,458,542,0,23,91,311,397,21,59,295,490,545,0,37,124,228,340,238,295,379,447,548,101,200,290,404,515,0,59,109,352,479,37,61,458,493,580,182,279,286,340,440,61,145,542,578,588];
+start = [0,79,376,458,542,0,23,91,311,397,21,59,295,490,545,0,37,124,228,340,238,295,379,447,548,101,200,290,404,515,0,59,109,352,440,37,61,458,493,580,182,279,286,340,506,61,145,542,578,588];

crates/fzn-huub/corpus/jobshop_la04.sol

@@ -1,2 +1,2 @@
 objective = 590;
-start = [0,304,398,490,581,0,19,30,452,486,19,33,113,213,398,135,230,339,346,445,33,107,124,324,418,30,115,186,296,392,230,304,434,490,581,78,185,262,384,482,54,115,124,200,254,0,96,126,185,346];
+start = [0,304,398,490,581,0,19,30,398,486,19,33,113,213,453,135,230,339,346,445,33,107,124,324,419,30,115,186,296,392,230,304,434,490,581,78,185,262,384,482,54,115,124,200,254,0,96,126,185,346];

crates/huub/src/actions/propagation.rs

@@ -8,12 +8,7 @@ use crate::{
 };
 
 pub(crate) trait PropagationActions: ExplanationActions + DecisionActions {
-	fn set_bool_val(
-		&mut self,
-		bv: BoolView,
-		val: bool,
-		reason: impl ReasonBuilder<Self>,
-	) -> Result<(), Conflict>;
+	fn set_bool(&mut self, bv: BoolView, reason: impl ReasonBuilder<Self>) -> Result<(), Conflict>;
 
 	fn set_int_lower_bound(
 		&mut self,

crates/huub/src/propagator/int_lin_le.rs

@@ -101,7 +101,7 @@ where
 		// propagate the reified variable if the sum of lower bounds is greater than the right-hand-side value
 		if let Some(r) = self.reification.get() {
 			if sum < 0 {
-				actions.set_bool_val(BoolView(BoolViewInner::Lit(*r)), false, |a: &mut P| {
+				actions.set_bool(BoolView(BoolViewInner::Lit(!r)), |a: &mut P| {
 					self.vars
 						.iter()
 						.map(|v| a.get_int_lower_bound_lit(*v))

crates/huub/src/propagator/int_lin_ne.rs

@@ -140,7 +140,7 @@ where
 			let val = self.violation - sum;
 			actions.set_int_not_eq(*v, val, self.reason(i))
 		} else if sum == self.violation {
-			actions.set_bool_val(r, false, self.reason(self.vars.len()))
+			actions.set_bool(!r, self.reason(self.vars.len()))
 		} else {
 			Ok(())
 		}

crates/huub/src/solver/engine.rs

@@ -233,13 +233,16 @@ impl IpasirPropagator for Engine {
 				.collect::<Vec<i32>>(),
 			"propagate"
 		);
-		for &lit in queue.iter() {
-			self.state.enqueue_propagators(lit, None);
-		}
 		// Debug helper to ensure that any reason is based on known true literals
 		#[cfg(debug_assertions)]
 		{
+			let mut prev = None;
 			for lit in queue.iter() {
+				// Notify of the assignment of the previous literal so it is available
+				// when checking the reason.
+				if let Some(prev) = prev {
+					self.notify_assignment(prev, false);
+				}
 				if let Some(reason) = self.state.reason_map.get(lit).cloned() {
 					let clause: Vec<_> = reason.to_clause(&mut self.propagators, &mut self.state);
 					for l in &clause {
@@ -256,6 +259,7 @@ impl IpasirPropagator for Engine {
 						);
 					}
 				}
+				prev = Some(*lit);
 			}
 		}
 		queue

crates/huub/src/solver/engine/solving_context.rs

@@ -41,6 +41,8 @@ enum ChangeType {
 }
 
 impl<'a> SolvingContext<'a> {
+	/// Create a new SolvingContext given the solver actions exposed by the SAT
+	/// oracle and the engine state.
 	pub(crate) fn new(slv: &'a mut dyn SolvingActions, state: &'a mut State) -> Self {
 		Self {
 			slv,
@@ -49,6 +51,8 @@ impl<'a> SolvingContext<'a> {
 		}
 	}
 
+	/// Run the propagators in the queue until a propagator detects a conflict,
+	/// returns literals to be propagated by the SAT oracle, or the queue is empty.
 	pub(crate) fn run_propagators(&mut self, propagators: &mut IndexVec<PropRef, BoxedPropagator>) {
 		while let Some(p) = self.state.propagator_queue.pop() {
 			debug_assert!(self.state.conflict.is_none());
@@ -75,21 +79,14 @@ impl<'a> SolvingContext<'a> {
 	}
 
 	#[inline]
+	/// Check whether a change is redundant, conflicting, or new with respect to
+	/// the bounds of an integer variable
 	fn check_change(&self, var: IntVarRef, change: &LitMeaning) -> ChangeType {
 		let (lb, ub) = self.state.int_vars[var].get_bounds(self);
 		match change {
 			LitMeaning::Eq(i) if lb == *i && ub == *i => ChangeType::Redundant,
 			LitMeaning::Eq(i) if *i < lb || *i > ub => ChangeType::Conflicting,
 			LitMeaning::NotEq(i) if *i < lb || *i > ub => ChangeType::Redundant,
-			LitMeaning::Eq(_) | LitMeaning::NotEq(_) => {
-				let lit = self.state.int_vars[var].get_bool_lit(change.clone());
-				let val = lit.and_then(|lit| self.get_bool_val(lit));
-				match val {
-					Some(true) => ChangeType::Redundant,
-					Some(false) => ChangeType::Conflicting,
-					None => ChangeType::New,
-				}
-			}
 			LitMeaning::GreaterEq(i) if *i <= lb => ChangeType::Redundant,
 			LitMeaning::GreaterEq(i) if *i > ub => ChangeType::Conflicting,
 			LitMeaning::Less(i) if *i > ub => ChangeType::Redundant,
@@ -99,6 +96,8 @@ impl<'a> SolvingContext<'a> {
 	}
 
 	#[inline]
+	/// Internal method used to propagate an integer variable given a literal
+	/// description to be enforced.
 	fn propagate_int(
 		&mut self,
 		iv: IntVarRef,
@@ -120,12 +119,14 @@ impl<'a> SolvingContext<'a> {
 			}
 			ChangeType::New => {
 				let bv = self.get_intref_lit(iv, lit_req.clone());
-				self.set_bool_val(bv, true, reason)
+				self.set_bool(bv, reason)
 			}
 		}
 	}
 
 	#[inline]
+	/// Internal method used to propagate a boolean variable used as a integer
+	/// given a literal description to be enforced.
 	fn propagate_bool_lin(
 		&mut self,
 		lit: RawLit,
@@ -134,10 +135,10 @@ impl<'a> SolvingContext<'a> {
 	) -> Result<(), Conflict> {
 		match lit_req {
 			LitMeaning::Eq(0) | LitMeaning::Less(1) | LitMeaning::NotEq(1) => {
-				self.set_bool_val(BoolView(BoolViewInner::Lit(lit)), false, reason)
+				self.set_bool(BoolView(BoolViewInner::Lit(!lit)), reason)
 			}
 			LitMeaning::Eq(1) | LitMeaning::GreaterEq(1) | LitMeaning::NotEq(0) => {
-				self.set_bool_val(BoolView(BoolViewInner::Lit(lit)), true, reason)
+				self.set_bool(BoolView(BoolViewInner::Lit(lit)), reason)
 			}
 			LitMeaning::Eq(_) => Err(Conflict::new(self, None, reason)),
 			LitMeaning::GreaterEq(i) if i > 1 => Err(Conflict::new(self, None, reason)),
@@ -206,38 +207,21 @@ impl InspectionActions for SolvingContext<'_> {
 }
 
 impl PropagationActions for SolvingContext<'_> {
-	fn set_bool_val(
-		&mut self,
-		bv: BoolView,
-		val: bool,
-		reason: impl ReasonBuilder<Self>,
-	) -> Result<(), Conflict> {
+	fn set_bool(&mut self, bv: BoolView, reason: impl ReasonBuilder<Self>) -> Result<(), Conflict> {
 		match bv.0 {
 			BoolViewInner::Lit(lit) => match self.state.trail.get_sat_value(lit) {
-				Some(b) if b == val => Ok(()),
-				Some(_) => Err(Conflict::new(
-					self,
-					Some(if val { lit } else { !lit }),
-					reason,
-				)),
+				Some(true) => Ok(()),
+				Some(false) => Err(Conflict::new(self, Some(lit), reason)),
 				None => {
-					let propagated_lit = if val { lit } else { !lit };
 					let reason = reason.build_reason(self);
-					trace!(lit = i32::from(propagated_lit), reason = ?reason, "propagate bool");
-					self.state.register_reason(propagated_lit, reason);
-					self.state.propagation_queue.push(propagated_lit);
-					let prev = self.state.trail.assign_lit(propagated_lit);
-					debug_assert!(prev.is_none());
+					trace!(lit = i32::from(lit), reason = ?reason, "propagate bool");
+					self.state.register_reason(lit, reason);
+					self.state.propagation_queue.push(lit);
 					Ok(())
 				}
 			},
-			BoolViewInner::Const(b) => {
-				if b != val {
-					Err(Conflict::new(self, None, reason))
-				} else {
-					Ok(())
-				}
-			}
+			BoolViewInner::Const(false) => Err(Conflict::new(self, None, reason)),
+			BoolViewInner::Const(true) => Ok(()),
 		}
 	}
 

crates/huub/src/solver/engine/trail.rs

@@ -153,29 +153,31 @@ impl Trail {
 	pub(crate) fn goto_assign_lit(&mut self, lit: RawLit) {
 		let var = lit.var();
 		if self.sat_store[Self::sat_index(var)].value.is_none() {
-			if self.sat_store[Self::sat_index(var)].restore.is_none() {
-				panic!("literal is not present in the trail")
-			}
 			while let Some(event) = self.redo() {
 				if matches!(event, TrailEvent::SatAssignment(r) if r == var) {
+					let e: Option<TrailEvent> = self.undo::<true>();
+					debug_assert_eq!(e, Some(TrailEvent::SatAssignment(var)));
 					trace!(
 						len = self.pos,
 						lit = i32::from(lit),
-						"redo to setting literal"
+						"redo to when literal was set"
 					);
 					return;
 				}
 			}
-			unreachable!("literal not on trail")
+			trace!(
+				len = self.pos,
+				lit = i32::from(lit),
+				"trail reset for unknown literal"
+			);
+			return;
 		}
 		while let Some(event) = self.undo::<true>() {
 			if matches!(event, TrailEvent::SatAssignment(r) if r == var) {
-				let e = self.redo();
-				debug_assert_eq!(e, Some(TrailEvent::SatAssignment(var)));
 				trace!(
 					len = self.pos,
 					lit = i32::from(lit),
-					"undo to setting literal"
+					"undo to when literal was set"
 				);
 				return;
 			}