From 09d3e1ff77e656976268fa27b6045ff6f284fd3b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 4 Dec 2011 16:10:11 -0800 Subject: Proof-logging in the updated solver. --- src/sat/bsat/satSolver2.h | 31 +++++++++++++++++++++---------- 1 file changed, 21 insertions(+), 10 deletions(-) (limited to 'src/sat/bsat/satSolver2.h') diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index a5ed85b3..937972a6 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -32,7 +32,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA ABC_NAMESPACE_HEADER_START - +//#define USE_FLOAT_ACTIVITY //================================================================================================= // Public interface: @@ -70,9 +70,6 @@ extern void * sat_solver2_store_release( sat_solver2 * s ); //================================================================================================= // Solver representation: -//struct clause_t; -//typedef struct clause_t clause; - struct varinfo_t; typedef struct varinfo_t varinfo; @@ -91,21 +88,26 @@ struct sat_solver2_t int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything int fNotUseRandom; // do not allow random decisions with a fixed probability // int fSkipSimplify; // set to one to skip simplification of the clause database + int fProofLogging; // enable proof-logging // clauses + veci clauses; // clause memory + veci* wlists; // watcher lists (for each literal) int iLearnt; // the first learnt clause int iLast; // the last learnt clause - veci* wlists; // watcher lists (for each literal) - - // clause memory - int * pMemArray; - int nMemAlloc; - int nMemSize; // activities +#ifdef USE_FLOAT_ACTIVITY + double var_inc; // Amount to bump next variable with. + double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. + float cla_inc; // Amount to bump next clause with. + float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. + double* activity; // A heuristic measurement of the activity of a variable. +#else int var_inc; // Amount to bump next variable with. int cla_inc; // Amount to bump next clause with. unsigned* activity; // A heuristic measurement of the activity of a variable. +#endif veci claActs; // clause activities veci claProofs; // clause proofs @@ -123,6 +125,15 @@ struct sat_solver2_t veci model; // If problem is solved, this vector contains the model (contains: lbool). veci conf_final; // If problem is unsatisfiable (possibly under assumptions), // this vector represent the final conflict clause expressed in the assumptions. + veci mark_levels; // temporary storage for labeled levels + veci min_lit_order; // ordering of removable literals + veci min_step_order;// ordering of resolution steps + + // proof logging + veci proof_clas; // sequence of proof clauses + veci proof_vars; // sequence of proof variables + int iStartChain; // beginning of the chain + // statistics stats_t stats; ABC_INT64_T nConfLimit; // external limit on the number of conflicts -- cgit v1.2.3