diff options
Diffstat (limited to 'vendor/varisat/src/prop')
| -rw-r--r-- | vendor/varisat/src/prop/assignment.rs | 237 | ||||
| -rw-r--r-- | vendor/varisat/src/prop/binary.rs | 36 | ||||
| -rw-r--r-- | vendor/varisat/src/prop/graph.rs | 137 | ||||
| -rw-r--r-- | vendor/varisat/src/prop/long.rs | 164 | ||||
| -rw-r--r-- | vendor/varisat/src/prop/watch.rs | 135 |
5 files changed, 709 insertions, 0 deletions
diff --git a/vendor/varisat/src/prop/assignment.rs b/vendor/varisat/src/prop/assignment.rs new file mode 100644 index 000000000..a87f60485 --- /dev/null +++ b/vendor/varisat/src/prop/assignment.rs @@ -0,0 +1,237 @@ +//! Partial assignment and backtracking. +use partial_ref::{partial, PartialRef}; + +use varisat_formula::{lit::LitIdx, Lit, Var}; + +use crate::{ + context::{parts::*, Context}, + decision::make_available, +}; + +use super::Reason; + +/// Current partial assignment. +#[derive(Default)] +pub struct Assignment { + assignment: Vec<Option<bool>>, + last_value: Vec<bool>, +} + +/// This compares two `Option<bool>` values as bytes. Workaround for bad code generation. +pub fn fast_option_eq(a: Option<bool>, b: Option<bool>) -> bool { + unsafe { std::mem::transmute::<_, u8>(a) == std::mem::transmute::<_, u8>(b) } +} + +impl Assignment { + /// Update structures for a new variable count. + pub fn set_var_count(&mut self, count: usize) { + self.assignment.resize(count, None); + self.last_value.resize(count, false); + } + + /// Current partial assignment as slice. + pub fn assignment(&self) -> &[Option<bool>] { + &self.assignment + } + + /// Value assigned to a variable. + pub fn var_value(&self, var: Var) -> Option<bool> { + self.assignment[var.index()] + } + + /// Value last assigned to a variable. + /// + /// If the variable is currently assigned this returns the previously assigned value. If the + /// variable was never assigned this returns false. + pub fn last_var_value(&self, var: Var) -> bool { + self.last_value[var.index()] + } + + /// Value assigned to a literal. + pub fn lit_value(&self, lit: Lit) -> Option<bool> { + self.assignment[lit.index()].map(|b| b ^ lit.is_negative()) + } + + pub fn lit_is_true(&self, lit: Lit) -> bool { + fast_option_eq(self.assignment[lit.index()], Some(lit.is_positive())) + } + + pub fn lit_is_false(&self, lit: Lit) -> bool { + fast_option_eq(self.assignment[lit.index()], Some(lit.is_negative())) + } + + pub fn lit_is_unk(&self, lit: Lit) -> bool { + fast_option_eq(self.assignment[lit.index()], None) + } + + pub fn assign_lit(&mut self, lit: Lit) { + self.assignment[lit.index()] = lit.is_positive().into() + } + + pub fn unassign_var(&mut self, var: Var) { + self.assignment[var.index()] = None; + } + + /// Set the assigned/unassigned value of a variable. + pub fn set_var(&mut self, var: Var, assignment: Option<bool>) { + self.assignment[var.index()] = assignment; + } +} + +/// Decision and propagation history. +#[derive(Default)] +pub struct Trail { + /// Stack of all propagated and all enqueued assignments + trail: Vec<Lit>, + /// Next assignment in trail to propagate + queue_head_pos: usize, + /// Decision levels as trail indices. + decisions: Vec<LitIdx>, + /// Number of unit clauses removed from the trail. + units_removed: usize, +} + +impl Trail { + /// Return the next assigned literal to propagate. + pub fn queue_head(&self) -> Option<Lit> { + self.trail.get(self.queue_head_pos).cloned() + } + + /// Return the next assigned literal to propagate and remove it from the queue. + pub fn pop_queue(&mut self) -> Option<Lit> { + let head = self.queue_head(); + if head.is_some() { + self.queue_head_pos += 1; + } + head + } + + /// Re-enqueue all assigned literals. + pub fn reset_queue(&mut self) { + self.queue_head_pos = 0; + } + + /// Assigned literals in assignment order. + pub fn trail(&self) -> &[Lit] { + &self.trail + } + + /// Clear the trail. + /// + /// This simply removes all entries without performing any backtracking. Can only be called with + /// no active decisions. + pub fn clear(&mut self) { + assert!(self.decisions.is_empty()); + self.units_removed += self.trail.len(); + self.trail.clear(); + self.queue_head_pos = 0; + } + + /// Start a new decision level. + /// + /// Does not enqueue the decision itself. + pub fn new_decision_level(&mut self) { + self.decisions.push(self.trail.len() as LitIdx) + } + + /// Current decision level. + pub fn current_level(&self) -> usize { + self.decisions.len() + } + + /// The number of assignments at level 0. + pub fn top_level_assignment_count(&self) -> usize { + self.decisions + .get(0) + .map(|&len| len as usize) + .unwrap_or(self.trail.len()) + + self.units_removed + } + + /// Whether all assignments are processed. + pub fn fully_propagated(&self) -> bool { + self.queue_head_pos == self.trail.len() + } +} + +/// Enqueues the assignment of true to a literal. +/// +/// This updates the assignment and trail, but does not perform any propagation. The literal has to +/// be unassigned when calling this. +pub fn enqueue_assignment( + mut ctx: partial!(Context, mut AssignmentP, mut ImplGraphP, mut TrailP), + lit: Lit, + reason: Reason, +) { + let assignment = ctx.part_mut(AssignmentP); + debug_assert!(assignment.lit_value(lit) == None); + + assignment.assign_lit(lit); + + let (trail, mut ctx) = ctx.split_part_mut(TrailP); + + trail.trail.push(lit); + + let node = &mut ctx.part_mut(ImplGraphP).nodes[lit.index()]; + node.reason = reason; + node.level = trail.decisions.len() as LitIdx; + node.depth = trail.trail.len() as LitIdx; +} + +/// Undo all assignments in decision levels deeper than the given level. +pub fn backtrack( + mut ctx: partial!(Context, mut AssignmentP, mut TrailP, mut VsidsP), + level: usize, +) { + let (assignment, mut ctx) = ctx.split_part_mut(AssignmentP); + let (trail, mut ctx) = ctx.split_part_mut(TrailP); + + // level can actually be greater than the current level. This happens when restart is called + // after a conflict backtracked into the assumptions, but before any assumption was reenqueued. + // TODO should we update assumption_levels on backtracking instead of allowing this here? + if level >= trail.decisions.len() { + return; + } + + let new_trail_len = trail.decisions[level] as usize; + + trail.queue_head_pos = new_trail_len; + trail.decisions.truncate(level); + + let trail_end = &trail.trail[new_trail_len..]; + for &lit in trail_end { + make_available(ctx.borrow(), lit.var()); + let var_assignment = &mut assignment.assignment[lit.index()]; + assignment.last_value[lit.index()] = *var_assignment == Some(true); + *var_assignment = None; + } + trail.trail.truncate(new_trail_len); +} + +/// Undo all decisions and assumptions. +pub fn full_restart( + mut ctx: partial!( + Context, + mut AssignmentP, + mut AssumptionsP, + mut TrailP, + mut VsidsP, + ), +) { + ctx.part_mut(AssumptionsP).full_restart(); + backtrack(ctx.borrow(), 0); +} + +/// Undo all decisions. +pub fn restart( + mut ctx: partial!( + Context, + mut AssignmentP, + mut TrailP, + mut VsidsP, + AssumptionsP + ), +) { + let level = ctx.part(AssumptionsP).assumption_levels(); + backtrack(ctx.borrow(), level); +} diff --git a/vendor/varisat/src/prop/binary.rs b/vendor/varisat/src/prop/binary.rs new file mode 100644 index 000000000..d89347c8a --- /dev/null +++ b/vendor/varisat/src/prop/binary.rs @@ -0,0 +1,36 @@ +//! Propagation of binary clauses. +use partial_ref::{partial, PartialRef}; + +use varisat_formula::Lit; + +use crate::context::{parts::*, Context}; + +use super::{enqueue_assignment, Conflict, Reason}; + +/// Propagate all literals implied by the given literal via binary clauses. +/// +/// On conflict return the binary clause propgating the conflicting assignment. +pub fn propagate_binary( + mut ctx: partial!( + Context, + mut AssignmentP, + mut ImplGraphP, + mut TrailP, + BinaryClausesP, + ), + lit: Lit, +) -> Result<(), Conflict> { + let (binary_clauses, mut ctx) = ctx.split_part(BinaryClausesP); + + for &implied in binary_clauses.implied(lit) { + let assignment = ctx.part(AssignmentP); + + if assignment.lit_is_false(implied) { + return Err(Conflict::Binary([implied, !lit])); + } else if !assignment.lit_is_true(implied) { + enqueue_assignment(ctx.borrow(), implied, Reason::Binary([!lit])); + } + } + + Ok(()) +} diff --git a/vendor/varisat/src/prop/graph.rs b/vendor/varisat/src/prop/graph.rs new file mode 100644 index 000000000..3a0e3a42d --- /dev/null +++ b/vendor/varisat/src/prop/graph.rs @@ -0,0 +1,137 @@ +//! The implication graph. + +use partial_ref::{partial, PartialRef}; + +use varisat_formula::{lit::LitIdx, Lit, Var}; + +use crate::{ + clause::ClauseRef, + context::{parts::*, Context}, +}; + +/// Assignments that caused a propagation. +#[derive(Copy, Clone, Eq, PartialEq, Debug)] +pub enum Reason { + Unit, + Binary([Lit; 1]), + Long(ClauseRef), +} + +impl Reason { + /// The literals that caused the propagation. + pub fn lits<'out, 'a, 'b>(&'a self, ctx: &'b partial!('b Context, ClauseAllocP)) -> &'out [Lit] + where + 'a: 'out, + 'b: 'out, + { + match self { + Reason::Unit => &[], + Reason::Binary(lit) => lit, + // The propagated literal is always kept at position 0 + Reason::Long(cref) => &ctx.part(ClauseAllocP).clause(*cref).lits()[1..], + } + } + + /// True if a unit clause or assumption and not a propagation. + pub fn is_unit(&self) -> bool { + match self { + Reason::Unit => true, + _ => false, + } + } +} + +/// Propagation that resulted in a conflict. +#[derive(Copy, Clone, Eq, PartialEq, Debug)] +pub enum Conflict { + Binary([Lit; 2]), + Long(ClauseRef), +} + +impl Conflict { + /// The literals that caused the conflict. + pub fn lits<'out, 'a, 'b>(&'a self, ctx: &'b partial!('b Context, ClauseAllocP)) -> &'out [Lit] + where + 'a: 'out, + 'b: 'out, + { + match self { + Conflict::Binary(lits) => lits, + Conflict::Long(cref) => ctx.part(ClauseAllocP).clause(*cref).lits(), + } + } +} + +/// Node and incoming edges of the implication graph. +#[derive(Copy, Clone)] +pub struct ImplNode { + pub reason: Reason, + pub level: LitIdx, + /// Position in trail when assigned, `LitIdx::max_value()` is used as sentinel for removed + /// units. + pub depth: LitIdx, +} + +/// The implication graph. +/// +/// This is a DAG having all assigned variables as nodes. It has unit clauses, assumptions and +/// decisions as sources. For each propagated assignment it has incomming edges from the literals +/// whose assignment caused the propagation to happen. +#[derive(Default)] +pub struct ImplGraph { + /// Contains only valid data for indices of assigned variables. + pub nodes: Vec<ImplNode>, +} + +impl ImplGraph { + /// Update structures for a new variable count. + pub fn set_var_count(&mut self, count: usize) { + self.nodes.resize( + count, + ImplNode { + reason: Reason::Unit, + level: 0, + depth: 0, + }, + ); + } + + /// Get the reason for an assigned variable. + /// + /// Returns stale data if the variable isn't assigned. + pub fn reason(&self, var: Var) -> &Reason { + &self.nodes[var.index()].reason + } + + /// Get the decision level of an assigned variable. + /// + /// Returns stale data if the variable isn't assigned. + pub fn level(&self, var: Var) -> usize { + self.nodes[var.index()].level as usize + } + + /// Get the trail depth of an assigned variable. + /// + /// Returns stale data if the variable isn't assigned. + pub fn depth(&self, var: Var) -> usize { + self.nodes[var.index()].depth as usize + } + + /// Updates the reason for an assigned variable. + /// + /// Make sure the reason vars are in front of the assigned variable in the trail. + pub fn update_reason(&mut self, var: Var, reason: Reason) { + self.nodes[var.index()].reason = reason + } + + /// Updates the reason and depth of a unit clause removed from the trail. + pub fn update_removed_unit(&mut self, var: Var) { + let node = &mut self.nodes[var.index()]; + node.reason = Reason::Unit; + node.depth = LitIdx::max_value(); + } + + pub fn is_removed_unit(&self, var: Var) -> bool { + self.nodes[var.index()].depth == LitIdx::max_value() + } +} diff --git a/vendor/varisat/src/prop/long.rs b/vendor/varisat/src/prop/long.rs new file mode 100644 index 000000000..8fde47ec7 --- /dev/null +++ b/vendor/varisat/src/prop/long.rs @@ -0,0 +1,164 @@ +//! Propagation of long clauses. +use partial_ref::{partial, PartialRef}; + +use varisat_formula::Lit; + +use crate::context::{parts::*, Context}; + +use super::{assignment::fast_option_eq, enqueue_assignment, Conflict, Reason, Watch}; + +/// Propagate all literals implied by long clauses watched by the given literal. +/// +/// On conflict return the clause propgating the conflicting assignment. +/// +/// See [`prop::watch`](crate::prop::watch) for the invariants that this has to uphold. +pub fn propagate_long( + mut ctx: partial!( + Context, + mut AssignmentP, + mut ImplGraphP, + mut TrailP, + mut WatchlistsP, + mut ClauseAllocP, + ), + lit: Lit, +) -> Result<(), Conflict> { + // The code below is heavily optimized and replaces a much nicer but sadly slower version. + // Nevertheless it still performs full bound checks. Therefore this function is safe to call + // even when some other code violated invariants of for example the clause db. + unsafe { + let (watchlists, mut ctx) = ctx.split_part_mut(WatchlistsP); + let (alloc, mut ctx) = ctx.split_part_mut(ClauseAllocP); + + let watch_begin; + let watch_end; + { + let watch_list = &mut watchlists.watched_by_mut(lit); + watch_begin = watch_list.as_mut_ptr(); + watch_end = watch_begin.add(watch_list.len()); + } + let mut watch_ptr = watch_begin; + + let false_lit = !lit; + + let mut watch_write = watch_ptr; + + let assignment_limit = ctx.part(AssignmentP).assignment().len(); + let assignment_ptr = ctx.part(AssignmentP).assignment().as_ptr(); + + let is_true = |lit: Lit| { + assert!(lit.index() < assignment_limit); + fast_option_eq(*assignment_ptr.add(lit.index()), Some(lit.is_positive())) + }; + + let is_false = |lit: Lit| { + assert!(lit.index() < assignment_limit); + fast_option_eq(*assignment_ptr.add(lit.index()), Some(lit.is_negative())) + }; + + 'watchers: while watch_ptr != watch_end { + let watch = *watch_ptr; + watch_ptr = watch_ptr.add(1); + + // If the blocking literal (which is part of the watched clause) is already true, the + // watched clause is satisfied and we don't even have to look at it. + if is_true(watch.blocking) { + *watch_write = watch; + watch_write = watch_write.add(1); + continue; + } + + let cref = watch.cref; + + // Make sure we can access at least 3 lits + alloc.check_bounds(cref, 3); + + let clause_ptr = alloc.lits_ptr_mut_unchecked(cref); + let &mut header = alloc.header_unchecked_mut(cref); + + // First we ensure that the literal we're currently propagating is at index 1. This + // prepares the literal order for further propagations, as the propagating literal has + // to be at index 0. Doing this here also avoids a similar check later should the clause + // be satisfied by a non-watched literal, as we can just move it to index 1. + let mut first = *clause_ptr.add(0); + if first == false_lit { + let c1 = *clause_ptr.add(1); + first = c1; + *clause_ptr.add(0) = c1; + *clause_ptr.add(1) = false_lit; + } + + // We create a new watch with the other watched literal as blocking literal. This will + // either replace the currently processed watch or be added to another literals watch + // list. + let new_watch = Watch { + cref, + blocking: first, + }; + + // If the other watched literal (now the first) isn't the blocking literal, check + // whether that one is true. If so nothing else needs to be done. + if first != watch.blocking && is_true(first) { + *watch_write = new_watch; + watch_write = watch_write.add(1); + continue; + } + + // At this point we try to find a non-false unwatched literal to replace our current + // literal as the watched literal. + + let clause_len = header.len(); + let mut lit_ptr = clause_ptr.add(2); + let lit_end = clause_ptr.add(clause_len); + + // Make sure we can access all clause literals. + alloc.check_bounds(cref, clause_len); + + while lit_ptr != lit_end { + let rest_lit = *lit_ptr; + if !is_false(rest_lit) { + // We found a non-false literal and make it a watched literal by reordering the + // literals and adding the watch to the corresponding watchlist. + *clause_ptr.offset(1) = rest_lit; + *lit_ptr = false_lit; + + // We're currently using unsafe to modify the watchlist of lit, so make extra + // sure we're not aliasing. + assert_ne!(!rest_lit, lit); + watchlists.add_watch(!rest_lit, new_watch); + continue 'watchers; + } + lit_ptr = lit_ptr.add(1); + } + + // We didn't find a non-false unwatched literal, so either we're propagating or we have + // a conflict. + *watch_write = new_watch; + watch_write = watch_write.add(1); + + // If the other watched literal is false we have a conflict. + if is_false(first) { + // We move all unprocessed watches and resize the currentl watchlist. + while watch_ptr != watch_end { + *watch_write = *watch_ptr; + watch_write = watch_write.add(1); + watch_ptr = watch_ptr.add(1); + } + let out_size = ((watch_write as usize) - (watch_begin as usize)) + / std::mem::size_of::<Watch>(); + + watchlists.watched_by_mut(lit).truncate(out_size as usize); + + return Err(Conflict::Long(cref)); + } + + // Otherwise we enqueue a new propagation. + enqueue_assignment(ctx.borrow(), first, Reason::Long(cref)); + } + + let out_size = + ((watch_write as usize) - (watch_begin as usize)) / std::mem::size_of::<Watch>(); + watchlists.watched_by_mut(lit).truncate(out_size as usize); + } + Ok(()) +} diff --git a/vendor/varisat/src/prop/watch.rs b/vendor/varisat/src/prop/watch.rs new file mode 100644 index 000000000..095ac86a9 --- /dev/null +++ b/vendor/varisat/src/prop/watch.rs @@ -0,0 +1,135 @@ +//! Watchlists to detect clauses that became unit. +//! +//! Each (long) clause has always two watches pointing to it. The watches are kept in the watchlists +//! of two different literals of the clause. Whenever the watches are moved to different literals +//! the litereals of the clause are permuted so the watched literals are in position 0 and 1. +//! +//! When a clause is not unit under the current assignment, the watched literals point at two +//! non-false literals. When a clause is unit and thus propagating, the true literal is watched and +//! in position 0, the other watched literal is the one with the largest decision level and kept in +//! position 1. When a clause becomes satisfied before becoming unit the watches can be kept as they +//! were. +//! +//! When a literal is assigned false that invariant can be invalidated. This can be detected by +//! scanning the watches of the assigned literal. When the assignment is processed the watches are +//! moved to restore that invariant. Unless there is a conflict, i.e. a clause with no non-false +//! literals, this can always be done. This also finds all clauses that became unit. The new unit +//! clauses are exactly those clauses where no two non-false literals can be found. +//! +//! There is no need to update watchlists on backtracking, as unassigning variables cannot +//! invalidate the invariant. +//! +//! See [Section 4.5.1 of the "Handbook of Satisfiability"][handbook-ch4] for more details and +//! references. +//! +//! As a further optimization we use blocking literals. This means that each watch stores a literal +//! of the clause that is different from the watched literal. It can be the other watched literal or +//! any unwatched literal. When that literal is true, the clause is already satisfied, meaning that +//! no watches need to be updated. This can be detected by just looking at the watch, avoiding +//! access of the clause database. This variant was introduced by [Niklas Sörensson and Niklas Eén +//! in "MINISAT 2.1 and MINISAT++1.0 — SAT Race 2008 Editions"][minisat-2.1]. +//! +//! [handbook-ch4]: https://www.satassociation.org/articles/FAIA185-0131.pdf +//! [minisat-2.1]: https://www.cril.univ-artois.fr/SAT09/solvers/booklet.pdf + +use partial_ref::{partial, PartialRef}; + +use varisat_formula::Lit; + +use crate::{ + clause::{db, ClauseRef}, + context::{parts::*, Context}, +}; + +/// A watch on a long clause. +#[derive(Copy, Clone)] +pub struct Watch { + /// Clause which has the referring lit in position 0 or 1. + pub cref: ClauseRef, + /// A lit of the clause, different from the referring lit. + pub blocking: Lit, +} + +/// Watchlists to detect clauses that became unit. +pub struct Watchlists { + /// Contains only valid data for indices of assigned variables. + watches: Vec<Vec<Watch>>, + /// Whether watchlists are present + enabled: bool, +} + +impl Default for Watchlists { + fn default() -> Watchlists { + Watchlists { + watches: vec![], + enabled: true, + } + } +} + +impl Watchlists { + /// Update structures for a new variable count. + pub fn set_var_count(&mut self, count: usize) { + self.watches.resize(count * 2, vec![]); + } + + /// Start watching a clause. + /// + /// `lits` have to be the first two literals of the given clause. + pub fn watch_clause(&mut self, cref: ClauseRef, lits: [Lit; 2]) { + if !self.enabled { + return; + } + + for i in 0..2 { + let watch = Watch { + cref, + blocking: lits[i ^ 1], + }; + self.add_watch(!lits[i], watch); + } + } + + /// Return watches for a given literal. + pub fn watched_by_mut(&mut self, lit: Lit) -> &mut Vec<Watch> { + &mut self.watches[lit.code()] + } + + /// Make a literal watch a clause. + pub fn add_watch(&mut self, lit: Lit, watch: Watch) { + self.watches[lit.code()].push(watch) + } + + /// Are watchlists enabled. + pub fn enabled(&self) -> bool { + self.enabled + } + + /// Clear and disable watchlists. + /// + /// Actual clearing of the watchlists is done on re-enabling of the watchlists. + pub fn disable(&mut self) { + self.enabled = false; + } +} + +/// Enable and rebuild watchlists. +pub fn enable_watchlists(mut ctx: partial!(Context, mut WatchlistsP, ClauseAllocP, ClauseDbP)) { + let (watchlists, mut ctx) = ctx.split_part_mut(WatchlistsP); + if watchlists.enabled { + return; + } + + for watchlist in watchlists.watches.iter_mut() { + watchlist.clear(); + } + + watchlists.enabled = true; + + let (alloc, mut ctx) = ctx.split_part(ClauseAllocP); + + for cref in db::clauses_iter(&ctx.borrow()) { + let lits = alloc.clause(cref).lits(); + watchlists.watch_clause(cref, [lits[0], lits[1]]); + } +} |