diff --git a/crates/huub/src/solver/engine.rs b/crates/huub/src/solver/engine.rs index 3c45639e..21edbabc 100644 --- a/crates/huub/src/solver/engine.rs +++ b/crates/huub/src/solver/engine.rs @@ -56,7 +56,10 @@ impl IpasirPropagator for Engine { // Process Boolean assignment if persistent && self.state.decision_level() != 0 { // Note that the assignment might already be known and trailed, but not previously marked as persistent - self.persistent.push(lit) + self.persistent.push(lit); + if self.state.trail.is_backtracking() { + return; + } } if self.state.trail.assign_sat(lit).is_some() { return; diff --git a/crates/huub/src/solver/engine/trail.rs b/crates/huub/src/solver/engine/trail.rs index 02e9a563..879710ef 100644 --- a/crates/huub/src/solver/engine/trail.rs +++ b/crates/huub/src/solver/engine/trail.rs @@ -5,6 +5,7 @@ use std::{ use index_vec::IndexVec; use pindakaas::{Lit as RawLit, Var as RawVar}; +use tracing::{debug, trace}; use crate::{actions::trailing::TrailingActions, IntVal}; @@ -16,25 +17,30 @@ index_vec::define_index_type! { #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) struct Trail { trail: Vec, + pos: usize, prev_len: Vec, int_value: IndexVec, sat_value: HashMap, + sat_restore_value: HashMap, } impl Default for Trail { fn default() -> Self { Self { trail: Vec::new(), + pos: 0, prev_len: Vec::new(), int_value: IndexVec::new(), sat_value: HashMap::new(), + sat_restore_value: HashMap::new(), } } } impl Trail { fn push_trail(&mut self, event: TrailEvent) { + debug_assert_eq!(self.pos, self.trail.len()); match event { TrailEvent::SatAssignment(r) => { let r = i32::from(r); @@ -48,43 +54,120 @@ impl Trail { self.trail.push(i as u32) } } + self.pos = self.trail.len(); } - fn pop_trail(&mut self) -> Option { - if self.trail.is_empty() { + fn undo(&mut self) -> Option { + debug_assert!(self.pos <= self.trail.len()); + if self.pos == 0 { return None; } - let i = self.trail.pop().unwrap() as i32; - Some(if i.is_positive() { + // Find event before current position + let i = self.trail[self.pos - 1] as i32; + let event = if i.is_positive() { + self.pos -= 1; // SAFETY: This is safe because RawVar uses the same representation as i32 TrailEvent::SatAssignment(unsafe { transmute(i) }) } else { let i = -i as usize; - let high = self.trail.pop().unwrap() as u64; - let low = self.trail.pop().unwrap() as u64; + let high = self.trail[self.pos - 2] as u64; + let low = self.trail[self.pos - 3] as u64; + self.pos -= 3; TrailEvent::IntAssignment(i.into(), ((high << 32) | low) as i64) - }) + }; + + match event { + TrailEvent::SatAssignment(r) => { + let b = self.sat_value.remove(&r).unwrap(); + if RESTORE { + let x = self.sat_restore_value.insert(r, b); + debug_assert!(x.is_none()); + } + } + TrailEvent::IntAssignment(i, v) => { + if RESTORE { + self.trail.swap(self.pos, self.pos + 2); + } + self.int_value[i] = v; + } + } + Some(event) } - fn undo_event(&mut self, event: TrailEvent) { + + fn redo(&mut self) -> Option { + debug_assert!(self.pos <= self.trail.len()); + + if self.pos == self.trail.len() { + return None; + } + // Find event at current position + let i = self.trail[self.pos] as i32; + let event = if i.is_positive() { + self.pos += 1; + // SAFETY: This is safe because RawVar uses the same representation as i32 + TrailEvent::SatAssignment(unsafe { transmute(i) }) + } else { + let i = -i as usize; + let high = self.trail[self.pos + 1] as u64; + let low = self.trail[self.pos + 2] as u64; + self.pos += 3; + TrailEvent::IntAssignment(i.into(), ((high << 32) | low) as i64) + }; + match event { TrailEvent::SatAssignment(r) => { - let _ = self.sat_value.remove(&r); + let b = self.sat_restore_value.remove(&r).unwrap(); + let x = self.sat_value.insert(r, b); + debug_assert!(x.is_none()); } TrailEvent::IntAssignment(i, v) => { + self.trail.swap(self.pos - 1, self.pos - 3); self.int_value[i] = v; } } + Some(event) } pub(crate) fn undo_until_found_lit(&mut self, lit: RawLit) { let var = lit.var(); - while let Some(event) = self.pop_trail() { + if !self.sat_value.contains_key(&var) { + if !self.sat_restore_value.contains_key(&var) { + panic!("literal is not present in the trail") + } + debug!( + lit = i32::from(lit), + "literal is already unset, restoring to point of setting literal" + ); + while let Some(event) = self.redo() { + let found = matches!(event, TrailEvent::SatAssignment(r) if r == var); + if found { + trace!( + len = self.pos, + lit = i32::from(lit), + "reversed the trail to find literal" + ); + return; + } + } + unreachable!("literal not on trail") + } + while let Some(event) = self.undo::() { let found = matches!(event, TrailEvent::SatAssignment(r) if r == var); - self.undo_event(event); if found { + let e = self.redo(); + debug_assert_eq!(e, Some(TrailEvent::SatAssignment(var))); + trace!( + len = self.pos, + lit = i32::from(lit), + "reversed the trail to find literal" + ); return; } } - panic!("literal {:?} was never assigned", lit) + unreachable!("literal not on trail") + } + + pub(crate) fn is_backtracking(&self) -> bool { + self.pos != self.trail.len() } pub(crate) fn notify_new_decision_level(&mut self) { @@ -98,11 +181,18 @@ impl Trail { "backtracking to level {level} length {len}, but trail is already at length {}", self.trail.len() ); - while self.trail.len() > len { - let event = self.pop_trail().unwrap(); - self.undo_event(event); + if len <= self.pos { + while self.pos > len { + let _ = self.undo::(); + } + } else { + while self.pos < len { + let _ = self.redo(); + } } - debug_assert_eq!(self.trail.len(), len); + debug_assert_eq!(self.pos, len); + self.trail.truncate(len); + self.sat_restore_value.clear(); } pub(crate) fn decision_level(&self) -> usize { self.prev_len.len() @@ -158,38 +248,51 @@ mod tests { use pindakaas::solver::{cadical::Cadical, NextVarRange}; use crate::{ - solver::engine::trail::{Trail, TrailEvent, TrailedInt}, + solver::engine::trail::{Trail, TrailEvent}, IntVal, }; #[test] fn test_trail_event() { let mut slv = Cadical::default(); + let mut trail = Trail::default(); let lits = slv.next_var_range(10).unwrap(); - let int_events: [(u32, IntVal); 10] = [ - (0, 0), - (1, 1), - (2, -1), - (i32::MAX as u32, IntVal::MAX), - (9474, IntVal::MIN), - (6966, 4084), - (4099, -9967), - (1977, 9076), - (2729, -4312), - (941, 1718), - ]; + let int_events: Vec<_> = [ + 0, + 1, + -1, + IntVal::MAX, + IntVal::MIN, + 4084, + -9967, + 9076, + -4312, + 1718, + ] + .into_iter() + .map(|i| (trail.track_int(0), i)) + .collect(); - let mut trail = Trail::default(); for (l, (i, v)) in lits.clone().zip(int_events.iter()) { trail.push_trail(TrailEvent::SatAssignment(l)); - trail.push_trail(TrailEvent::IntAssignment(TrailedInt::from_raw(*i), *v)); + let _ = trail.assign_sat(if usize::from(*i) % 2 == 0 { + l.into() + } else { + !l + }); + trail.push_trail(TrailEvent::IntAssignment(*i, *v)); } for (l, (i, v)) in lits.rev().zip(int_events.iter().rev()) { - assert_eq!( - trail.pop_trail().unwrap(), - TrailEvent::IntAssignment(TrailedInt::from_raw(*i), *v) - ); - assert_eq!(trail.pop_trail().unwrap(), TrailEvent::SatAssignment(l)) + let e = trail.undo::().unwrap(); + assert_eq!(e, TrailEvent::IntAssignment(*i, *v)); + let r = trail.redo().unwrap(); + assert_eq!(r, e); + let _ = trail.undo::().unwrap(); + let e = trail.undo::().unwrap(); + assert_eq!(e, TrailEvent::SatAssignment(l)); + let r = trail.redo().unwrap(); + assert_eq!(r, e); + let _ = trail.undo::().unwrap(); } } }