#[cfg(feature = "clause_vivification")]
use super::vivify::vivify;
use {
super::{
conflict::handle_conflict,
restart::{self, ProgressUpdate, RestartDecision, RestartIF, Restarter},
Certificate, Solver, SolverEvent, SolverResult,
},
crate::{
assign::{self, AssignIF, AssignStack, PropagateIF, VarManipulateIF, VarSelectIF},
cdb::{ClauseDB, ClauseDBIF},
processor::{EliminateIF, Eliminator},
state::{Stat, State, StateIF},
types::*,
},
};
pub trait SolveIF {
fn solve(&mut self) -> SolverResult;
}
macro_rules! RESTART {
($asg: expr, $rst: expr) => {
$asg.cancel_until($asg.root_level);
$rst.handle(SolverEvent::Restart);
};
}
impl SolveIF for Solver {
fn solve(&mut self) -> SolverResult {
let Solver {
ref mut asg,
ref mut cdb,
ref mut elim,
ref mut rst,
ref mut state,
} = self;
if cdb.check_size().is_err() {
return Err(SolverError::OutOfMemory);
}
asg.num_asserted_vars = asg.stack_len();
state.progress_header();
state.progress(asg, cdb, elim, rst);
state.flush("");
state.flush("Preprocessing stage: ");
if 0 < asg.stack_len() {
elim.eliminate_satisfied_clauses(asg, cdb, false);
}
if elim.enable {
const USE_PRE_PROCESSING_ELIMINATOR: bool = true;
state.flush("phasing...");
elim.activate();
elim.prepare(asg, cdb, true);
for vi in 1..=asg.num_vars {
if asg.assign(vi).is_some() {
continue;
}
if let Some((p, m)) = elim.stats(vi) {
#[cfg(not(feature = "incremental_solver"))]
{
if m == 0 {
let l = Lit::from_assign(vi, true);
if asg.assign_at_root_level(l).is_err() {
return Ok(Certificate::UNSAT);
}
} else if p == 0 {
let l = Lit::from_assign(vi, false);
if asg.assign_at_root_level(l).is_err() {
return Ok(Certificate::UNSAT);
}
}
}
asg.var_mut(vi).set(Flag::PHASE, m < p);
elim.enqueue_var(asg, vi, false);
}
}
if USE_PRE_PROCESSING_ELIMINATOR {
state.flush("simplifying...");
if elim.simplify(asg, cdb, rst, state).is_err() {
state.progress(asg, cdb, elim, rst);
if cdb.check_size().is_err() {
return Err(SolverError::OutOfMemory);
}
return Ok(Certificate::UNSAT);
}
for vi in 1..=asg.num_vars {
if asg.assign(vi).is_some() || asg.var(vi).is(Flag::ELIMINATED) {
continue;
}
match elim.stats(vi) {
Some((_, 0)) => (),
Some((0, _)) => (),
Some((p, m)) if m * 10 < p => asg.var_mut(vi).turn_on(Flag::PHASE),
Some((p, m)) if p * 10 < m => asg.var_mut(vi).turn_off(Flag::PHASE),
_ => (),
}
}
for vi in elim.sorted_iterator() {
asg.set_activity(*vi, 0.0);
}
asg.rebuild_order();
}
elim.stop(asg, cdb);
}
state.progress(asg, cdb, elim, rst);
let answer = search(asg, cdb, elim, rst, state);
state.progress(asg, cdb, elim, rst);
match answer {
Ok(true) => {
let model = asg.extend_model(cdb, elim.eliminated_lits());
#[cfg(debug)]
{
if let Some(cid) = cdb.validate(&model, true) {
panic!(
"Level {} generated assignment({:?}) falsifies {}:{:?}",
asg.decision_level(),
cdb.validate(&model, false).is_none(),
cid,
"asg.dump(&cdb[cid])",
);
}
}
if cdb.validate(&model, false).is_some() {
return Err(SolverError::SolverBug);
}
let vals = asg
.var_iter()
.skip(1)
.map(|v| i32::from(Lit::from((v.index, model[v.index]))))
.collect::<Vec<i32>>();
for v in asg.var_iter_mut().skip(1) {
if v.is(Flag::ELIMINATED) {
v.turn_off(Flag::ELIMINATED);
}
}
RESTART!(asg, rst);
Ok(Certificate::SAT(vals))
}
Ok(false) | Err(SolverError::NullLearnt) => {
RESTART!(asg, rst);
Ok(Certificate::UNSAT)
}
Err(e) => {
RESTART!(asg, rst);
Err(e)
}
}
}
}
fn search(
asg: &mut AssignStack,
cdb: &mut ClauseDB,
elim: &mut Eliminator,
rst: &mut Restarter,
state: &mut State,
) -> Result<bool, SolverError> {
let mut a_decision_was_made = false;
let mut last_core = 0;
let mut next_progress = 10_000;
let mut best_asserted = state.target.num_of_variables;
#[cfg(feature = "var_staging")]
let mut parity = false;
#[cfg(feature = "Luby_restart")]
rst.update(ProgressUpdate::Luby);
while 0 < asg.derefer(assign::property::Tusize::NumUnassignedVar) {
if !asg.remains() {
let lit = asg.select_decision_literal();
asg.assign_by_decision(lit);
a_decision_was_made = true;
}
let ci = asg.propagate(cdb);
if !ci.is_none() {
if asg.decision_level() == asg.root_level {
analyze_final(asg, state, &cdb[ci]);
return Ok(false);
}
asg.update_rewards();
cdb.update_rewards();
handle_conflict(asg, cdb, elim, rst, state, ci)?;
rst.update(ProgressUpdate::ASG(
asg.derefer(assign::property::Tusize::NumUnassignedVar),
));
if rst.restart() == Some(RestartDecision::Force) {
if let Some(new_cycle) = rst.stabilize() {
RESTART!(asg, rst);
let block_level = rst.derefer(restart::property::Tusize::TriggerLevel);
let num_cycle = rst.derefer(restart::property::Tusize::NumCycle);
let num_unreachable = asg.derefer(assign::property::Tusize::NumUnreachableVar);
asg.update_activity_decay(if new_cycle { None } else { Some(block_level) });
#[cfg(feature = "var_staging")]
{
parity = !parity;
asg.select_staged_vars(None, parity);
}
if last_core != num_unreachable || 0 == num_unreachable {
state.log(
asg.num_conflict,
format!(
"#cycle:{:>5}, core:{:>9}, level:{:>9},/cpr:{:>9.2}",
num_cycle,
num_unreachable,
block_level,
asg.refer(assign::property::TEma::PPC).get(),
),
);
last_core = num_unreachable;
}
if cdb.reduce(asg, asg.num_conflict) {
#[cfg(feature = "clause_vivification")]
if vivify(asg, cdb, elim, state).is_err() {
analyze_final(asg, state, &cdb[ci]);
return Ok(false);
}
if state.config.c_ip_int <= elim.to_simplify as usize {
elim.activate();
elim.simplify(asg, cdb, rst, state)?;
}
}
if next_progress < asg.num_conflict {
state.progress(asg, cdb, elim, rst);
next_progress = asg.num_conflict + 10_000;
}
} else {
RESTART!(asg, rst);
}
}
if asg.decision_level() == asg.root_level && asg.num_asserted_vars < asg.stack_len() {
asg.num_asserted_vars = asg.stack_len();
}
if a_decision_was_made {
a_decision_was_made = false;
} else {
state[Stat::NoDecisionConflict] += 1;
}
if let Some(na) = asg.best_assigned() {
if na < best_asserted {
state.flush("");
state.flush(format!("unreachable core: {}", na));
rst.handle(SolverEvent::ShrinkCore);
best_asserted = na;
}
}
if asg.num_conflict % (10 * state.reflection_interval) == 0 {
#[cfg(feature = "strategy_adaptation")]
adapt_modules(asg, rst, state);
if let Some(p) = state.elapsed() {
if 1.0 <= p {
return Err(SolverError::TimeOut);
}
} else {
return Err(SolverError::UndescribedError);
}
}
}
}
Ok(true)
}
#[cfg(feature = "strategy_adaptation")]
fn adapt_modules(asg: &mut AssignStack, rst: &mut Restarter, state: &mut State) {
let asg_num_conflict = asg.num_conflict;
if 10 * state.reflection_interval == asg_num_conflict {
RESTART!(asg, rst);
state.select_strategy(asg, cdb);
}
#[cfg(feature = "boundary_check")]
debug_assert!(state.strategy.1 != asg_num_conflict || 0 == asg.decision_level());
asg.handle(SolverEvent::Adapt(state.strategy, asg_num_conflict));
cdb.handle(SolverEvent::Adapt(state.strategy, asg_num_conflict));
rst.handle(SolverEvent::Adapt(state.strategy, asg_num_conflict));
}
fn analyze_final(asg: &mut AssignStack, state: &mut State, c: &Clause) {
let mut seen = vec![false; asg.num_vars + 1];
state.conflicts.clear();
if asg.decision_level() == 0 {
return;
}
for l in &c.lits {
let vi = l.vi();
if 0 < asg.level(vi) {
asg.var_mut(vi).turn_on(Flag::CA_SEEN);
}
}
let end = if asg.decision_level() <= asg.root_level {
asg.stack_len()
} else {
asg.len_upto(asg.root_level)
};
for l in asg.stack_range(asg.len_upto(0)..end) {
let vi = l.vi();
if seen[vi] {
if asg.reason(vi) == AssignReason::default() {
state.conflicts.push(!*l);
} else {
let level = asg.level_ref();
for l in &c[(c.len() != 2) as usize..] {
let vj = l.vi();
if 0 < level[vj] {
seen[vj] = true;
}
}
}
}
seen[vi] = false;
}
}