/**************************************************************************************************
MiniSat -- Copyright (c) 2005, Niklas Sorensson
http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
#include <stdio.h>
#include <assert.h>
#include <math.h>
#include <time.h>
#include "solver.h"
#define ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
//=================================================================================================
// Simple (var/literal) helpers:
static inline int lit_var(lit l) { return l >> 1; }
static inline int lit_sign(lit l) { return (l & 1); }
//=================================================================================================
// Debug:
//#define VERBOSEDEBUG
// For derivation output (verbosity level 2)
#define L_IND "%-*d"
#define L_ind solver_dlevel(s)*3+3,solver_dlevel(s)
#define L_LIT "%sx%d"
#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
// Just like 'assert()' but expression will be evaluated in the release version as well.
static inline void check(int expr) { assert(expr); }
static void printlits(lit* begin, lit* end)
{
int i;
for (i = 0; i < end - begin; i++)
printf(L_LIT" ",L_lit(begin[i]));
}
//=================================================================================================
// Random numbers:
// Returns a random float 0 <= x < 1. Seed must never be 0.
static inline double drand(double* seed) {
int q;
*seed *= 1389796;
q = (int)(*seed / 2147483647);
*seed -= (double)q * 2147483647;
return *seed / 2147483647; }
// Returns a random integer 0 <= x < size. Seed must never be 0.
static inline int irand(double* seed, int size) {
return (int)(drand(seed) * size); }
//=================================================================================================
// Predeclarations:
void sort(void** array, int size, int(*comp)(const void *, const void *));
//=================================================================================================
// Clause datatype + minor functions:
struct clause_t
{
int size_learnt;
lit lits[0];
};
static inline int clause_size (clause* c) { return c->size_learnt >> 1; }
static inline lit* clause_begin (clause* c) { return c->lits; }
static inline int clause_learnt (clause* c) { return c->size_learnt & 1; }
static inline float clause_activity (clause* c) { return *((float*)&c->lits[c->size_learnt>>1]); }
static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[c->size_learnt>>1]) = a; }
//=================================================================================================
// Encode literals in clause pointers:
clause* clause_from_lit (lit l) { return (clause*)(((unsigned long)l) + ((unsigned long)l) + 1); }
bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); }
lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); }
//=================================================================================================
// Simple helpers:
static inline int solver_dlevel(solver* s) { return veci_size(&s->trail_lim); }
static inline vec* solver_read_wlist (solver* s, lit l){ return &s->wlists[l]; }
static inline void vec_remove(vec* v, void* e)
{
void** ws = vec_begin(v);
int j = 0;
for (; ws[j] != e ; j++);
assert(j < vec_size(v));
for (; j < vec_size(v)-1; j++) ws[j] = ws[j+1];
vec_resize(v,vec_size(v)-1);
}
//=================================================================================================
// Variable order functions:
static inline void order_update(solver* s, int v) // updateorder
{
// int clk = clock();
int* orderpos = s->orderpos;
double* activity = s->activity;
int* heap = veci_begin(&s->order);
int i = orderpos[v];
int x = heap[i];
int parent = (i - 1) / 2;
assert(s->orderpos[v] != -1);
while (i != 0 && activity[x] > activity[heap[parent]]){
heap[i] = heap[parent];
orderpos[heap[i]] = i;
i = parent;
parent = (i - 1) / 2;
}
heap[i] = x;
orderpos[x] = i;
// s->timeUpdate += clock() - clk;
}
static inline void order_assigned(solver* s, int v)
{
}
static inline void order_unassigned(solver* s, int v) // undoorder
{
// int clk = clock();
int* orderpos = s->orderpos;
if (orderpos[v] == -1){
orderpos[v] = veci_size(&s->order);
veci_push(&s->order,v);
order_update(s,v);
}
// s->timeUpdate += clock() - clk;
}
static int order_select(solver* s, float random_var_freq) // selectvar
{
// int clk = clock();
static int Counter = 0;
int* heap;
double* activity;
int* orderpos;
lbool* values = s->assigns;
// The first decisions
if ( s->pPrefVars && s->nPrefDecNum < s->nPrefVars )
{
int i;
s->nPrefDecNum++;
for ( i = 0; i < s->nPrefVars; i++ )
if ( values[s->pPrefVars[i]] == l_Undef )
return s->pPrefVars[i];
}
// Random decision:
if (drand(&s->random_seed) < random_var_freq){
int next = irand(&s->random_seed,s->size);
assert(next >= 0 && next < s->size);
if (values[next] == l_Undef)
return next;
}
// Activity based decision:
heap = veci_begin(&s->order);
activity = s->activity;
orderpos = s->orderpos;
while (veci_size(&s->order) > 0){
int next = heap[0];
int size = veci_size(&s->order)-1;
int x = heap[size];
veci_resize(&s->order,size);
orderpos[next] = -1;
if (size > 0){
double act = activity[x];
int i = 0;
int child = 1;
while (child < size){
if (child+1 < size && activity[heap[child]] < activity[heap[child+1]])
child++;
assert(child < size);
if (act >= activity[heap[child]])
break;
heap[i] = heap[child];
orderpos[heap[i]] = i;
i = child;
child = 2 * child + 1;
}
heap[i] = x;
orderpos[heap[i]] = i;
}
if (values[next] == l_Undef)
return next;
}
// s->timeSelect += clock() - clk;
return var_Undef;
}
// J-frontier
extern void Asat_JManAssign( Asat_JMan_t * p, int Var );
extern void Asat_JManUnassign( Asat_JMan_t * p, int Var );
extern int Asat_JManSelect( Asat_JMan_t * p );
//=================================================================================================
// Activity functions:
static inline void act_var_rescale(solver* s) {
double* activity = s->activity;
int i;
for (i = 0; i < s->size; i++)
activity[i] *= 1e-100;
s->var_inc *= 1e-100;
}
static inline void act_var_bump(solver* s, int v) {
double* activity = s->activity;
if ((activity[v] += s->var_inc) > 1e100)
// if ((activity[v] += s->var_inc*s->factors[v]/100000000) > 1e100)
act_var_rescale(s);
//printf("bump %d %f\n", v-1, activity[v]);
if ( s->pJMan == NULL && s->orderpos[v] != -1 )
order_update(s,v);
}
static inline void act_var_decay(solver* s) { s->var_inc *= s->var_decay; }
static inline void act_clause_rescale(solver* s) {
clause** cs = (clause**)vec_begin(&s->learnts);
int i;
for (i = 0; i < vec_size(&s->learnts); i++){
float a = clause_activity(cs[i]);
clause_setactivity(cs[i], a * (float)1e-20);
}
s->cla_inc *= (float)1e-20;
}
static inline void act_clause_bump(solver* s, clause *c) {
float a = clause_activity(c) + s->cla_inc;
clause_setactivity(c,a);
if (a > 1e20) act_clause_rescale(s);
}
static inline void act_clause_decay(solver* s) { s->cla_inc *= s->cla_decay; }
//=================================================================================================
// Clause functions:
/* pre: size > 1 && no variable occurs twice
*/
static clause* clause_new(solver* s, lit* begin, lit* end, int learnt)
{
int size;
clause* c;
int i;
assert(end - begin > 1);
assert(learnt >= 0 && learnt < 2);
size = end - begin;
// c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
#else
c = (clause*)Asat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
#endif
c->size_learnt = (size << 1) | learnt;
assert(((unsigned int)c & 1) == 0);
for (i = 0; i < size; i++)
{
assert(begin[i] >= 0);
c->lits[i] = begin[i];
}
if (learnt)
*((float*)&c->lits[size]) = 0.0;
assert(begin[0] >= 0);
assert(begin[0] < s->size*2);
assert(begin[1] >= 0);
assert(begin[1] < s->size*2);
assert(neg(begin[0]) < s->size*2);
assert(neg(begin[1]) < s->size*2);
//vec_push(solver_read_wlist(s,neg(begin[0])),(void*)c);
//vec_push(solver_read_wlist(s,neg(begin[1])),(void*)c);
vec_push(solver_read_wlist(s,neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
vec_push(solver_read_wlist(s,neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
return c;
}
static void clause_remove(solver* s, clause* c)
{
lit* lits = clause_begin(c);
assert(neg(lits[0]) < s->size*2);
assert(neg(lits[1]) < s->size*2);
assert(lits[0] < s->size*2);
//vec_remove(solver_read_wlist(s,neg(lits[0])),(void*)c);
//vec_remove(solver_read_wlist(s,neg(lits[1])),(void*)c);
vec_remove(solver_read_wlist(s,neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
vec_remove(solver_read_wlist(s,neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
if (clause_learnt(c)){
s->solver_stats.learnts--;
s->solver_stats.learnts_literals -= clause_size(c);
}else{
s->solver_stats.clauses--;
s->solver_stats.clauses_literals -= clause_size(c);
}
#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
free(c);
#else
Asat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
#endif
}
static lbool clause_simplify(solver* s, clause* c)
{
lit* lits = clause_begin(c);
lbool* values = s->assigns;
int i;
assert(solver_dlevel(s) == 0);
for (i = 0; i < clause_size(c); i++){
lbool sig = !lit_sign(lits[i]); sig += sig - 1;
if (values[lit_var(lits[i])] == sig)
return l_True;
}
return l_False;
}
//=================================================================================================
// Minor (solver) functions:
static void solver_setnvars(solver* s,int n)
{
int var;
if (s->cap < n){
while (s->cap < n) s->cap = s->cap*2+1;
s->wlists = (vec*) realloc(s->wlists, sizeof(vec)*s->cap*2);
s->activity = (double*) realloc(s->activity, sizeof(double)*s->cap);
s->assigns = (lbool*) realloc(s->assigns, sizeof(lbool)*s->cap);
s->orderpos = (int*) realloc(s->orderpos, sizeof(int)*s->cap);
s->reasons = (clause**)realloc(s->reasons, sizeof(clause*)*s->cap);
s->levels = (int*) realloc(s->levels, sizeof(int)*s->cap);
s->tags = (lbool*) realloc(s->tags, sizeof(lbool)*s->cap);
s->trail = (lit*) realloc(s->trail, sizeof(lit)*s->cap);
}
for (var = s->size; var < n; var++){
vec_new(&s->wlists[2*var]);
vec_new(&s->wlists[2*var+1]);
s->activity [var] = 0;
s->assigns [var] = l_Undef;
s->orderpos [var] = var;
s->reasons [var] = (clause*)0;
s->levels [var] = 0;
s->tags [var] = l_Undef;
assert(veci_size(&s->order) == var);
veci_push(&s->order,var);
order_update(s,var);
}
s->size = n > s->size ? n : s->size;
}
static inline bool enqueue(solver* s, lit l, clause* from)
{
lbool* values = s->assigns;
int v = lit_var(l);
lbool val = values[v];
lbool sig = !lit_sign(l); sig += sig - 1;
#ifdef VERBOSEDEBUG
printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
#endif
if (val != l_Undef){
return val == sig;
}else{
// New fact -- store it.
int* levels = s->levels;
clause** reasons = s->reasons;
#ifdef VERBOSEDEBUG
printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
#endif
values [v] = sig;
levels [v] = solver_dlevel(s);
reasons[v] = from;
s->trail[s->qtail++] = l;
if ( s->pJMan )
Asat_JManAssign( s->pJMan, v );
else
order_assigned(s, v);
return 1;
}
}
static inline void assume(solver* s, lit l){
assert(s->qtail == s->qhead);
assert(s->assigns[lit_var(l)] == l_Undef);
#ifdef VERBOSEDEBUG
printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l));
#endif
veci_push(&s->trail_lim,s->qtail);
enqueue(s,l,(clause*)0);
}
static inline void solver_canceluntil(solver* s, int level) {
lit* trail;
lbool* values;
clause** reasons;
int bound;
int c;
if (solver_dlevel(s) <= level)
return;
trail = s->trail;
values = s->assigns;
reasons = s->reasons;
bound = veci_begin(&s->trail_lim)[level];
for (c = s->qtail-1; c >= bound; c--) {
int x = lit_var(trail[c]);
values [x] = l_Undef;
reasons[x] = (clause*)0;
}
if ( s->pJMan )
for (c = s->qtail-1; c >= bound; c--)
Asat_JManUnassign( s->pJMan, lit_var(trail[c]) );
else
for (c = s->qhead-1; c >= bound; c--)
order_unassigned( s, lit_var(trail[c]) );
s->qhead = s->qtail = bound;
veci_resize(&s->trail_lim,level);
}
static void solver_record(solver* s, veci* cls)
{
lit* begin = veci_begin(cls);
lit* end = begin + veci_size(cls);
clause* c = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0;
enqueue(s,*begin,c);
assert(veci_size(cls) > 0);
if (c != 0) {
vec_push(&s->learnts,(void*)c);
act_clause_bump(s,c);
s->solver_stats.learnts++;
s->solver_stats.learnts_literals += veci_size(cls);
}
}
static double solver_progress(solver* s)
{
lbool* values = s->assigns;
int* levels = s->levels;
int i;
double progress = 0;
double F = 1.0 / s->size;
for (i = 0; i < s->size; i++)
if (values[i] != l_Undef)
progress += pow(F, levels[i]);
return progress / s->size;
}
//=================================================================================================
// Major methods:
static bool solver_lit_removable(solver* s, lit l, int minl)
{
lbool* tags = s->tags;
clause** reasons = s->reasons;
int* levels = s->levels;
int top = veci_size(&s->tagged);
assert(lit_var(l) >= 0 && lit_var(l) < s->size);
assert(reasons[lit_var(l)] != 0);
veci_resize(&s->stack,0);
veci_push(&s->stack,lit_var(l));
while (veci_size(&s->stack) > 0){
clause* c;
int v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
assert(v >= 0 && v < s->size);
veci_resize(&s->stack,veci_size(&s->stack)-1);
assert(reasons[v] != 0);
c = reasons[v];
if (clause_is_lit(c)){
int v = lit_var(clause_read_lit(c));
if (tags[v] == l_Undef && levels[v] != 0){
if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
veci_push(&s->stack,v);
tags[v] = l_True;
veci_push(&s->tagged,v);
}else{
int* tagged = veci_begin(&s->tagged);
int j;
for (j = top; j < veci_size(&s->tagged); j++)
tags[tagged[j]] = l_Undef;
veci_resize(&s->tagged,top);
return 0;
}
}
}else{
lit* lits = clause_begin(c);
int i, j;
for (i = 1; i < clause_size(c); i++){
int v = lit_var(lits[i]);
if (tags[v] == l_Undef && levels[v] != 0){
if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
veci_push(&s->stack,lit_var(lits[i]));
tags[v] = l_True;
veci_push(&s->tagged,v);
}else{
int* tagged = veci_begin(&s->tagged);
for (j = top; j < veci_size(&s->tagged); j++)
tags[tagged[j]] = l_Undef;
veci_resize(&s->tagged,top);
return 0;
}
}
}
}
}
return 1;
}
static void solver_analyze(solver* s, clause* c, veci* learnt)
{
lit* trail = s->trail;
lbool* tags = s->tags;
clause** reasons = s->reasons;
int* levels = s->levels;
int cnt = 0;
lit p = lit_Undef;
int ind = s->qtail-1;
lit* lits;
int i, j, minl;
int* tagged;
veci_push(learnt,lit_Undef);
do{
assert(c != 0);
if (clause_is_lit(c)){
lit q = clause_read_lit(c);
assert(lit_var(q) >= 0 && lit_var(q) < s->size);
if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
tags[lit_var(q)] = l_True;
veci_push(&s->tagged,lit_var(q));
act_var_bump(s,lit_var(q));
if (levels[lit_var(q)] == solver_dlevel(s))
cnt++;
else
veci_push(learnt,q);
}
}else{
if (clause_learnt(c))
act_clause_bump(s,c);
lits = clause_begin(c);
//printlits(lits,lits+clause_size(c)); printf("\n");
for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
lit q = lits[j];
assert(lit_var(q) >= 0 && lit_var(q) < s->size);
if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
tags[lit_var(q)] = l_True;
veci_push(&s->tagged,lit_var(q));
act_var_bump(s,lit_var(q));
if (levels[lit_var(q)] == solver_dlevel(s))
cnt++;
else
veci_push(learnt,q);
}
}
}
while (tags[lit_var(trail[ind--])] == l_Undef);
p = trail[ind+1];
c = reasons[lit_var(p)];
cnt--;
}while (cnt > 0);
// *veci_begin(learnt) = neg(p);
lits = veci_begin(learnt);
lits[0] = neg(p);
minl = 0;
for (i = 1; i < veci_size(learnt); i++){
int lev = levels[lit_var(lits[i])];
minl |= 1 << (lev & 31);
}
// simplify (full)
for (i = j = 1; i < veci_size(learnt); i++){
if (reasons[lit_var(lits[i])] == 0 || !solver_lit_removable(s,lits[i],minl))
lits[j++] = lits[i];
}
// j = veci_size(learnt);
// update size of learnt + statistics
s->solver_stats.max_literals += veci_size(learnt);
veci_resize(learnt,j);
s->solver_stats.tot_literals += j;
// clear tags
tagged = veci_begin(&s->tagged);
for (i = 0; i < veci_size(&s->tagged); i++)
tags[tagged[i]] = l_Undef;
veci_resize(&s->tagged,0);
#ifdef DEBUG
for (i = 0; i < s->size; i++)
assert(tags[i] == l_Undef);
#endif
#ifdef VERBOSEDEBUG
printf(L_IND"Learnt {", L_ind);
for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i]));
#endif
if (veci_size(learnt) > 1){
int max_i = 1;
int max = levels[lit_var(lits[1])];
lit tmp;
for (i = 2; i < veci_size(learnt); i++)
if (levels[lit_var(lits[i])] > max){
max = levels[lit_var(lits[i])];
max_i = i;
}
tmp = lits[1];
lits[1] = lits[max_i];
lits[max_i] = tmp;
}
#ifdef VERBOSEDEBUG
{
int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
printf(" } at level %d\n", lev);
}
#endif
}
clause* solver_propagate(solver* s)
{
lbool* values = s->assigns;
clause* confl = (clause*)0;
lit* lits;
//printf("solver_propagate\n");
while (confl == 0 && s->qtail - s->qhead > 0){
lit p = s->trail[s->qhead++];
vec* ws = solver_read_wlist(s,p);
clause **begin = (clause**)vec_begin(ws);
clause **end = begin + vec_size(ws);
clause **i, **j;
s->solver_stats.propagations++;
s->simpdb_props--;
//printf("checking lit %d: "L_LIT"\n", vec_size(ws), L_lit(p));
for (i = j = begin; i < end; ){
if (clause_is_lit(*i)){
*j++ = *i;
if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
confl = s->binary;
(clause_begin(confl))[1] = neg(p);
(clause_begin(confl))[0] = clause_read_lit(*i++);
// Copy the remaining watches:
while (i < end)
*j++ = *i++;
}
}else{
lit false_lit;
lbool sig;
lits = clause_begin(*i);
// Make sure the false literal is data[1]:
false_lit = neg(p);
if (lits[0] == false_lit){
lits[0] = lits[1];
lits[1] = false_lit;
}
assert(lits[1] == false_lit);
//printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
// If 0th watch is true, then clause is already satisfied.
sig = !lit_sign(lits[0]); sig += sig - 1;
if (values[lit_var(lits[0])] == sig){
*j++ = *i;
}else{
// Look for new watch:
lit* stop = lits + clause_size(*i);
lit* k;
for (k = lits + 2; k < stop; k++){
lbool sig = lit_sign(*k); sig += sig - 1;
if (values[lit_var(*k)] != sig){
lits[1] = *k;
*k = false_lit;
vec_push(solver_read_wlist(s,neg(lits[1])),*i);
goto next; }
}
*j++ = *i;
// Clause is unit under assignment:
if (!enqueue(s,lits[0], *i)){
confl = *i++;
// Copy the remaining watches:
while (i < end)
*j++ = *i++;
}
}
}
next:
i++;
}
s->solver_stats.inspects += j - (clause**)vec_begin(ws);
vec_resize(ws,j - (clause**)vec_begin(ws));
}
return confl;
}
static inline int clause_cmp (const void* x, const void* y) {
return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
void solver_reducedb(solver* s)
{
int i, j;
double extra_lim = s->cla_inc / vec_size(&s->learnts); // Remove any clause below this activity
clause** learnts = (clause**)vec_begin(&s->learnts);
clause** reasons = s->reasons;
sort(vec_begin(&s->learnts), vec_size(&s->learnts), &clause_cmp);
for (i = j = 0; i < vec_size(&s->learnts) / 2; i++){
if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
clause_remove(s,learnts[i]);
else
learnts[j++] = learnts[i];
}
for (; i < vec_size(&s->learnts); i++){
if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
clause_remove(s,learnts[i]);
else
learnts[j++] = learnts[i];
}
//printf("reducedb deleted %d\n", vec_size(&s->learnts) - j);
vec_resize(&s->learnts,j);
}
static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
{
int* levels = s->levels;
double var_decay = 0.95;
double clause_decay = 0.999;
double random_var_freq = 0.0;//0.02;
int conflictC = 0;
veci learnt_clause;
assert(s->root_level == solver_dlevel(s));
s->solver_stats.starts++;
s->var_decay = (float)(1 / var_decay );
s->cla_decay = (float)(1 / clause_decay);
veci_resize(&s->model,0);
veci_new(&learnt_clause);
for (;;){
clause* confl = solver_propagate(s);
if (confl != 0){
// CONFLICT
int blevel;
#ifdef VERBOSEDEBUG
printf(L_IND"**CONFLICT**\n", L_ind);
#endif
s->solver_stats.conflicts++; conflictC++;
if (solver_dlevel(s) == s->root_level){
veci_delete(&learnt_clause);
return l_False;
}
veci_resize(&learnt_clause,0);
solver_analyze(s, confl, &learnt_clause);
blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
solver_canceluntil(s,blevel);
solver_record(s,&learnt_clause);
act_var_decay(s);
act_clause_decay(s);
}else{
// NO CONFLICT
int next;
if (nof_conflicts >= 0 && conflictC >= nof_conflicts)
{
// Reached bound on number of conflicts:
s->progress_estimate = solver_progress(s);
solver_canceluntil(s,s->root_level);
veci_delete(&learnt_clause);
return l_Undef;
}
if ( s->nConfLimit && s->solver_stats.conflicts > s->nConfLimit ||
s->nInsLimit && s->solver_stats.inspects > s->nInsLimit )
{
// Reached bound on number of conflicts:
s->progress_estimate = solver_progress(s);
solver_canceluntil(s,s->root_level);
veci_delete(&learnt_clause);
return l_Undef;
}
if (solver_dlevel(s) == 0)
// Simplify the set of problem clauses:
solver_simplify(s);
if (nof_learnts >= 0 && vec_size(&s->learnts) - s->qtail >= nof_learnts)
// Reduce the set of learnt clauses:
solver_reducedb(s);
// New variable decision:
s->solver_stats.decisions++;
if ( s->pJMan )
next = Asat_JManSelect( s->pJMan );
else
next = order_select(s,(float)random_var_freq);
if (next == var_Undef){
// Model found:
lbool* values = s->assigns;
int i;
for (i = 0; i < s->size; i++) veci_push(&s->model,(int)values[i]);
solver_canceluntil(s,s->root_level);
veci_delete(&learnt_clause);
return l_True;
}
assume(s,neg(toLit(next)));
}
}
return l_Undef; // cannot happen
}
//=================================================================================================
// External solver functions:
solver* solver_new(void)
{
solver* s = (solver*)malloc(sizeof(solver));
// initialize vectors
vec_new(&s->clauses);
vec_new(&s->learnts);
veci_new(&s->order);
veci_new(&s->trail_lim);
veci_new(&s->tagged);
veci_new(&s->stack);
veci_new(&s->model);
// initialize arrays
s->wlists = 0;
s->activity = 0;
s->factors = 0;
s->assigns = 0;
s->orderpos = 0;
s->reasons = 0;
s->levels = 0;
s->tags = 0;
s->trail = 0;
// initialize other vars
s->size = 0;
s->cap = 0;
s->qhead = 0;
s->qtail = 0;
s->cla_inc = 1;
s->cla_decay = 1;
s->var_inc = 1;
s->var_decay = 1;
s->root_level = 0;
s->simpdb_assigns = 0;
s->simpdb_props = 0;
s->random_seed = 91648253;
s->progress_estimate = 0;
s->binary = (clause*)malloc(sizeof(clause) + sizeof(lit)*2);
s->binary->size_learnt = (2 << 1);
s->verbosity = 0;
s->solver_stats.starts = 0;
s->solver_stats.decisions = 0;
s->solver_stats.propagations = 0;
s->solver_stats.inspects = 0;
s->solver_stats.conflicts = 0;
s->solver_stats.clauses = 0;
s->solver_stats.clauses_literals = 0;
s->solver_stats.learnts = 0;
s->solver_stats.learnts_literals = 0;
s->solver_stats.max_literals = 0;
s->solver_stats.tot_literals = 0;
#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
s->pMem = NULL;
#else
s->pMem = Asat_MmStepStart( 10 );
#endif
s->pJMan = NULL;
s->pPrefVars = NULL;
s->nPrefVars = 0;
s->timeTotal = clock();
s->timeSelect = 0;
s->timeUpdate = 0;
return s;
}
void solver_delete(solver* s)
{
#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
int i;
for (i = 0; i < vec_size(&s->clauses); i++)
free(vec_begin(&s->clauses)[i]);
for (i = 0; i < vec_size(&s->learnts); i++)
free(vec_begin(&s->learnts)[i]);
#else
Asat_MmStepStop( s->pMem, 0 );
#endif
// delete vectors
vec_delete(&s->clauses);
vec_delete(&s->learnts);
veci_delete(&s->order);
veci_delete(&s->trail_lim);
veci_delete(&s->tagged);
veci_delete(&s->stack);
veci_delete(&s->model);
free(s->binary);
// delete arrays
if (s->wlists != 0){
int i;
for (i = 0; i < s->size*2; i++)
vec_delete(&s->wlists[i]);
// if one is different from null, all are
free(s->wlists);
free(s->activity );
free(s->assigns );
free(s->orderpos );
free(s->reasons );
free(s->levels );
free(s->trail );
free(s->tags );
}
if ( s->pJMan ) Asat_JManStop( s );
if ( s->pPrefVars ) free( s->pPrefVars );
if ( s->factors ) free( s->factors );
free(s);
}
bool solver_addclause(solver* s, lit* begin, lit* end)
{
lit *i,*j;
int maxvar;
lbool* values;
lit last;
if (begin == end) return 0;
//printlits(begin,end); printf("\n");
// insertion sort
maxvar = lit_var(*begin);
for (i = begin + 1; i < end; i++){
lit l = *i;
maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
for (j = i; j > begin && *(j-1) > l; j--)
*j = *(j-1);
*j = l;
}
solver_setnvars(s,maxvar+1);
//printlits(begin,end); printf("\n");
values = s->assigns;
// delete duplicates
last = lit_Undef;
for (i = j = begin; i < end; i++){
//printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
lbool sig = !lit_sign(*i); sig += sig - 1;
if (*i == neg(last) || sig == values[lit_var(*i)])
return 1; // tautology
else if (*i != last && values[lit_var(*i)] == l_Undef)
last = *j++ = *i;
}
//printf("final: "); printlits(begin,j); printf("\n");
if (j == begin) // empty clause
return 0;
else if (j - begin == 1) // unit clause
return enqueue(s,*begin,(clause*)0);
// create new clause
vec_push(&s->clauses,clause_new(s,begin,j,0));
s->solver_stats.clauses++;
s->solver_stats.clauses_literals += j - begin;
return 1;
}
bool solver_simplify(solver* s)
{
clause** reasons;
int type;
assert(solver_dlevel(s) == 0);
if (solver_propagate(s) != 0)
return 0;
if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
return 1;
reasons = s->reasons;
for (type = 0; type < 2; type++){
vec* cs = type ? &s->learnts : &s->clauses;
clause** cls = (clause**)vec_begin(cs);
int i, j;
for (j = i = 0; i < vec_size(cs); i++){
if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
clause_simplify(s,cls[i]) == l_True)
clause_remove(s,cls[i]);
else
cls[j++] = cls[i];
}
vec_resize(cs,j);
}
s->simpdb_assigns = s->qhead;
// (shouldn't depend on 'stats' really, but it will do for now)
s->simpdb_props = (int)(s->solver_stats.clauses_literals + s->solver_stats.learnts_literals);
return 1;
}
bool solver_solve(solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit )
{
double nof_conflicts = 100;
// double nof_conflicts = 1000000;
double nof_learnts = solver_nclauses(s) / 3;
lbool status = l_Undef;
lbool* values = s->assigns;
lit* i;
// set the external limits
s->nConfLimit = nConfLimit; // external limit on the number of conflicts
s->nInsLimit = nInsLimit; // external limit on the number of implications
for (i = begin; i < end; i++)
if ((lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]) == l_False || (assume(s,*i), solver_propagate(s) != 0)){
solver_canceluntil(s,0);
return l_False; }
s->root_level = solver_dlevel(s);
if (s->verbosity >= 1){
printf("==================================[MINISAT]===================================\n");
printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n");
printf("| | Clauses Literals | Limit Clauses Literals Lit/Cl | |\n");
printf("==============================================================================\n");
}
while (status == l_Undef){
double Ratio = (s->solver_stats.learnts == 0)? 0.0 :
s->solver_stats.learnts_literals / (double)s->solver_stats.learnts;
if (s->verbosity >= 1){
printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n",
(double)s->solver_stats.conflicts,
(double)s->solver_stats.clauses,
(double)s->solver_stats.clauses_literals,
(double)nof_learnts,
(double)s->solver_stats.learnts,
(double)s->solver_stats.learnts_literals,
Ratio,
s->progress_estimate*100);
fflush(stdout);
}
s->nPrefDecNum = 0;
status = solver_search(s,(int)nof_conflicts, (int)nof_learnts);
nof_conflicts *= 1.5;
nof_learnts *= 1.1;
// quit the loop if reached an external limit
if ( s->nConfLimit && s->solver_stats.conflicts > s->nConfLimit )
{
// printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
break;
}
if ( s->nInsLimit && s->solver_stats.inspects > s->nInsLimit )
{
// printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
break;
}
}
if (s->verbosity >= 1)
printf("==============================================================================\n");
solver_canceluntil(s,0);
s->timeTotal = clock() - s->timeTotal;
return status;
}
int solver_nvars(solver* s)
{
return s->size;
}
int solver_nclauses(solver* s)
{
return vec_size(&s->clauses);
}
//=================================================================================================
// Sorting functions (sigh):
static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
{
int i, j, best_i;
void* tmp;
for (i = 0; i < size-1; i++){
best_i = i;
for (j = i+1; j < size; j++){
if (comp(array[j], array[best_i]) < 0)
best_i = j;
}
tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
}
}
static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
{
if (size <= 15)
selectionsort(array, size, comp);
else{
void* pivot = array[irand(seed, size)];
void* tmp;
int i = -1;
int j = size;
for(;;){
do i++; while(comp(array[i], pivot)<0);
do j--; while(comp(pivot, array[j])<0);
if (i >= j) break;
tmp = array[i]; array[i] = array[j]; array[j] = tmp;
}
sortrnd(array , i , comp, seed);
sortrnd(&array[i], size-i, comp, seed);
}
}
void sort(void** array, int size, int(*comp)(const void *, const void *))
{
double seed = 91648253;
sortrnd(array,size,comp,&seed);
}