luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Improvement to the SAT solver (skipping binary clauses).

This commit is contained in:
Alan Mishchenko 2011-11-25 18:06:36 -08:00
parent 7a0a4d4d79
commit 9726d5a85e
3 changed files with 57 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/sat/bsat/satSolver.c
View File

@ -306,6 +306,15 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
assert(end - begin > 1);
assert(learnt >= 0 && learnt < 2);
size = end - begin;
// do not allocate memory for the two-literal problem clause
if ( size == 2 && !learnt )
{
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(clause_from_lit(begin[1])));
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(clause_from_lit(begin[0])));
return NULL;
}
// c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
@ -336,6 +345,8 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
// if ( learnt )
// printf( "%d ", size );
return c;
}
@ -1212,6 +1223,7 @@ void sat_solver_delete(sat_solver* s)
int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
{
clause * c;
lit *i,*j;
int maxvar;
lbool* values;
@ -1271,7 +1283,9 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
return enqueue(s,*begin,(clause*)0);
// create new clause
vecp_push(&s->clauses,clause_new(s,begin,j,0));
c = clause_new(s,begin,j,0);
if ( c )
vecp_push(&s->clauses,c);
s->stats.clauses++;

8
src/sat/bsat/satSolver.h
View File

@ -36,7 +36,7 @@ ABC_NAMESPACE_HEADER_START
//=================================================================================================
// Simple types:
/*
#ifndef __cplusplus
#ifndef false
# define false 0
@ -64,7 +64,7 @@ static inline int lit_sign (lit l) { return l & 1; }
static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; }
*/
//=================================================================================================
// Public interface:
@ -84,14 +84,14 @@ extern int sat_solver_nclauses(sat_solver* s);
extern int sat_solver_nconflicts(sat_solver* s);
extern void sat_solver_setnvars(sat_solver* s,int n);
/*
struct stats_t
{
ABC_INT64_T starts, decisions, propagations, inspects, conflicts;
ABC_INT64_T clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
};
typedef struct stats_t stats_t;
*/
extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p );
extern int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars );

38
src/sat/bsat/satVec.h
View File

@ -86,6 +86,44 @@ static inline void vecp_push (vecp* v, void* e)
//=================================================================================================
// Simple types:
#ifndef __cplusplus
#ifndef false
# define false 0
#endif
#ifndef true
# define true 1
#endif
#endif
typedef int lit;
typedef char lbool;
static const int var_Undef = -1;
static const lit lit_Undef = -2;
static const lbool l_Undef = 0;
static const lbool l_True = 1;
static const lbool l_False = -1;
static inline lit toLit (int v) { return v + v; }
static inline lit toLitCond(int v, int c) { return v + v + (c != 0); }
static inline lit lit_neg (lit l) { return l ^ 1; }
static inline int lit_var (lit l) { return l >> 1; }
static inline int lit_sign (lit l) { return l & 1; }
static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; }
struct stats_t
{
ABC_INT64_T starts, decisions, propagations, inspects, conflicts;
ABC_INT64_T clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
};
typedef struct stats_t stats_t;
ABC_NAMESPACE_HEADER_END