Skip to content

Commit

Permalink
chore(sat): Move clause minimization to independent file
Browse files Browse the repository at this point in the history
  • Loading branch information
@arbimo
arbimo committed Nov 15, 2024
1 parent ef72b71 commit df7051c
Show file tree
Hide file tree
Showing 2 changed files with 220 additions and 205 deletions.
208 changes: 3 additions & 205 deletions solver/src/core/state/domains.rs
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@
use itertools::Itertools;

use crate::backtrack::{Backtrack, DecLvl, DecisionLevelClass, EventIndex, ObsTrail};
use crate::collections::ref_store::RefMap;
use crate::core::literals::{Disjunction, DisjunctionBuilder, ImplicationGraph, LitSet};
Expand All @@ -8,12 +6,13 @@ use crate::core::state::event::Event;
use crate::core::state::int_domains::IntDomains;
use crate::core::state::{Cause, DomainsSnapshot, Explainer, Explanation, ExplanationQueue, InvalidUpdate, OptDomain};
use crate::core::*;
use std::collections::HashSet;
use std::fmt::{Debug, Formatter};

#[cfg(debug_assertions)]
pub mod witness;

mod minimize;

/// Structure that contains the domains of optional variable.
///
/// Internally an optional variable is split between
Expand Down Expand Up @@ -519,215 +518,14 @@ impl Domains {
#[cfg(debug_assertions)]
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);
let clause = minimize::minimize_clause(clause, self, explainer);

#[cfg(debug_assertions)]
debug_assert!(!witness::pruned_by_clause(&clause), "Post minimization: {clause:?}");

Conflict { clause, resolved }
}

/// Minimizes the clause by removing any redundant literals.
///
/// This corresponds to clause minimization.
/// ref: Efficient All-UIP Learned Clause Minimization, Fleury and Biere (SAT21)
fn minimize_clause(&mut self, clause: Disjunction, explainer: &mut impl Explainer) -> Disjunction {
#[derive(Clone, Copy)]
struct Elem {
lit: Lit,
index: EventIndex,
dl: DecLvl,
}
// preprocessed the elemends of the clause so that we have their negation and their order by the inference time
// as a side effect, they are grouped by decision level
let elems = clause
.literals()
.iter()
.copied()
.map(|l| Elem {
lit: !l,
index: self.implying_event(!l).unwrap(),
dl: self.entailing_level(!l),
})
.sorted_by_key(|e| e.index)
.collect_vec();

// decisions levels for which at least one element of the clause appears
let decision_levels: HashSet<_> = elems.iter().map(|e| e.dl).collect();

#[derive(Default)]
struct Res {
clause: Vec<Lit>,
/// literals {l1, ..., ln} such that C => !li
redundant: LitSet,
/// literals {l1, ..., ln} such that C =/=> !li
not_redundant_negs: LitSet,
queue: Vec<(u32, Lit)>,
}
impl Res {
/// Add a literal to the clause (marking i as redundant for future calls)
fn add(&mut self, l: Lit) {
self.clause.push(!l);
self.mark_redundant(l);
}
/// Records that C => l
fn mark_redundant(&mut self, l: Lit) {
self.redundant.insert(l)
}
/// Records that C =/=> l
fn mark_not_redundant(&mut self, l: Lit) {
// we insert the negation, to facilitate the checking
self.not_redundant_negs.insert(!l);
}
/// Returns true if it it is known that C => l
fn known_redundant(&self, l: Lit) -> bool {
self.redundant.contains(!l)
}
/// Returns true if it it is known that C =/=> l
fn known_not_redundant(&self, l: Lit) -> bool {
// if this is true, then there is a literal li such that C =/=> li and !li => !l
// the latter means that l => li, thus it can *not* be the case that C => l, otherwise, we would have C => li
self.not_redundant_negs.contains(!l)
}
fn redundant_cached(&self, l: Lit) -> Option<bool> {
if self.known_redundant(l) {
Some(true)
} else if self.known_not_redundant(l) {
Some(false)
} else {
None // unknown
}
}
fn check_redundant(
&mut self,
l: Lit,
doms: &Domains,
explainer: &mut dyn Explainer,
decision_levels: &HashSet<DecLvl>,
) -> bool {
// we will go depth first to search for an obviously not redundant literal
let mut depth = 1;
// stack of the depth first search. First element is the depth in the search tree second element is the literal we want to classify
// note: we only reuse the queue to avoid reallocation
self.queue.clear();
self.queue.push((1, l));

// we do a depth first search until we find a non-redundant or exhaust the space
// - if we find a non-redundant, we will immediatly unwind the stack, mark all its parents as non-redudant as well and return false
// - when a literal is shown redundant it is removed from the queue
// - if a literal is in an unknown state we add all its implicants to the queue. If we come back to it (tree depth decreased) it means
// all its children were shown redundant and we can classify it as redundant as well
// We cache all intermediate results to keep the complexity linear in the size of the trail
loop {
if let Some((d, cur)) = self.queue.last().copied() {
if d == depth - 1 {
// we have exhausted all children, and all are redundant
// (otherwise, we would have unwound the stack completely)
self.mark_redundant(l);
depth -= 1;
self.queue.pop();
} else {
debug_assert_eq!(d, depth);
let status = self.redundant_cached(cur).or_else(|| {
// no known classification, try the different rule for immediate classification
let dec_lvl = doms.entailing_level(cur);
if dec_lvl == DecLvl::ROOT {
// entailed at root => redundant
self.mark_redundant(cur);
Some(true)
} else if !decision_levels.contains(&dec_lvl) {
// no literals from the clause on this decision level => not redundant
self.mark_not_redundant(cur);
Some(false)
} else {
let Some(event) = doms.implying_event(cur) else {
unreachable!()
};
let event = doms.get_event(event);
if event.cause == Origin::DECISION {
// decision => not redundant
self.mark_not_redundant(cur);
Some(false)
} else {
// unknown we will need to look at its implicants (that will become children in the search tree)
None
}
}
});
match status {
Some(true) => {
// redundant, dequeue
self.queue.pop();
}
Some(false) => {
// not redundant => unwind stack, marking all parent as not redundant
while let Some((d, l)) = self.queue.pop() {
if d == depth - 1 {
// we changed level, this literal is our predecessor and thus not redundant
self.mark_not_redundant(l);
// mark next
depth = d;
}
}
// return final classification
break false;
}
None => {
// unknown status, enqueue all antecedants
// classification will be made when we come back to it
for antecedant in doms.implying_literals(cur, explainer).unwrap() {
self.queue.push((depth + 1, antecedant));
}
depth += 1;
}
}
}
} else {
// finished depth first search without encountering a single non-redundant
// classify the literal as redundant
break true;
}
}
}
}
let mut res = Res::default();

// iterate on all literals, grouped by decision level
let mut next = 0;
while next < elems.len() {
// create a slice of all elements on the same decision level
let first_on_level = elems[next];
let level = first_on_level.dl;
let mut last_on_level = next;
while last_on_level + 1 < elems.len() && elems[last_on_level + 1].dl == level {
last_on_level += 1;
}
let on_level = &elems[next..=last_on_level];

// TODO: attempt to shrink to UIP

// minimize the element on the decision level
for (i, e) in on_level.iter().copied().enumerate() {
let l = e.lit;
if i == 0 {
// first on level, cannot be redundant
res.add(l);
} else {
let redundant = res.check_redundant(l, self, explainer, &decision_levels);
if !redundant {
// literal is not redundant, add it to the clause
res.add(l);
}
}
}

// proceed to first element of next decision level
next = last_on_level + 1;
}

Disjunction::new(res.clause)
}

/// Returns all decisions that were taken since the root decision level.
pub fn decisions(&self) -> Vec<(DecLvl, Lit)> {
let mut decs = Vec::new();
Expand Down
Loading

0 comments on commit df7051c

Please sign in to comment.