1 // *********************************************************************
2 // Copyright 2000-2004, Princeton University. All rights reserved.
3 // By using this software the USER indicates that he or she has read,
4 // understood and will comply with the following:
6 // --- Princeton University hereby grants USER nonexclusive permission
7 // to use, copy and/or modify this software for internal, noncommercial,
8 // research purposes only. Any distribution, including commercial sale
9 // or license, of this software, copies of the software, its associated
10 // documentation and/or modifications of either is strictly prohibited
11 // without the prior consent of Princeton University. Title to copyright
12 // to this software and its associated documentation shall at all times
13 // remain with Princeton University. Appropriate copyright notice shall
14 // be placed on all software copies, and a complete copy of this notice
15 // shall be included in all copies of the associated documentation.
16 // No right is granted to use in advertising, publicity or otherwise
17 // any trademark, service mark, or the name of Princeton University.
20 // --- This software and any associated documentation is provided "as is"
22 // PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
23 // OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
24 // PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR
25 // ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
26 // TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.
28 // Princeton University shall not be liable under any circumstances for
29 // any direct, indirect, special, incidental, or consequential damages
30 // with respect to any claim by USER or any third party on account of
31 // or arising from the use, or inability to use, this software or its
32 // associated documentation, even if Princeton University has been advised
33 // of the possibility of those damages.
34 // *********************************************************************
36 #ifndef __SAT_SOLVER__
37 #define __SAT_SOLVER__
39 #include "zchaff_version.h"
40 #include "zchaff_dbase.h"
62 typedef void(*HookFunPtrT)(void *) ;
63 typedef void(*OutsideConstraintHookPtrT)(CSolver * solver);
64 typedef bool(*SatHookPtrT)(CSolver * solver);
66 // **Struct********************************************************************
68 // Synopsis [Sat solver parameters ]
74 // ****************************************************************************
76 struct CSolverParameters {
87 int bound_update_frequency;
88 unsigned window_width;
100 unsigned head_activity;
101 unsigned tail_activity;
102 unsigned head_num_lits;
103 unsigned tail_num_lits;
115 // **Struct********************************************************************
117 // Synopsis [Sat solver statistics ]
123 // ****************************************************************************
125 struct CSolverStats {
126 bool been_reset; // when delete clause in incremental solving,
129 bool is_mem_out; // this flag will be set if memory out
130 double start_cpu_time;
131 double finish_cpu_time;
132 int current_randomness;
135 int next_cls_deletion;
136 int next_var_score_decay;
137 int num_free_variables;
138 int num_free_branch_vars;
139 long64 total_bubble_move;
141 int num_decisions_stack_conf;
142 int num_decisions_vsids;
143 int num_decisions_shrinking;
145 int shrinking_benefit;
146 int shrinking_cls_length;
150 long64 num_implications;
152 int num_del_orig_cls;
155 // **Class*********************************************************************
157 // Synopsis [Sat Solver]
159 // Description [This class contains the process and datastructrues to solve
164 // ****************************************************************************
166 inline bool cmp_var_stat(const pair<CVariable *, int> & v1,
167 const pair<CVariable *, int> & v2) {
168 return v1.second >= v2.second;
171 struct cmp_var_assgn_pos {
172 bool operator() (CVariable * v1, CVariable * v2) {
173 if (v1->dlevel() > v2->dlevel())
175 else if (v1->dlevel() < v2->dlevel())
177 else if (v1->assgn_stack_pos() > v2->assgn_stack_pos())
183 struct CImplication {
188 struct ImplicationQueue:queue<CImplication> {
189 void dump(ostream & os) {
190 queue<CImplication> temp(*this);
191 os << "Implication Queue Previous: " ;
192 while (!temp.empty()) {
193 CImplication a = temp.front();
194 os << "(" << ((a.lit & 0x1) ? "-" : "+") << (a.lit >> 1)
195 << ":" << a.antecedent << ") ";
201 class CSolver:public CDatabase {
203 int _id; // the id of the solver, in case
204 // we need to distinguish
205 bool _force_terminate;
206 CSolverParameters _params; // parameters for the solver
207 CSolverStats _stats; // statistics and states
209 int _dlevel; // current decision elvel
210 vector<vector<int>*>_assignment_stack;
211 queue<int> _recent_shrinkings;
212 bool _mark_increase_score; // used in mark_vars during
213 // multiple conflict analysis
214 long64 _implication_id;
215 ImplicationQueue _implication_queue;
217 // hook function run after certain number of decisions
218 vector<pair<int, pair<HookFunPtrT, int> > > _hooks;
219 OutsideConstraintHookPtrT _outside_constraint_hook;
220 SatHookPtrT _sat_hook; // hook function run after a satisfiable
221 // solution found, return true to continue
222 // solving and false to terminate as satisfiable
224 // these are for decision making
225 int _max_score_pos; // index the unassigned var with
227 vector<pair<CVariable*, int> > _ordered_vars; // pair's first pointing to
228 // the var, second is the score.
230 // these are for conflict analysis
231 int _num_marked; // used when constructing learned clause
232 int _num_in_new_cl; // used when constructing learned clause
233 vector<ClauseIdx> _conflicts; // the conflicting clauses
234 vector<int> _conflict_lits; // used when constructing learned clause
235 vector<int> _resolvents;
236 multimap<int, int> _shrinking_cls;
239 void re_init_stats(void);
240 void init_stats(void);
241 void init_parameters(void);
242 void init_solve(void);
243 void real_solve(void);
245 int preprocess(void);
247 void run_periodic_functions(void);
249 // for decision making
250 bool decide_next_branch(void);
251 void decay_variable_score(void) ;
252 void adjust_variable_order(int * lits, int n_lits);
253 void update_var_score(void);
255 // for conflict analysis
256 ClauseIdx add_conflict_clause(int * lits, int n_lits, int gflag);
257 int analyze_conflicts(void);
258 ClauseIdx finish_add_conf_clause(int gflag);
259 int conflict_analysis_firstUIP(void);
260 void mark_vars(ClauseIdx cl, int var_idx);
261 void back_track(int level);
264 void set_var_value(int var, int value, ClauseIdx ante, int dl);
265 void set_var_value_BCP(int v, int value);
266 void unset_var_value(int var);
270 void delete_unrelevant_clauses(void);
271 ClauseIdx add_clause_with_gid(int * lits, int n_lits, int gid = 0);
274 // constructors and destructors
278 // member access function
279 void set_time_limit(float t);
280 void set_mem_limit(int s);
281 void enable_cls_deletion(bool allow);
282 void set_randomness(int n) ;
283 void set_random_seed(int seed);
285 void set_variable_number(int n);
286 int add_variable(void) ;
287 void mark_var_branchable(int vid);
288 void mark_var_unbranchable(int vid);
290 inline int & dlevel(void) {
294 inline int outcome(void) {
295 return _stats.outcome;
298 inline int num_decisions(void) {
299 return _stats.num_decisions;
302 inline int num_decisions_stack_conf(void) {
303 return _stats.num_decisions_stack_conf;
306 inline int num_decisions_vsids(void) {
307 return _stats.num_decisions_vsids;
310 inline int num_decisions_shrinking(void) {
311 return _stats.num_decisions_shrinking;
314 inline int num_shrinkings(void) {
315 return _stats.num_shrinkings;
318 inline int & num_free_variables(void) {
319 return _stats.num_free_variables;
322 inline int max_dlevel(void) {
323 return _stats.max_dlevel;
326 inline int random_seed(void) {
327 return _stats.random_seed;
330 inline long64 num_implications(void) {
331 return _stats.num_implications;
334 inline long64 total_bubble_move(void) {
335 return _stats.total_bubble_move;
338 inline char * version(void) {
339 return __ZCHAFF_VERSION__;
342 float elapsed_cpu_time(void);
343 float cpu_run_time(void) ;
344 int estimate_mem_usage(void) {
345 return CDatabase::estimate_mem_usage();
350 void queue_implication(int lit, ClauseIdx ante_clause) {
353 i.antecedent = ante_clause;
354 _implication_queue.push(i);
357 // top level function
358 inline int id(void) {
362 inline void set_id(int i) {
366 inline void force_terminate(void) {
367 _force_terminate = true;
370 inline void unset_force_terminate(void) {
371 _force_terminate = false;
374 // for incremental SAT
375 int add_clause_incr(int * lits, int n_lits, int gid = 0);
377 void make_decision(int lit) {
379 queue_implication(lit, NULL_CLAUSE);
382 void add_hook(HookFunPtrT fun, int interval);
384 inline void add_outside_constraint_hook(OutsideConstraintHookPtrT fun) {
385 _outside_constraint_hook = fun;
388 inline void add_sat_hook(SatHookPtrT fun) {
392 void verify_integrity(void);
393 void delete_clause_group(int gid);
396 ClauseIdx add_orig_clause(int * lits, int n_lits, int gid = 0);
397 void clean_up_dbase(void);
398 void dump_assignment_stack(ostream & os = cout);
399 void dump_implication_queue(ostream & os = cout);
401 void print_cls(ostream & os = cout);
402 void dump(ostream & os = cout ) {
404 dump_assignment_stack(os);
406 void add_outside_clauses(void);