82 lines
2.7 KiB
C
82 lines
2.7 KiB
C
/* note that internally, literals use a representation different from the API.
|
||
* variables are numbered from 0 (not 1) and 2v and 2v+1 correspond to v
|
||
* and ¬v, resp. */
|
||
#define VAR(l) ((l)>>1)
|
||
#define NOT(l) ((l)^1)
|
||
|
||
/* l[0] and l[1] are special: they are the watched literals.
|
||
* all clauses that have literal l on their watchlist form a linked list starting with s->lit[l].watch
|
||
* and watch[i] having the next clause for l[i] */
|
||
struct SATClause {
|
||
SATClause *next;
|
||
SATClause *watch[2];
|
||
double activity; /* activity is increased every time a clause is used to resolve a conflict (tiebreaking heuristic during purging) */
|
||
int n; /* >= 2 for learned clauses and > 2 for input clauses (binary input clauses are kept in the bimp tables) */
|
||
ushort range; /* heuristic used during purging, low range => keep clause (range 0..256) */
|
||
int l[1];
|
||
};
|
||
|
||
struct SATLit {
|
||
int *bimp; /* array of literals implied by this literal through binary clauses (Binary IMPlications) */
|
||
SATClause *watch; /* linked list of watched clauses */
|
||
int nbimp;
|
||
char val; /* -1 = not assigned, 0 = false, 1 = true */
|
||
};
|
||
|
||
struct SATVar {
|
||
double activity; /* activity is increased every time a variable shows up in a conflict */
|
||
union {
|
||
SATClause *reason; /* nil for decision and free literals */
|
||
int binreason; /* used when isbinreason == 1: the reason is the clause l ∨ l->binreason */
|
||
};
|
||
int lvl; /* level at which this variable is defined, or -1 for free variables */
|
||
int heaploc; /* location in binary heap or -1 when not in heap */
|
||
uint stamp; /* "stamp" value used for conflict resolution etc. */
|
||
uchar flags; /* see below */
|
||
char isbinreason;
|
||
};
|
||
|
||
enum {
|
||
VARPHASE = 1, /* for a free variables, VARPHASE is used as a first guess the next time it is picked */
|
||
VARUSER = 0x80, /* user assigned variable (unit clause in input) */
|
||
};
|
||
|
||
/* records conflicts during purging */
|
||
struct SATConflict {
|
||
union {
|
||
SATClause *c;
|
||
uvlong b;
|
||
};
|
||
int lvl; /* bit 31 denotes binary conflict */
|
||
};
|
||
#define CFLLVL(c) ((c).lvl & 0x7fffffff)
|
||
|
||
enum {
|
||
SATBLOCKSZ = 65536,
|
||
SATVARALLOC = 64,
|
||
CLAUSEALIGN = 8,
|
||
CFLCLALLOC = 16,
|
||
};
|
||
|
||
void saterror(SATSolve *, char *, ...);
|
||
void sataddtrail(SATSolve *, int);
|
||
void satdebuginit(SATSolve *);
|
||
void satprintstate(SATSolve *);
|
||
void satsanity(SATSolve *);
|
||
SATVar *satheaptake(SATSolve *);
|
||
void satheapput(SATSolve *, SATVar *);
|
||
void satreheap(SATSolve *, SATVar *);
|
||
void satheapreset(SATSolve *);
|
||
int satnrand(SATSolve *, int);
|
||
void *satrealloc(SATSolve *, void *, ulong);
|
||
SATClause *satnewclause(SATSolve *, int, int);
|
||
SATClause *satreplclause(SATSolve *, int);
|
||
void satcleanup(SATSolve *, int);
|
||
void satbackjump(SATSolve *, int);
|
||
|
||
#define signf(l) (((l)<<31>>31|1)*((l)+2>>1))
|
||
#pragma varargck type "Γ" SATClause*
|
||
|
||
#define ε 2.2250738585072014e-308
|
||
#define MAXACTIVITY 1e100
|