CVC3
2.4.1
|
#include <xchaff_solver.h>
Protected Member Functions | |
void | real_solve (void) |
int | preprocess (bool allowNewClauses) |
int | deduce (void) |
bool | decide_next_branch (void) |
int | analyze_conflicts (void) |
int | conflict_analysis_grasp (void) |
int | conflict_analysis_zchaff (void) |
void | back_track (int level) |
void | init (void) |
void | mark_vars_at_level (ClauseIdx cl, int var_idx, int dl) |
int | find_max_clause_dlevel (ClauseIdx cl) |
void | set_var_value (int var, int value, ClauseIdx ante, int dl) |
void | set_var_value_not_current_dl (int v, vector< CLitPoolElement * > &neg_ht_clauses) |
void | set_var_value_with_current_dl (int v, vector< CLitPoolElement * > &neg_ht_clauses) |
void | unset_var_value (int var) |
void | run_periodic_functions (void) |
void | update_var_stats (void) |
bool | time_out (void) |
void | delete_unrelevant_clauses (void) |
Class**********************************************************************
Synopsis [Sat Solver]
Description [This class contains the process and datastructrues to solve the Sat problem.]
SeeAlso []
Definition at line 148 of file xchaff_solver.h.
CSolver::CSolver | ( | void | ) |
Definition at line 43 of file xchaff_solver.cpp.
References _assignment_hook, _decision_hook, _deduction_hook, _dlevel, _dlevel_hook, _num_marked, _params, _stats, CSolverParameters::allow_clause_deletion, CSolverParameters::allow_multiple_conflict, CSolverParameters::allow_multiple_conflict_clause, CSolverParameters::allow_restart, CSolverParameters::back_track_complete, CSolverParameters::base_randomness, CSolverParameters::bubble_init_step, CSolverParameters::clause_deletion_interval, CSolverParameters::decision_strategy, dlevel(), CSolverStats::finish_cpu_time, CSolverStats::finish_world_time, CSolverStats::is_mem_out, CSolverStats::is_solver_started, CSolverStats::last_cpu_time, CSolverParameters::max_conflict_clause_length, CSolverStats::max_dlevel, CSolverParameters::max_unrelevance, CSolverParameters::min_num_clause_lits_for_delete, CSolverParameters::next_restart_backtrack, CSolverParameters::next_restart_time, CSolverStats::num_backtracks, CSolverStats::num_decisions, CSolverStats::num_implications, CSolverStats::outcome, CSolverParameters::preprocess_strategy, CSolverParameters::randomness, CSolverParameters::restart_backtrack_incr, CSolverParameters::restart_backtrack_incr_incr, CSolverParameters::restart_randomness, CSolverParameters::restart_time_incr_incr, CSolverParameters::restart_time_increment, CSolverStats::start_cpu_time, CSolverStats::start_world_time, CSolverParameters::time_limit, CSolverStats::total_bubble_move, UNKNOWN, and CSolverParameters::verbosity.
CSolver::~CSolver | ( | ) |
Definition at line 101 of file xchaff_solver.cpp.
References _assignment_stack, _stats, CSolverStats::is_solver_started, and CDatabase::variables().
|
protected |
Definition at line 763 of file xchaff_solver.cpp.
References _addedUnitClauses, _conflicts, _implication_queue, _stats, analyze_conflicts(), CONFLICT, decide_next_branch(), deduce(), CDatabase::find_unit_literal(), CSolverStats::is_mem_out, MEM_OUT, CSolverStats::outcome, queue_implication(), run_periodic_functions(), SATISFIABLE, TIME_OUT, time_out(), and UNSATISFIABLE.
Referenced by continueCheck(), and solve().
|
protected |
Definition at line 706 of file xchaff_solver.cpp.
References _params, CDatabase::clause(), CDatabase::clauses(), CONFLICT, deduce(), CVariable::dlevel(), std::endl(), CDatabase::find_unit_literal(), CVariable::lits_count(), NO_CONFLICT, NULL_CLAUSE, num_free_variables(), CClause::num_lits(), queue_implication(), UNKNOWN, CVariable::value(), CDatabase::variable(), CDatabase::variables(), and CSolverParameters::verbosity.
Referenced by solve().
|
protected |
Definition at line 852 of file xchaff_solver.cpp.
References _assignment_stack, _conflicts, _deduction_hook, _deduction_hook_cookie, _implication_queue, _params, CSolverParameters::back_track_complete, CHECK, CONFLICT, dlevel(), find_max_clause_dlevel(), NO_CONFLICT, restart(), set_var_value(), UNKNOWN, CVariable::value(), CDatabase::variables(), and verify_integrity().
Referenced by preprocess(), and real_solve().
|
protected |
Definition at line 617 of file xchaff_solver.cpp.
References _conflicts, _decision_hook, _decision_hook_cookie, _dlevel_hook, _dlevel_hook_cookie, _implication_queue, _max_score_pos, _params, _stats, _var_order, CSolverParameters::base_randomness, CHECK, dlevel(), std::endl(), CSolverStats::max_dlevel, NULL_CLAUSE, CSolverStats::num_decisions, num_free_variables(), queue_implication(), CSolverParameters::randomness, CVariable::score(), UNKNOWN, CVariable::value(), and CDatabase::variables().
Referenced by real_solve().
|
protected |
Definition at line 912 of file xchaff_solver.cpp.
References conflict_analysis_zchaff().
Referenced by real_solve().
|
protected |
|
protected |
Definition at line 916 of file xchaff_solver.cpp.
References _assignment_stack, _conflict_lits, _conflicts, _implication_queue, _num_marked, _params, _stats, add_clause(), back_track(), CSolverParameters::back_track_complete, CHECK, CDatabase::clause(), CVariable::clear_marked(), dlevel(), dump_assignment_stack(), std::endl(), find_max_clause_dlevel(), CDatabase::find_unit_literal(), CVariable::in_new_cl(), CDatabase::is_conflict(), CVariable::is_marked(), CSolverStats::is_mem_out, mark_vars_at_level(), max_dlevel(), NULL_CLAUSE, queue_implication(), CVariable::set_in_new_cl(), CDatabase::variable(), and CDatabase::variables().
Referenced by analyze_conflicts().
|
protected |
Definition at line 830 of file xchaff_solver.cpp.
References _assignment_stack, _dlevel_hook, _dlevel_hook_cookie, _stats, CHECK, CHECK_FULL, dlevel(), dump(), std::endl(), CSolverStats::num_backtracks, num_free_variables(), unset_var_value(), and verify_integrity().
Referenced by conflict_analysis_zchaff(), and restart().
|
protected |
Definition at line 142 of file xchaff_solver.cpp.
References _assignment_stack, _last_var_lits_count, _stats, _var_order, CHECK, current_cpu_time(), current_world_time(), dump(), CDatabase::init(), CSolverStats::is_solver_started, CSolverStats::num_free_variables, CDatabase::num_variables(), CSolverStats::start_cpu_time, CSolverStats::start_world_time, and CDatabase::variables().
Referenced by solve().
|
protected |
Definition at line 890 of file xchaff_solver.cpp.
References _conflict_lits, _num_marked, CDatabase::clause(), dlevel(), CVariable::set_in_new_cl(), CVariable::set_marked(), and CDatabase::variable().
Referenced by conflict_analysis_zchaff().
|
protected |
Definition at line 447 of file xchaff_solver.cpp.
References CDatabase::_variables, CDatabase::clause(), dlevel(), FLIPPED, CClause::literals(), NULL_CLAUSE, and UNKNOWN.
Referenced by conflict_analysis_zchaff(), and deduce().
|
protected |
Definition at line 296 of file xchaff_solver.cpp.
References _assignment_hook, _assignment_hook_cookie, _stats, CDatabase::_variables, CHECK, CHECK_FULL, CVariable::dlevel(), dlevel(), dump(), std::endl(), CVariable::ht_ptr(), num_free_variables(), CSolverStats::num_implications, CVariable::set_antecedence(), set_var_value_not_current_dl(), set_var_value_with_current_dl(), UNKNOWN, CVariable::value(), and verify_integrity().
Referenced by deduce().
|
protected |
Definition at line 368 of file xchaff_solver.cpp.
References _conflicts, CLitPoolElement::direction(), dlevel(), CVariable::ht_ptr(), CDatabase::literal_value(), queue_implication(), CLitPoolElement::s_var(), CLitPoolElement::unset_ht(), CLitPoolElement::val(), CLitPoolElement::var_index(), and CDatabase::variable().
Referenced by set_var_value().
|
protected |
Definition at line 321 of file xchaff_solver.cpp.
References _conflicts, CLitPoolElement::direction(), CVariable::ht_ptr(), CDatabase::literal_value(), queue_implication(), CLitPoolElement::s_var(), CLitPoolElement::unset_ht(), CLitPoolElement::val(), CLitPoolElement::var_index(), and CDatabase::variable().
Referenced by set_var_value().
|
protected |
Definition at line 433 of file xchaff_solver.cpp.
References _assignment_hook, _assignment_hook_cookie, _max_score_pos, CHECK, std::endl(), NULL_CLAUSE, UNKNOWN, and CDatabase::variable().
Referenced by back_track().
|
protected |
Definition at line 109 of file xchaff_solver.cpp.
References _hooks, _params, _stats, CSolverParameters::allow_clause_deletion, CSolverParameters::allow_restart, CSolverParameters::clause_deletion_interval, current_cpu_time(), delete_unrelevant_clauses(), std::endl(), CSolverParameters::next_restart_backtrack, CSolverParameters::next_restart_time, CSolverStats::num_backtracks, CSolverStats::num_decisions, CSolverParameters::randomness, restart(), CSolverParameters::restart_backtrack_incr, CSolverParameters::restart_backtrack_incr_incr, CSolverParameters::restart_randomness, CSolverParameters::restart_time_incr_incr, CSolverParameters::restart_time_increment, update_var_stats(), and CSolverParameters::verbosity.
Referenced by real_solve().
|
protected |
Definition at line 601 of file xchaff_solver.cpp.
References _last_var_lits_count, _max_score_pos, _var_order, compare_var_stat(), CVariable::lits_count(), CVariable::score(), CVariable::var_score_pos(), CDatabase::variable(), and CDatabase::variables().
Referenced by restart(), and run_periodic_functions().
|
protected |
Definition at line 587 of file xchaff_solver.cpp.
References _params, _stats, current_cpu_time(), CSolverStats::start_cpu_time, and CSolverParameters::time_limit.
Referenced by real_solve().
|
protected |
Definition at line 513 of file xchaff_solver.cpp.
References _params, CDatabase::_stats, CDatabase::_unused_clause_idx_queue, CHECK, CHECK_FULL, CDatabase::clauses(), dump(), std::endl(), CClause::in_use(), CDatabase::init_num_clauses(), CClause::literal(), CDatabase::literal_value(), CDatabase::mark_clause_deleted(), CSolverParameters::max_conflict_clause_length, CSolverParameters::max_unrelevance, CDatabaseStats::mem_used_up, CSolverParameters::min_num_clause_lits_for_delete, CDatabase::num_deleted_clauses(), CDatabase::num_deleted_literals(), CClause::num_lits(), and CDatabase::variables().
Referenced by run_periodic_functions().
|
inline |
Definition at line 228 of file xchaff_solver.h.
References _params, and CSolverParameters::time_limit.
Referenced by Xchaff::SetBudget().
|
inline |
Definition at line 230 of file xchaff_solver.h.
References CDatabase::set_mem_limit().
Referenced by Xchaff::SetMemLimit().
|
inline |
Definition at line 233 of file xchaff_solver.h.
References _params, and CSolverParameters::decision_strategy.
|
inline |
Definition at line 235 of file xchaff_solver.h.
References _params, and CSolverParameters::preprocess_strategy.
|
inline |
Definition at line 237 of file xchaff_solver.h.
References _params, and CSolverParameters::allow_clause_deletion.
Referenced by Xchaff::DisableClauseDeletion(), and Xchaff::EnableClauseDeletion().
|
inline |
Definition at line 239 of file xchaff_solver.h.
References _params, and CSolverParameters::clause_deletion_interval.
|
inline |
Definition at line 241 of file xchaff_solver.h.
References _params, and CSolverParameters::max_unrelevance.
|
inline |
Definition at line 243 of file xchaff_solver.h.
References _params, and CSolverParameters::min_num_clause_lits_for_delete.
|
inline |
Definition at line 245 of file xchaff_solver.h.
References _params, and CSolverParameters::max_conflict_clause_length.
|
inline |
Definition at line 247 of file xchaff_solver.h.
References _params, and CSolverParameters::allow_multiple_conflict.
|
inline |
Definition at line 250 of file xchaff_solver.h.
References _params, and CSolverParameters::allow_multiple_conflict_clause.
|
inline |
Definition at line 253 of file xchaff_solver.h.
References _params, and CSolverParameters::base_randomness.
Referenced by Xchaff::SetRandomness().
|
inline |
Definition at line 256 of file xchaff_solver.h.
References current_world_time().
Referenced by Xchaff::SetRandSeed().
|
inline |
Definition at line 264 of file xchaff_solver.h.
References _dlevel_hook, and _dlevel_hook_cookie.
Referenced by Xchaff::RegisterDLevelHook().
|
inline |
Definition at line 266 of file xchaff_solver.h.
References _decision_hook, and _decision_hook_cookie.
Referenced by Xchaff::RegisterDecisionHook().
|
inline |
Definition at line 268 of file xchaff_solver.h.
References _assignment_hook, and _assignment_hook_cookie.
Referenced by Xchaff::RegisterAssignmentHook().
|
inline |
Definition at line 270 of file xchaff_solver.h.
References _deduction_hook, and _deduction_hook_cookie.
Referenced by Xchaff::RegisterDeductionHook().
|
inline |
Definition at line 274 of file xchaff_solver.h.
References _stats, and CSolverStats::outcome.
|
inline |
Definition at line 275 of file xchaff_solver.h.
References _stats, and CSolverStats::num_decisions.
Referenced by Xchaff::GetNumDecisions().
|
inline |
Definition at line 276 of file xchaff_solver.h.
References _stats, and CSolverStats::num_free_variables.
Referenced by back_track(), decide_next_branch(), preprocess(), and set_var_value().
|
inline |
Definition at line 279 of file xchaff_solver.h.
References _stats, and CSolverStats::max_dlevel.
Referenced by conflict_analysis_zchaff(), and Xchaff::GetMaxDLevel().
|
inline |
Definition at line 280 of file xchaff_solver.h.
References _stats, and CSolverStats::num_implications.
Referenced by Xchaff::GetNumImplications().
|
inline |
Definition at line 281 of file xchaff_solver.h.
References _stats, and CSolverStats::total_bubble_move.
|
inline |
Definition at line 283 of file xchaff_solver.h.
|
inline |
Definition at line 287 of file xchaff_solver.h.
Referenced by continueCheck(), elapsed_cpu_time(), init(), run_periodic_functions(), solve(), time_out(), and total_run_time().
|
inline |
Definition at line 296 of file xchaff_solver.h.
Referenced by continueCheck(), init(), set_random_seed(), and solve().
|
inline |
Definition at line 303 of file xchaff_solver.h.
References _stats, current_cpu_time(), and CSolverStats::last_cpu_time.
|
inline |
Definition at line 310 of file xchaff_solver.h.
References _stats, current_cpu_time(), CSolverStats::is_solver_started, and CSolverStats::start_cpu_time.
Referenced by Xchaff::GetBudgetUsed(), and Xchaff::GetTotalTime().
|
inline |
Definition at line 316 of file xchaff_solver.h.
References _stats, CSolverStats::finish_cpu_time, and CSolverStats::start_cpu_time.
|
inline |
Definition at line 321 of file xchaff_solver.h.
References _stats, CSolverStats::finish_world_time, and CSolverStats::start_world_time.
|
inline |
Definition at line 326 of file xchaff_solver.h.
References CDatabase::estimate_mem_usage().
Referenced by Xchaff::GetMemUsed().
|
inline |
Definition at line 329 of file xchaff_solver.h.
References _assignment_stack, _stats, CSolverStats::max_dlevel, and CDatabase::mem_usage().
|
inline |
Definition at line 337 of file xchaff_solver.h.
References _dlevel.
Referenced by add_clause(), back_track(), conflict_analysis_zchaff(), CSolver(), decide_next_branch(), deduce(), dump_assignment_stack(), find_max_clause_dlevel(), mark_vars_at_level(), restart(), set_var_value(), and set_var_value_not_current_dl().
|
inline |
Definition at line 340 of file xchaff_solver.h.
References _hooks.
|
inline |
Definition at line 345 of file xchaff_solver.h.
References _implication_queue, CHECK, and std::endl().
Referenced by add_clause(), conflict_analysis_zchaff(), decide_next_branch(), preprocess(), real_solve(), set_var_value_not_current_dl(), and set_var_value_with_current_dl().
int CSolver::add_variables | ( | int | new_vars | ) |
Definition at line 160 of file xchaff_solver.cpp.
References _assignment_stack, _last_var_lits_count, _stats, _var_order, CSolverStats::is_solver_started, CSolverStats::num_free_variables, and CDatabase::variables().
Referenced by Xchaff::AddVariables().
ClauseIdx CSolver::add_clause | ( | vector< long > & | lits, |
bool | addConflicts = true |
||
) |
Definition at line 179 of file xchaff_solver.cpp.
References _addedUnitClauses, CDatabase::_clauses, _conflicts, CDatabase::_stats, _stats, CDatabase::_unused_clause_idx_queue, CDatabase::clause(), CVariable::dlevel(), dlevel(), CDatabase::enlarge_lit_pool(), CDatabase::find_unit_literal(), CVariable::ht_ptr(), CClause::init(), CDatabase::is_conflict(), CSolverStats::is_solver_started, CDatabase::lit_pool_end(), CDatabase::lit_pool_free_space(), CDatabase::lit_pool_push_back(), CDatabase::literal_value(), CClause::literals(), CVariable::lits_count(), CDatabaseStats::num_added_clauses, CDatabaseStats::num_added_literals, CClause::num_lits(), queue_implication(), CLitPoolElement::set_ht(), UNKNOWN, CLitPoolElement::var_index(), CLitPoolElement::var_sign(), CDatabase::variable(), and CDatabase::variables().
Referenced by Xchaff::AddClause(), and conflict_analysis_zchaff().
void CSolver::verify_integrity | ( | void | ) |
Definition at line 886 of file xchaff_solver.cpp.
Referenced by back_track(), deduce(), and set_var_value().
|
inline |
Definition at line 358 of file xchaff_solver.h.
References _last_var_lits_count, _params, back_track(), dlevel(), std::endl(), CVariable::score(), update_var_stats(), CDatabase::variable(), CDatabase::variables(), and CSolverParameters::verbosity.
Referenced by deduce(), and run_periodic_functions().
int CSolver::solve | ( | bool | allowNewClauses | ) |
Definition at line 804 of file xchaff_solver.cpp.
References _dlevel_hook, _dlevel_hook_cookie, _stats, CONFLICT, current_cpu_time(), current_world_time(), CSolverStats::finish_cpu_time, CSolverStats::finish_world_time, init(), CSolverStats::outcome, preprocess(), real_solve(), and UNSATISFIABLE.
Referenced by Xchaff::Satisfiable().
int CSolver::continueCheck | ( | ) |
Definition at line 822 of file xchaff_solver.cpp.
References _stats, current_cpu_time(), current_world_time(), CSolverStats::finish_cpu_time, CSolverStats::finish_world_time, CSolverStats::outcome, and real_solve().
Referenced by Xchaff::Continue().
void CSolver::dump_assignment_stack | ( | ostream & | os = cout | ) |
Definition at line 463 of file xchaff_solver.cpp.
References _assignment_stack, dlevel(), std::endl(), FLIPPED, CVariable::get_antecedence(), and CDatabase::variable().
Referenced by conflict_analysis_zchaff(), and dump().
void CSolver::output_current_stats | ( | void | ) |
|
inline |
Definition at line 381 of file xchaff_solver.h.
References CDatabase::dump(), and dump_assignment_stack().
Referenced by back_track(), delete_unrelevant_clauses(), init(), and set_var_value().
|
protected |
Definition at line 151 of file xchaff_solver.h.
|
protected |
Definition at line 152 of file xchaff_solver.h.
Referenced by add_variables(), back_track(), conflict_analysis_zchaff(), deduce(), dump_assignment_stack(), init(), mem_usage(), and ~CSolver().
|
protected |
Definition at line 153 of file xchaff_solver.h.
Referenced by conflict_analysis_zchaff(), decide_next_branch(), deduce(), queue_implication(), and real_solve().
|
protected |
Definition at line 154 of file xchaff_solver.h.
Referenced by conflict_analysis_zchaff(), CSolver(), decide_next_branch(), deduce(), delete_unrelevant_clauses(), enable_cls_deletion(), preprocess(), restart(), run_periodic_functions(), set_allow_multiple_conflict(), set_allow_multiple_conflict_clause(), set_cls_del_interval(), set_decision_strategy(), set_max_conflict_clause_length(), set_max_unrelevance(), set_min_num_clause_lits_for_delete(), set_preprocess_strategy(), set_randomness(), set_time_limit(), and time_out().
|
protected |
Definition at line 155 of file xchaff_solver.h.
Referenced by add_clause(), add_variables(), back_track(), conflict_analysis_zchaff(), continueCheck(), cpu_run_time(), CSolver(), decide_next_branch(), elapsed_cpu_time(), init(), max_dlevel(), mem_usage(), num_decisions(), num_free_variables(), num_implications(), outcome(), real_solve(), run_periodic_functions(), set_var_value(), solve(), time_out(), total_bubble_move(), total_run_time(), world_run_time(), and ~CSolver().
|
protected |
Definition at line 157 of file xchaff_solver.h.
Referenced by add_hook(), and run_periodic_functions().
|
protected |
Definition at line 160 of file xchaff_solver.h.
Referenced by decide_next_branch(), unset_var_value(), and update_var_stats().
|
protected |
Definition at line 161 of file xchaff_solver.h.
Referenced by add_variables(), init(), restart(), and update_var_stats().
|
protected |
Definition at line 162 of file xchaff_solver.h.
Referenced by add_variables(), decide_next_branch(), init(), and update_var_stats().
|
protected |
Definition at line 165 of file xchaff_solver.h.
Referenced by conflict_analysis_zchaff(), CSolver(), and mark_vars_at_level().
|
protected |
Definition at line 166 of file xchaff_solver.h.
Referenced by add_clause(), conflict_analysis_zchaff(), decide_next_branch(), deduce(), real_solve(), set_var_value_not_current_dl(), and set_var_value_with_current_dl().
|
protected |
Definition at line 167 of file xchaff_solver.h.
Referenced by conflict_analysis_zchaff(), and mark_vars_at_level().
|
protected |
Definition at line 170 of file xchaff_solver.h.
Referenced by back_track(), CSolver(), decide_next_branch(), RegisterDLevelHook(), and solve().
|
protected |
Definition at line 171 of file xchaff_solver.h.
Referenced by CSolver(), decide_next_branch(), and RegisterDecisionHook().
|
protected |
Definition at line 172 of file xchaff_solver.h.
Referenced by CSolver(), RegisterAssignmentHook(), set_var_value(), and unset_var_value().
|
protected |
Definition at line 173 of file xchaff_solver.h.
Referenced by CSolver(), deduce(), and RegisterDeductionHook().
|
protected |
Definition at line 174 of file xchaff_solver.h.
Referenced by back_track(), decide_next_branch(), RegisterDLevelHook(), and solve().
|
protected |
Definition at line 175 of file xchaff_solver.h.
Referenced by decide_next_branch(), and RegisterDecisionHook().
|
protected |
Definition at line 176 of file xchaff_solver.h.
Referenced by RegisterAssignmentHook(), set_var_value(), and unset_var_value().
|
protected |
Definition at line 177 of file xchaff_solver.h.
Referenced by deduce(), and RegisterDeductionHook().
|
protected |
Definition at line 180 of file xchaff_solver.h.
Referenced by add_clause(), and real_solve().