266 lines
6.6 KiB
C
266 lines
6.6 KiB
C
|
|
/* 2012 (C) Jussi Rintanen, jrintanen.jr@gmail.com */
|
|
|
|
#if defined(__LP64__)
|
|
#define PTRINT long
|
|
#else
|
|
#define PTRINT int
|
|
#endif
|
|
|
|
typedef struct _thread {
|
|
int cround; /* Counter which is incremented for new conflict clauses */
|
|
int maxwasseen;
|
|
int *wasseen; /* Counter when literal was last encountered */
|
|
#define MAXCCLENGTH 10000000
|
|
int cc[MAXCCLENGTH]; /* Conflict clause which is being constructed */
|
|
#ifndef FUIP
|
|
int stck[MAXCCLENGTH]; /* The stack used during computing the conflict clause */
|
|
#endif
|
|
|
|
} thread;
|
|
|
|
thread *threads;
|
|
|
|
#define SVAR(v) (v)
|
|
#define ACTVAR(a) ((a)+(sati->nOfSVars))
|
|
#define TVAR(v,t) ((v)+(t)*(sati->nOfVarsPerTime))
|
|
#define TLIT(l,t) ((l)+2*(t)*(sati->nOfVarsPerTime))
|
|
#define TACT(a,t) ((ACTVAR(a))+(t)*(sati->nOfVarsPerTime))
|
|
|
|
typedef struct _nintlist { int hd; struct _nintlist *tl; } nintlist;
|
|
|
|
|
|
/*********************** VARIABLES *******************/
|
|
|
|
#define STATUSTYPE char
|
|
|
|
/************* LITERALS & WATCH LISTS *****************/
|
|
|
|
/* The watch list has the watch list EMBEDDED in the clause data structure
|
|
(Biere et al. ???)
|
|
*/
|
|
|
|
#define LITWATCHES(l) (sati->lits[(l)].watches)
|
|
|
|
typedef struct _literal {
|
|
int *watches;
|
|
#ifdef WEIGHTS
|
|
short score; /* Scores for choosing decision variables */
|
|
#endif
|
|
} literal;
|
|
|
|
/********************** HEAP *********************/
|
|
|
|
/* Heap for keeping track of the highest score variables.
|
|
Each element in the heap has two components:
|
|
k: key, i.e. the index of the variable
|
|
v: value, i.e. the current VSIDS score/weight
|
|
*/
|
|
|
|
typedef struct {
|
|
int k;
|
|
short v;
|
|
} pair;
|
|
|
|
typedef struct _heap {
|
|
int els;
|
|
int maxels;
|
|
pair *array;
|
|
} *heap;
|
|
|
|
|
|
/******************* SAT INSTANCE *******************/
|
|
|
|
#define REASONDLEVEL
|
|
|
|
#ifdef REASONDLEVEL
|
|
typedef struct {
|
|
PTRINT reason;
|
|
int dlevel;
|
|
} RD;
|
|
#endif
|
|
|
|
typedef struct _satinstance {
|
|
short id; /* Unique integer id for the instance */
|
|
int thread; /* The thread this is run in. */
|
|
|
|
short value; /* The truth-value of the instance, -1 = unknown */
|
|
int nOfVars; /* Number of propositional variables */
|
|
int nOfVarsPerTime; /* Number of vars per time point */
|
|
short nOfTPoints; /* Number of time points */
|
|
|
|
nintlist **l2its; /* Array for 2-literal clauses (for all time points), non-changing */
|
|
int **al2its; /* Array for 2-literal clauses (for all time points), non-changing */
|
|
|
|
literal *lits; /* Data structure for literals */
|
|
|
|
int *declevels;
|
|
#ifdef COSTS
|
|
int declevelscost;
|
|
#endif
|
|
|
|
#if defined REPRTWO || defined REPRFOUR
|
|
#define VALTYPE int
|
|
#else
|
|
#define VALTYPE char
|
|
#endif
|
|
|
|
VALTYPE *variableval;
|
|
|
|
int dlevel; /* Current decision level of the SAT instance. */
|
|
|
|
int decisions; /* How many decision made */
|
|
int conflicts; /* How many conflicts */
|
|
int decaysteps; /* Counter for variable weight decays */
|
|
|
|
int conflicttype2lit;
|
|
int *conflictclause; /* Clause that was falsified */
|
|
int conflictl1; /* Following four set when empty clause derived. */
|
|
int conflictl2;
|
|
|
|
#ifndef MULTICORE
|
|
int cc[MAXCCLENGTH]; /* Conflict clause which is being constructed */
|
|
#ifndef FUIP
|
|
int stck[MAXCCLENGTH]; /* The stack used during computing the conflict clause */
|
|
#endif
|
|
#endif
|
|
|
|
#ifdef VSIDS
|
|
STATUSTYPE *variablestatus;
|
|
/* These are the status bits.
|
|
bit 0 is phase there?
|
|
bit 1 phase
|
|
bit 2 dirty? (whether inferred with the goal clauses)
|
|
*/
|
|
#define VARSTATUS(v) (sati->variablestatus[(v)])
|
|
#endif
|
|
|
|
#ifndef REASONDLEVEL
|
|
|
|
PTRINT *variablereason;
|
|
int *variabledlevel;
|
|
#define LITREASON(l) (sati->variablereason[VAR(l)])
|
|
#define LITDLEVEL(l) (sati->variabledlevel[VAR(l)])
|
|
|
|
#else
|
|
|
|
RD *variablerd;
|
|
|
|
#define LITREASON(l) (sati->variablerd[VAR(l)].reason)
|
|
#define LITDLEVEL(l) (sati->variablerd[VAR(l)].dlevel)
|
|
|
|
#endif
|
|
|
|
|
|
#ifdef VSIDS
|
|
int *hindex; /* Index of each variable in the heap. */
|
|
heap scoreheap; /* Literals ordered according to their score */
|
|
#endif
|
|
|
|
int *initialunittable; /* Table for the unit clauses in the input */
|
|
int maxinitialunits; /* The size of the table */
|
|
int initialunits; /* Number of unit clauses in the table */
|
|
|
|
int *unitstack; /* Stack of assignments made */
|
|
int endunitstack,startunitstack; /* Unprocessed part of the stack */
|
|
|
|
int nOfSVars; /* Planning: number of state variables (per time) */
|
|
int nOfActions; /* Planning number of actions (per time) */
|
|
|
|
int complete; /* true if all input clauses have been added */
|
|
int notcalledbefore; /* true if solve0 not called yet. */
|
|
|
|
/* Fields for the heuristics */
|
|
int pheuristic; /* Which planning-based heuristic to use. */
|
|
int heuristic; /* Which branching heuristic to use. */
|
|
/* Unit clauses that have been learned */
|
|
#define MAXUCC 10000
|
|
int NofUCClauses;
|
|
int UCC[MAXUCC];
|
|
|
|
/* Variables for the planning heuristic */
|
|
int heuristic_mode; /* This is 0 for actions, 1 for inertia, 2 for noops. */
|
|
int heuristic_time; /* The next two are for inertia and noops. */
|
|
int heuristic_index;
|
|
#ifdef COSTS
|
|
int costbound; /* Cost bound */
|
|
int currentcost; /* Cost of current (partial) assignment */
|
|
int *costs; /* Costs all (untimed) state variables */
|
|
#endif
|
|
|
|
|
|
#ifdef GOALWEIGHTS
|
|
int *supportsg; /* Which subgoal action supports. */
|
|
int *supportsa; /* Which action (previous decision) action supports. */
|
|
#endif
|
|
|
|
#ifdef LBD
|
|
int LBDcounter;
|
|
int *LBDflag;
|
|
#endif
|
|
|
|
} *satinstance;
|
|
|
|
typedef enum { InitC, FinalC, TransC } clausetype;
|
|
|
|
float estimateinstancesize(int,int,int);
|
|
|
|
satinstance newinstance(int,int,int,int,int);
|
|
void freeinstance(satinstance);
|
|
|
|
void addnewclause(satinstance,int,clausetype); /* Number of literals in the clause (> 2) */
|
|
void addliteral(satinstance,int,int); /* Put literal to the given loc in the clause */
|
|
void finishclause(satinstance); /* Finish adding the clause */
|
|
|
|
int add1clause(satinstance,int,clausetype); /* Add a 1-literal clause */
|
|
void add2clause(satinstance,int,int,clausetype); /* Add a 2-literal clause */
|
|
|
|
void instancecomplete();
|
|
|
|
void planningparameters(satinstance,int,int);
|
|
void setheuristic(satinstance,int);
|
|
void setpheuristic(satinstance,int);
|
|
|
|
int solve(satinstance);
|
|
int solve0(satinstance,int,int);
|
|
|
|
int noT2clauses;
|
|
|
|
void addtimedvarcost(satinstance,int,int);
|
|
|
|
int varvalue(satinstance,int);
|
|
int vartruep(satinstance,int);
|
|
int tvarvalue(satinstance,int,int);
|
|
int tvarvar(satinstance,int);
|
|
int tvartime(satinstance,int);
|
|
|
|
int VALUE(int);
|
|
int NEG(int);
|
|
int VAR(int);
|
|
int PLIT(int);
|
|
int NLIT(int);
|
|
int LIT(int);
|
|
|
|
#define UNASS -1
|
|
|
|
int propagate(satinstance);
|
|
|
|
void init_clausesets(int);
|
|
|
|
double allocatedbyCL;
|
|
float memoryused();
|
|
|
|
int flagShortCutHorizon;
|
|
|
|
void shortcuts(satinstance sati);
|
|
|
|
typedef struct _shortcutclause {
|
|
int l1,l2,tdiff;
|
|
} shortcutclause;
|
|
|
|
shortcutclause *shortcutclauses;
|
|
int nofshortcutclauses;
|
|
int maxshortcutclauses;
|
|
|
|
void nextround(satinstance sati);
|