Skip to content

Commit

Permalink
Remove AssignStack::propagate_sandbox
Browse files Browse the repository at this point in the history
  • Loading branch information
@shnarazk
shnarazk committed Jul 21, 2024
1 parent 72a7c59 commit 1a8e201
Show file tree
Hide file tree
Showing 4 changed files with 62 additions and 38 deletions.
82 changes: 53 additions & 29 deletions src/assign/propagate.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,9 +41,9 @@ pub trait PropagateIF {
/// execute backjump in vivification sandbox
fn backtrack_sandbox(&mut self);
/// execute *boolean constraint propagation* or *unit propagation*.
fn propagate(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult;
/// `propagate` for vivification, which allows dead clauses.
fn propagate_sandbox(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult;
fn propagate(&mut self, cdb: &mut impl ClauseDBIF, sandbox: bool) -> PropagationResult;
// /// `propagate` for vivification, which allows dead clauses.
// fn propagate_sandbox(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult;
/// propagate then clear asserted literals
fn clear_asserted_literals(&mut self, cdb: &mut impl ClauseDBIF) -> MaybeInconsistent;
}
Expand Down Expand Up @@ -272,7 +272,7 @@ impl PropagateIF for AssignStack {
/// So Eliminator should call `garbage_collect` before me.
/// - The order of literals in binary clauses will be modified to hold
/// propagation order.
fn propagate(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult {
fn propagate(&mut self, cdb: &mut impl ClauseDBIF, sandbox: bool) -> PropagationResult {
#[cfg(feature = "boundary_check")]
macro_rules! check_in {
($cid: expr, $tag :expr) => {
Expand All @@ -285,9 +285,11 @@ impl PropagateIF for AssignStack {
}
macro_rules! conflict_path {
($lit: expr, $reason: expr) => {
self.dpc_ema.update(self.num_decision);
self.ppc_ema.update(self.num_propagation);
self.num_conflict += 1;
if !sandbox {
self.dpc_ema.update(self.num_decision);
self.ppc_ema.update(self.num_propagation);
self.num_conflict += 1;
}
return Err(($lit, $reason));
};
}
Expand All @@ -311,13 +313,15 @@ impl PropagateIF for AssignStack {
#[cfg(feature = "trail_saving")]
macro_rules! from_saved_trail {
() => {
if let cc @ Err(_) = self.reuse_saved_trail(cdb) {
self.num_propagation += 1;
self.num_conflict += 1;
self.num_reconflict += 1;
self.dpc_ema.update(self.num_decision);
self.ppc_ema.update(self.num_propagation);
return cc;
if !sandbox {
if let cc @ Err(_) = self.reuse_saved_trail(cdb) {
self.num_propagation += 1;
self.num_conflict += 1;
self.num_reconflict += 1;
self.dpc_ema.update(self.num_decision);
self.ppc_ema.update(self.num_propagation);
return cc;
}
}
};
}
Expand All @@ -329,13 +333,15 @@ impl PropagateIF for AssignStack {
let dl = self.decision_level();
from_saved_trail!();
while let Some(p) = self.trail.get(self.q_head) {
self.num_propagation += 1;
self.q_head += 1;
if !sandbox {
self.num_propagation += 1;
}
#[cfg(feature = "debug_propagation")]
{
assert!(!self.var[p.vi()].is(FlagVar::PROPAGATED));
self.var[p.vi()].turn_on(FlagVar::PROPAGATED);
}
self.q_head += 1;
let propagating = Lit::from(usize::from(*p));
let false_lit = !*p;

Expand Down Expand Up @@ -390,7 +396,14 @@ impl PropagateIF for AssignStack {
}
}
if other_value == Some(false) {
check_in!(ci, Propagate::EmitConflict(self.num_conflict + 1, other));
check_in!(
ci,
if sandbox {
Propagate::SandboxEmitConflict(self.num_conflict, propagating)
} else {
Propagate::EmitConflict(self.num_conflict + 1, other)
}
);
conflict_path!(
other,
if len == 0 {
Expand Down Expand Up @@ -419,19 +432,31 @@ impl PropagateIF for AssignStack {
#[cfg(feature = "chrono_BT")]
dl,
);
check_in!(cid, Propagate::BecameUnit(self.num_conflict, cached));
check_in!(
cid,
if sandbox {
Propagate::SandboxBecameUnit(self.num_conflict)
} else {
Propagate::BecameUnit(self.num_conflict, cached)
}
);
wli = c.next_watch(false_index);
}
}
from_saved_trail!();
if !sandbox {
from_saved_trail!();
}
}
let na: usize = self.q_head + self.num_eliminated_vars + self.num_asserted_vars;
if self.num_best_assign <= na && 0 < dl {
self.best_assign = true;
self.num_best_assign = na;
if !sandbox {
let na: usize = self.q_head + self.num_eliminated_vars + self.num_asserted_vars;
if self.num_best_assign <= na && 0 < dl {
self.best_assign = true;
self.num_best_assign = na;
}
}
Ok(())
}
/*
//
//## How to generate propagate_sandbox from propagate
//
Expand All @@ -442,7 +467,6 @@ impl PropagateIF for AssignStack {
// 1. delete codes about trail_saving
// 1. delete codes about stat counters: num_*, ema_*
// 1. delete comments
// 1. (allow dead clauses)
// 1. (allow eliminated vars)
//
fn propagate_sandbox(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult {
Expand Down Expand Up @@ -487,18 +511,17 @@ impl PropagateIF for AssignStack {
wli = c.next_watch(false_index);
continue 'next_clause;
}
let start = c.search_from as usize;
let len = c.len() - 2;
let start = c.search_from as usize;
for i in 0..c.len() - 2 {
let k = (i + start) % len + 2;
let lk = c[k];
if lit_assign!(self.var[lk.vi()], lk) != Some(false) {
let next = cdb.transform_by_updating_watch(wli, k);
check_in!(
ci,
Propagate::SandboxFindNewWatch(self.num_conflict, false_lit, !lk)
);
wli = next;
wli = cdb.transform_by_updating_watch(wli, k);
continue 'next_clause;
}
}
Expand Down Expand Up @@ -530,16 +553,17 @@ impl PropagateIF for AssignStack {
}
Ok(())
}
*/
fn clear_asserted_literals(&mut self, cdb: &mut impl ClauseDBIF) -> MaybeInconsistent {
debug_assert_eq!(self.decision_level(), self.root_level);
loop {
if self.remains() {
self.propagate_sandbox(cdb)
self.propagate(cdb, true)
.map_err(SolverError::RootLevelConflict)?;
}
self.propagate_at_root_level(cdb)?;
if self.remains() {
self.propagate_sandbox(cdb)
self.propagate(cdb, true)
.map_err(SolverError::RootLevelConflict)?;
} else {
break;
Expand Down
8 changes: 4 additions & 4 deletions src/cdb/vivify.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ impl VivifyIF for ClauseDB {
fn vivify(&mut self, asg: &mut AssignStack, state: &mut State) -> MaybeInconsistent {
const NUM_TARGETS: Option<usize> = Some(VIVIFY_LIMIT);
if asg.remains() {
asg.propagate_sandbox(self).map_err(|cc| {
asg.propagate(self, true).map_err(|cc| {
state.log(None, "By vivifier");
SolverError::RootLevelConflict(cc)
})?;
Expand All @@ -42,7 +42,7 @@ impl VivifyIF for ClauseDB {
asg.backtrack_sandbox();
debug_assert_eq!(asg.decision_level(), asg.root_level());
if asg.remains() {
asg.propagate_sandbox(self)
asg.propagate(self, true)
.map_err(SolverError::RootLevelConflict)?;
}

Expand Down Expand Up @@ -78,7 +78,7 @@ impl VivifyIF for ClauseDB {
decisions.push(!lit);
asg.assign_by_decision(!lit);
//## Rule 3
if let Err(cc) = asg.propagate_sandbox(self) {
if let Err(cc) = asg.propagate(self, true) {
let mut vec: Vec<Lit>;
match cc.1 {
AssignReason::BinaryLink(l) => {
Expand Down Expand Up @@ -159,7 +159,7 @@ impl VivifyIF for ClauseDB {
}
asg.backtrack_sandbox();
if asg.remains() {
asg.propagate_sandbox(self)
asg.propagate(self, true)
.map_err(SolverError::RootLevelConflict)?;
}
asg.clear_asserted_literals(self)?;
Expand Down
8 changes: 4 additions & 4 deletions src/processor/simplify.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -219,7 +219,7 @@ impl EliminateIF for Eliminator {
// self.eliminate_combination_limit = cdb.derefer(cdb::property::Tf64::LiteralBlockEntanglement);
self.eliminate(asg, cdb, state)?;
} else {
asg.propagate_sandbox(cdb)
asg.propagate(cdb, true)
.map_err(SolverError::RootLevelConflict)?;
}
if self.mode != EliminatorMode::Dormant {
Expand Down Expand Up @@ -422,7 +422,7 @@ impl Eliminator {
}
}
if asg.remains() {
asg.propagate_sandbox(cdb)
asg.propagate(cdb, true)
.map_err(SolverError::RootLevelConflict)?;
}
Ok(())
Expand All @@ -442,7 +442,7 @@ impl Eliminator {
loop {
let na = asg.stack_len();
self.eliminate_main(asg, cdb, state)?;
asg.propagate_sandbox(cdb)
asg.propagate(cdb, true)
.map_err(SolverError::RootLevelConflict)?;
if na == asg.stack_len()
&& (!self.is_running()
Expand Down Expand Up @@ -485,7 +485,7 @@ impl Eliminator {
}
self.backward_subsumption_check(asg, cdb)?;
debug_assert!(self.clause_queue.is_empty());
asg.propagate_sandbox(cdb)
asg.propagate(cdb, true)
.map_err(SolverError::RootLevelConflict)?;
}
self.clear_clause_queue(cdb);
Expand Down
2 changes: 1 addition & 1 deletion src/solver/search.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -425,7 +425,7 @@ impl SolveIF for Solver {
let lit = asg.select_decision_literal();
asg.assign_by_decision(lit);
}
let Err(cc) = asg.propagate(cdb) else {
let Err(cc) = asg.propagate(cdb, false) else {
continue;
};
if asg.decision_level() == asg.root_level() {
Expand Down

0 comments on commit 1a8e201

Please sign in to comment.