Skip to content

Commit

Permalink
snapshot
Browse files Browse the repository at this point in the history
  • Loading branch information
@shnarazk
shnarazk committed Nov 16, 2024
1 parent 7f7f7b1 commit d55e37c
Show file tree
Hide file tree
Showing 8 changed files with 124 additions and 119 deletions.
2 changes: 1 addition & 1 deletion Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ default = [
"keep_just_used_clauses",
"LRB_rewarding",
"reason_side_rewarding",
# "rephase",
"rephase",
"reward_annealing",
# "stochastic_local_search",
"trail_saving",
Expand Down
4 changes: 4 additions & 0 deletions src/assign/stack.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -212,6 +212,10 @@ impl Instantiate for AssignStack {
SolverEvent::Eliminate(vi) => {
self.make_var_eliminated(vi);
}
SolverEvent::Restart => {
#[cfg(feature = "trail_saving")]
self.clear_saved_trail();
}
SolverEvent::Stage(scale) => {
self.stage_scale = scale;
#[cfg(feature = "trail_saving")]
Expand Down
105 changes: 41 additions & 64 deletions src/cdb/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,12 +87,14 @@ pub trait ClauseDBIF:
/// reduce learnt clauses
/// # CAVEAT
/// *precondition*: decision level == 0.
fn reduce(&mut self, asg: &mut impl AssignIF, threshold: f64);
fn reduce(&mut self, threshold: f64);
/// remove all learnt clauses.
fn reset(&mut self);
/// update flags.
/// return `true` if it's learnt.
fn update_entanglement(&mut self, asg: &impl AssignIF, ci: ClauseIndex);
/// update LBD and return the new value
fn update_lbd(&mut self, asg: &impl AssignIF, ci: ClauseIndex) -> DecisionLevel;
/// record an asserted literal to unsat certification.
fn certificate_add_assertion(&mut self, lit: Lit);
/// save the certification record to a file.
Expand Down Expand Up @@ -518,21 +520,29 @@ impl ClauseDBIF for ClauseDB {
let rank: DecisionLevel = c.update_lbd(asg, lbd_temp);
self.lb_entanglement.update(rank as f64);
}
fn update_lbd(&mut self, asg: &impl AssignIF, ci: ClauseIndex) -> DecisionLevel {
let ClauseDB {
ref mut clause,
ref mut lbd_temp,
..
} = self;
let c = &mut clause[ci];
c.update_lbd(asg, lbd_temp)
}
/// reduce the number of 'learnt' or *removable* clauses.
#[cfg(feature = "keep_just_used_clauses")]
fn reduce(&mut self, asg: &mut impl AssignIF, threshold: f64) {
impl Clause {
fn extended_lbd(&self) -> f64 {
let l: f64 = self.len() as f64;
let r: f64 = self.rank as f64;
r + (l - r) / (l - r + 1.0)
}
}
fn reduce(&mut self, threshold: f64) {
// impl Clause {
// fn extended_lbd(&self) -> f64 {
// let l: f64 = self.len() as f64;
// let r: f64 = self.rank as f64;
// r + (l - r) / (l - r + 1.0)
// }
// }
// let ClauseDB {
// ref mut clause,
// ref mut lbd_temp,
// ref mut num_reduction,

// #[cfg(feature = "clause_rewarding")]
// ref tick,
// #[cfg(feature = "clause_rewarding")]
Expand All @@ -542,71 +552,38 @@ impl ClauseDBIF for ClauseDB {
self.num_reduction += 1;
// let mut keep: usize = 0;
// let mut alives: usize = 0;
// let mut perm: Vec<OrderedProxy<ClauseIndex>> = Vec::with_capacity(clause.len());
// let reduction_threshold = self.reduction_threshold + 4;
for ci in 1..self.clause.len() {
if self.clause[ci].is_dead() {
continue;
}
// alives += 1;
// keep += 1;
self.clause[ci].turn_off(FlagClause::NEW_CLAUSE);
// if self.clause[ci].is(FlagClause::FORWD_LINK)
// || self.clause[ci].is(FlagClause::BCKWD_LINK)
// {
// self.clause[ci].turn_off(FlagClause::FORWD_LINK);
// self.clause[ci].turn_off(FlagClause::BCKWD_LINK);
// continue;
// }
/* let fwd: bool = self.clause[ci].is(FlagClause::FORWD_LINK);
self.clause[ci].turn_off(FlagClause::FORWD_LINK);
if self.clause[ci].is(FlagClause::BCKWD_LINK) {
self.clause[ci].turn_off(FlagClause::BCKWD_LINK);
continue;
} */
if self.clause[ci].is(FlagClause::FORWD_LINK)
|| self.clause[ci].is(FlagClause::BCKWD_LINK)
{
let fwd = self.clause[ci].is(FlagClause::FORWD_LINK);
if fwd {
self.clause[ci].turn_off(FlagClause::FORWD_LINK);
}
let bck = self.clause[ci].is(FlagClause::BCKWD_LINK);
if bck {
self.clause[ci].turn_off(FlagClause::BCKWD_LINK);
}
let new = self.clause[ci].is(FlagClause::NEW_CLAUSE);
if new {
self.clause[ci].turn_off(FlagClause::NEW_CLAUSE);
}
if !self.clause[ci].is(FlagClause::LEARNT) {
continue;
}
/* let bwd: bool = self.clause[ci].is(FlagClause::BCKWD_LINK);
if bwd {
self.clause[ci].turn_off(FlagClause::BCKWD_LINK);
} */
if self.clause[ci].is(FlagClause::LEARNT) {
let ClauseDB {
ref mut clause,
ref mut lbd_temp,
..
} = self;
if clause[ci].rank < threshold as DecisionLevel {
continue;
}
clause[ci].update_lbd(asg, lbd_temp);
if threshold < clause[ci].extended_lbd() {
// keep -= 1;
// perm.push(OrderedProxy::new(ci, c.rank as f64));
self.delete_clause(ci);
continue;
}
if bck {
continue;
}
// alives += 1;
// keep += 1;
if (threshold as DecisionLevel) < self.clause[ci].rank
/* extended_lbd() */
{
// keep -= 1;
self.delete_clause(ci);
}
}
// let keep = perm.len().max(alives);
// if perm.is_empty() {
// return;
// }
// perm.sort();
// let threshold = perm[keep.min(perm.len() - 1)].value();
// for i in perm.iter().skip(keep) {
// // Being clause-position-independent, we keep or delete
// // all clauses that have a same value as a unit.
// if i.value() == threshold {
// continue;
// }
// self.delete_clause(i.to());
// }
}
#[cfg(not(feature = "keep_just_used_clauses"))]
#[allow(unreachable_code, unused_variables)]
Expand Down
1 change: 1 addition & 0 deletions src/cdb/vivify.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -145,6 +145,7 @@ impl VivifyIF for ClauseDB {
1 => {
self.certificate_add_assertion(vec[0]);
asg.assign_at_root_level(vec[0])?;
state.stm.handle(SolverEvent::Assert(vec[0].vi()));
num_assert += 1;
}
_ => {
Expand Down
1 change: 1 addition & 0 deletions src/processor/eliminate.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -167,6 +167,7 @@ pub fn eliminate_var(
*/
elim[vi].clear();
asg.handle(SolverEvent::Eliminate(vi));
state.stm.handle(SolverEvent::Eliminate(vi));
elim.backward_subsumption_check(asg, cdb)
}

Expand Down
7 changes: 5 additions & 2 deletions src/solver/conflict.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -376,8 +376,11 @@ fn conflict_analyze(
}

if max_lbd < cdb[ci].rank {
max_lbd = cdb[ci].rank;
ci_with_max_lbd = Some(ci);
let r = cdb.update_lbd(asg, ci);
if max_lbd < r {
max_lbd = r;
ci_with_max_lbd = Some(ci);
}
}
assert_eq!(
p,
Expand Down
116 changes: 66 additions & 50 deletions src/solver/search.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ const STAGE_SIZE: usize = 32;
pub struct SearchState {
num_reduction: usize,
reduce_step: usize,
next_restart: usize,
next_reduce: usize,
current_core: usize,
current_span: usize,
Expand Down Expand Up @@ -63,6 +64,7 @@ pub trait SolveIF {
macro_rules! RESTART {
($asg: expr, $cdb: expr, $state: expr) => {
$asg.cancel_until($asg.root_level());
$asg.handle(SolverEvent::Restart);
$cdb.handle(SolverEvent::Restart);
$state.handle(SolverEvent::Restart);
};
Expand Down Expand Up @@ -424,6 +426,7 @@ impl SolveIF for Solver {
num_reduction: 0,
reduce_step: (nv + nc) as usize,
next_reduce: 64,
next_restart: 1024,
from_segment_beginning: 0,
current_core: asg.derefer(assign::property::Tusize::NumUnassertedVar),
current_span: 1,
Expand Down Expand Up @@ -463,6 +466,7 @@ impl SolveIF for Solver {
cdb.update_activity_tick();

if asg.root_level() == handle_conflict(asg, cdb, state, &cc)? {
state.stm.handle(SolverEvent::Assert(0));
// let nv: u32 = asg.derefer(assign::Tusize::NumUnassertedVar).ilog2();
// let nc: u32 = cdb
// .iter()
Expand All @@ -471,9 +475,29 @@ impl SolveIF for Solver {
// .ilog2();
// ss.reduce_step = ((nv + nc) as usize + ss.reduce_step) / 2;
}
let num_conflict = asg.derefer(assign::Tusize::NumConflict);
let with_restart = ss.next_restart <= num_conflict
&& 1.0 <= cdb.refer(cdb::property::TEma::LBD).trend();
// && (ents + 1.0 < lbd || 1.0 <= cdb.refer(cdb::property::TEma::LBD).trend())
if with_restart {
RESTART!(asg, cdb, state);
// asg.clear_asserted_literals(cdb)?;
// let lbd = cdb.refer(cdb::property::TEma::LBD).get();
// let ent: f64 = cdb.refer(cdb::property::TEma::Entanglement).get_slow();
// let k: f64 = (state.stm.current_segment() as f64).log2();
// let ratio: f64 = state.stm.segment_progress_ratio();
// let x: f64 = k * (2.0 * ratio - 1.0);
// let sgm = |x: f64| 1.0 / (1.0 + (-x).exp());
// ss.next_restart = num_conflict + (((ent + lbd) * sgm(x)) as usize).max(6);
ss.next_restart = num_conflict + 10;

#[cfg(feature = "trace_equivalency")]
cdb.check_consistency(asg, "before simplify");

asg.clear_asserted_literals(cdb)?;
}
ss.from_segment_beginning += 1;
if ss.current_span <= ss.from_segment_beginning {
let with_restart = 1.0 < cdb.refer(cdb::property::TEma::LBD).trend();
ss.from_segment_beginning = 0;

#[cfg(feature = "graph_view")]
Expand All @@ -482,36 +506,22 @@ impl SolveIF for Solver {
let next_stage: Option<bool> = state
.stm
.prepare_new_stage(asg.derefer(assign::Tusize::NumConflict));
if with_restart || next_stage.is_some() {
RESTART!(asg, cdb, state);

#[cfg(any(feature = "best_phases_tracking", feature = "rephase"))]
if ss.with_rephase {
asg.select_rephasing_target();
asg.clear_asserted_literals(cdb)?;
if next_stage == Some(true) {
ss.with_rephase = false;
}
}

#[cfg(feature = "trace_equivalency")]
cdb.check_consistency(asg, "before simplify");
}
ss.current_span = state.stm.current_span() as usize;
let scale = state.stm.current_scale();
asg.handle(SolverEvent::Stage(scale));
if let Some(new_segment) = next_stage {
if new_segment && !with_restart {
RESTART!(asg, cdb, state);
ss.next_restart += 10;
}
// a beginning of a new cycle
{
let stm = &state.stm;
let b: f64 = stm.segment_starting_cycle() as f64;
let n: f64 = stm.current_cycle() as f64 - b;

if cfg!(feature = "reward_annealing") {
let k: f64 = (stm.current_segment() as f64).log2();
let ratio: f64 = stm.segment_progress_ratio();
const SLOP: f64 = 8.0;
const R: (f64, f64) = (0.84, 0.995);
const R: (f64, f64) = (0.88, 0.995);
let d: f64 = R.1 - (R.1 - R.0) * SLOP / (k + SLOP);
let x: f64 = k * (2.0 * ratio - 1.0);
let r = {
Expand All @@ -520,45 +530,46 @@ impl SolveIF for Solver {
};
asg.update_activity_decay(r);
}

let num_restart = asg.derefer(assign::Tusize::NumRestart);
if ss.next_reduce <= num_restart {
let ent: f64 = cdb.refer(cdb::property::TEma::Entanglement).get_slow();
let lbd: f64 = cdb.refer(cdb::property::TEma::LBD).get_slow();
// Note: val can be inf. It got better results.
let val: f64 = 0.5 * ent.min(lbd) + ent.max(lbd) / (1.0 + n).log2();
state.reduction_threshold = val;
cdb.reduce(asg, val);
ss.num_reduction += 1;
ss.reduce_step += 1;
ss.next_reduce = ss.reduce_step + num_restart;

if cfg!(feature = "clause_vivification") {
cdb.vivify(asg, state)?;
}
if cfg!(feature = "clause_elimination")
&& !cfg!(feature = "incremental_solver")
&& ss.num_reduction % 8 == 0
{
let mut elim = Eliminator::instantiate(&state.config, &state.cnf);
state.flush("clause subsumption, ");
elim.simplify(asg, cdb, state, false)?;
asg.eliminated.append(elim.eliminated_lits());
state[Stat::Simplify] += 1;
state[Stat::SubsumedClause] = elim.num_subsumed;
}
let num_restart = asg.derefer(assign::Tusize::NumRestart);
if new_segment && ss.next_reduce <= num_restart {
let lbd = cdb.refer(cdb::property::TEma::LBD).get();
let b: f64 = state.stm.segment_starting_cycle() as f64;
let _n: f64 = state.stm.current_cycle() as f64 - b;
let ents: f64 = cdb.refer(cdb::property::TEma::Entanglement).get_slow();
// Note: val can be inf. It got better results.
// let val: f64 = 0.5 * ent.min(lbd) + ent.max(lbd) / (1.0 + n).log2();
let val = (ents + lbd).sqrt().min(1.0);
state.reduction_threshold = val;
cdb.reduce(val);
ss.num_reduction += 1;
ss.reduce_step += ss.current_core.ilog2() as usize;
ss.next_reduce = ss.reduce_step + num_restart;

if cfg!(feature = "clause_vivification") {
cdb.vivify(asg, state)?;
}
if cfg!(feature = "clause_elimination")
&& !cfg!(feature = "incremental_solver")
&& ss.num_reduction % 8 == 0
{
let mut elim = Eliminator::instantiate(&state.config, &state.cnf);
state.flush("clause subsumption, ");
elim.simplify(asg, cdb, state, false)?;
let el = elim.eliminated_lits();
if 0 < el.len() {
asg.eliminated.append(el);
}
state[Stat::Simplify] += 1;
state[Stat::SubsumedClause] = elim.num_subsumed;
}
}
state
.stm
.set_span_base(state.c_lvl.get_slow() - state.b_lvl.get_slow());

asg.clear_asserted_literals(cdb)?;
dump_stage(asg, cdb, state, &ss.previous_stage);

#[cfg(feature = "rephase")]
rephase(asg, cdb, state, ss);

if new_segment {
state.exploration_rate_ema.update(1.0);
}
Expand All @@ -577,6 +588,11 @@ impl SolveIF for Solver {
return Err(SolverError::UndescribedError);
}
}
#[cfg(feature = "rephase")]
if with_restart {
asg.select_rephasing_target();
rephase(asg, cdb, state, ss);
}
}
if let Some(na) = asg.best_assigned() {
if ss.current_core < na && ss.core_was_rebuilt.is_none() {
Expand Down
Loading

0 comments on commit d55e37c

Please sign in to comment.