src/sat/bsat/satSolver.c File Reference

#include <stdio.h>
#include <assert.h>
#include <string.h>
#include <math.h>
#include "satSolver.h"

Include dependency graph for satSolver.c:

Go to the source code of this file.

Data Structures
struct	clause_t
Defines
#define	L_IND   "%-*d"
#define	L_ind   sat_solver_dlevel(s)*3+3,sat_solver_dlevel(s)
#define	L_LIT   "%sx%d"
#define	L_lit(p)   lit_sign(p)?"~":"", (lit_var(p))
Functions
static void	check (int expr)
static void	printlits (lit *begin, lit *end)
static double	drand (double *seed)
static int	irand (double *seed, int size)
static void	sat_solver_sort (void **array, int size, int(*comp)(const void *, const void *))
static int	clause_size (clause *c)
static lit *	clause_begin (clause *c)
static int	clause_learnt (clause *c)
static float	clause_activity (clause *c)
static void	clause_setactivity (clause *c, float a)
static clause *	clause_from_lit (lit l)
static bool	clause_is_lit (clause *c)
static lit	clause_read_lit (clause *c)
static int	sat_solver_dlevel (sat_solver *s)
static vecp *	sat_solver_read_wlist (sat_solver *s, lit l)
static void	vecp_remove (vecp *v, void *e)
static void	order_update (sat_solver *s, int v)
static void	order_assigned (sat_solver *s, int v)
static void	order_unassigned (sat_solver *s, int v)
static int	order_select (sat_solver *s, float random_var_freq)
static void	act_var_rescale (sat_solver *s)
static void	act_var_bump (sat_solver *s, int v)
static void	act_var_bump_factor (sat_solver *s, int v)
static void	act_var_decay (sat_solver *s)
static void	act_clause_rescale (sat_solver *s)
static void	act_clause_bump (sat_solver *s, clause *c)
static void	act_clause_decay (sat_solver *s)
static clause *	clause_new (sat_solver *s, lit *begin, lit *end, int learnt)
static void	clause_remove (sat_solver *s, clause *c)
static lbool	clause_simplify (sat_solver *s, clause *c)
void	sat_solver_setnvars (sat_solver *s, int n)
static bool	enqueue (sat_solver *s, lit l, clause *from)
static void	assume (sat_solver *s, lit l)
static void	sat_solver_canceluntil (sat_solver *s, int level)
static void	sat_solver_record (sat_solver *s, veci *cls)
static double	sat_solver_progress (sat_solver *s)
static bool	sat_solver_lit_removable (sat_solver *s, lit l, int minl)
static void	sat_solver_analyze (sat_solver *s, clause *c, veci *learnt)
clause *	sat_solver_propagate (sat_solver *s)
static int	clause_cmp (const void *x, const void *y)
void	sat_solver_reducedb (sat_solver *s)
static lbool	sat_solver_search (sat_solver *s, sint64 nof_conflicts, sint64 nof_learnts)
sat_solver *	sat_solver_new (void)
void	sat_solver_delete (sat_solver *s)
bool	sat_solver_addclause (sat_solver *s, lit *begin, lit *end)
bool	sat_solver_simplify (sat_solver *s)
int	sat_solver_solve (sat_solver *s, lit *begin, lit *end, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal)
int	sat_solver_nvars (sat_solver *s)
int	sat_solver_nclauses (sat_solver *s)
int	sat_solver_nconflicts (sat_solver *s)
void	sat_solver_store_alloc (sat_solver *s)
void	sat_solver_store_write (sat_solver *s, char *pFileName)
void	sat_solver_store_free (sat_solver *s)
void	sat_solver_store_mark_roots (sat_solver *s)
void	sat_solver_store_mark_clauses_a (sat_solver *s)
void *	sat_solver_store_release (sat_solver *s)
static void	selectionsort (void **array, int size, int(*comp)(const void *, const void *))
static void	sortrnd (void **array, int size, int(*comp)(const void *, const void *), double *seed)

---

Define Documentation

#define L_ind   sat_solver_dlevel(s)*3+3,sat_solver_dlevel(s)

Definition at line 38 of file satSolver.c.

#define L_IND   "%-*d"

Definition at line 37 of file satSolver.c.

#define L_lit

(

p

)

lit_sign(p)?"~":"", (lit_var(p))

Definition at line 40 of file satSolver.c.

#define L_LIT   "%sx%d"

Definition at line 39 of file satSolver.c.

---

Function Documentation

static void act_clause_bump	(	sat_solver *	s,
		clause *	c
	)			[inline, static]

Definition at line 258 of file satSolver.c.

                                                             {
    float a = clause_activity(c) + s->cla_inc;
    clause_setactivity(c,a);
    if (a > 1e20) act_clause_rescale(s);
}

static void act_clause_decay

(

sat_solver *

s

)

[inline, static]

Definition at line 264 of file satSolver.c.

{ s->cla_inc *= s->cla_decay; }

static void act_clause_rescale

(

sat_solver *

s

)

[inline, static]

Definition at line 247 of file satSolver.c.

                                                     {
    clause** cs = (clause**)vecp_begin(&s->learnts);
    int i;
    for (i = 0; i < vecp_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 void act_var_bump	(	sat_solver *	s,
		int	v
	)			[inline, static]

Definition at line 227 of file satSolver.c.

                                                      {
    s->activity[v] += s->var_inc;
    if (s->activity[v] > 1e100)
        act_var_rescale(s);
    //printf("bump %d %f\n", v-1, activity[v]);
    if (s->orderpos[v] != -1)
        order_update(s,v);
}

static void act_var_bump_factor	(	sat_solver *	s,
		int	v
	)			[inline, static]

Definition at line 236 of file satSolver.c.

                                                             {
    s->activity[v] += (s->var_inc * s->factors[v]);
    if (s->activity[v] > 1e100)
        act_var_rescale(s);
    //printf("bump %d %f\n", v-1, activity[v]);
    if (s->orderpos[v] != -1)
        order_update(s,v);
}

static void act_var_decay

(

sat_solver *

s

)

[inline, static]

Definition at line 245 of file satSolver.c.

{ s->var_inc *= s->var_decay; }

static void act_var_rescale

(

sat_solver *

s

)

[inline, static]

Definition at line 219 of file satSolver.c.

                                                  {
    double* activity = s->activity;
    int i;
    for (i = 0; i < s->size; i++)
        activity[i] *= 1e-100;
    s->var_inc *= 1e-100;
}

static void assume	(	sat_solver *	s,
		lit	l
	)			[inline, static]

Definition at line 434 of file satSolver.c.

                                               {
    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 void check

(

int

expr

)

[inline, static]

Definition at line 43 of file satSolver.c.

{ assert(expr); }

static float clause_activity

(

clause *

c

)

[inline, static]

Definition at line 87 of file satSolver.c.

{ return *((float*)&c->lits[c->size_learnt>>1]); }

static lit* clause_begin

(

clause *

c

)

[inline, static]

Definition at line 85 of file satSolver.c.

{ return c->lits; }

static int clause_cmp	(	const void *	x,
		const void *	y
	)			[inline, static]

Definition at line 791 of file satSolver.c.

                                                            {
    return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }

static clause* clause_from_lit

(

lit

l

)

[inline, static]

Definition at line 93 of file satSolver.c.

{ return (clause*)((unsigned long)l + (unsigned long)l + 1);  }

static bool clause_is_lit

(

clause *

c

)

[inline, static]

Definition at line 94 of file satSolver.c.

{ return ((unsigned long)c & 1);                              }

static int clause_learnt

(

clause *

c

)

[inline, static]

Definition at line 86 of file satSolver.c.

{ return c->size_learnt & 1; }

static clause* clause_new	(	sat_solver *	s,
		lit *	begin,
		lit *	end,
		int	learnt
	)			[static]

Definition at line 271 of file satSolver.c.

{
    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 SAT_USE_SYSTEM_MEMORY_MANAGEMENT
    c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
#else
    c = (clause*)Sat_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++)
        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(lit_neg(begin[0]) < s->size*2);
    assert(lit_neg(begin[1]) < s->size*2);

    //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
    //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);

    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])));

    return c;
}

static lit clause_read_lit

(

clause *

c

)

[inline, static]

Definition at line 95 of file satSolver.c.

{ return (lit)((unsigned long)c >> 1);                        }

static void clause_remove	(	sat_solver *	s,
		clause *	c
	)			[static]

Definition at line 314 of file satSolver.c.

{
    lit* lits = clause_begin(c);
    assert(lit_neg(lits[0]) < s->size*2);
    assert(lit_neg(lits[1]) < s->size*2);

    //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
    //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);

    assert(lits[0] < s->size*2);
    vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
    vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));

    if (clause_learnt(c)){
        s->stats.learnts--;
        s->stats.learnts_literals -= clause_size(c);
    }else{
        s->stats.clauses--;
        s->stats.clauses_literals -= clause_size(c);
    }

#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
    free(c);
#else
    Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
#endif
}

static void clause_setactivity	(	clause *	c,
		float	a
	)			[inline, static]

Definition at line 88 of file satSolver.c.

{ *((float*)&c->lits[c->size_learnt>>1]) = a; }

static lbool clause_simplify	(	sat_solver *	s,
		clause *	c
	)			[static]

Definition at line 343 of file satSolver.c.

{
    lit*   lits   = clause_begin(c);
    lbool* values = s->assigns;
    int i;

    assert(sat_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;
}

static int clause_size

(

clause *

c

)

[inline, static]

Definition at line 84 of file satSolver.c.

{ return c->size_learnt >> 1; }

static double drand

(

double *

seed

)

[inline, static]

Definition at line 57 of file satSolver.c.

                                         {
    int q;
    *seed *= 1389796;
    q = (int)(*seed / 2147483647);
    *seed -= (double)q * 2147483647;
    return *seed / 2147483647; }

static bool enqueue	(	sat_solver *	s,
		lit	l,
		clause *	from
	)			[inline, static]

Definition at line 403 of file satSolver.c.

{
    lbool* values = s->assigns;
    int    v      = lit_var(l);
    lbool  val    = values[v];
#ifdef VERBOSEDEBUG
    printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
#endif

    lbool sig = !lit_sign(l); sig += sig - 1;
    if (val != l_Undef){
        return val == sig;
    }else{
        // New fact -- store it.
#ifdef VERBOSEDEBUG
        printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
#endif
        int*     levels  = s->levels;
        clause** reasons = s->reasons;

        values [v] = sig;
        levels [v] = sat_solver_dlevel(s);
        reasons[v] = from;
        s->trail[s->qtail++] = l;

        order_assigned(s, v);
        return true;
    }
}

static int irand	(	double *	seed,
		int	size
	)			[inline, static]

Definition at line 66 of file satSolver.c.

                                                {
    return (int)(drand(seed) * size); }

static void order_assigned	(	sat_solver *	s,
		int	v
	)			[inline, static]

Definition at line 136 of file satSolver.c.

{
}

static int order_select	(	sat_solver *	s,
		float	random_var_freq
	)			[inline, static]

Definition at line 151 of file satSolver.c.

{
    int*    heap;
    double* activity;
    int*    orderpos;

    lbool* values = s->assigns;

    // 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;
        }

//printf( "-%d ", next );
        if (values[next] == l_Undef)
            return next;
    }

    return var_Undef;
}

static void order_unassigned	(	sat_solver *	s,
		int	v
	)			[inline, static]

Definition at line 140 of file satSolver.c.

{
    int* orderpos = s->orderpos;
    if (orderpos[v] == -1){
        orderpos[v] = veci_size(&s->order);
        veci_push(&s->order,v);
        order_update(s,v);
//printf( "+%d ", v );
    }
}

static void order_update	(	sat_solver *	s,
		int	v
	)			[inline, static]

Definition at line 115 of file satSolver.c.

{
    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;
}

static void printlits	(	lit *	begin,
		lit *	end
	)			[static]

Definition at line 45 of file satSolver.c.

{
    int i;
    for (i = 0; i < end - begin; i++)
        printf(L_LIT" ",L_lit(begin[i]));
}

bool sat_solver_addclause	(	sat_solver *	s,
		lit *	begin,
		lit *	end
	)

Definition at line 1048 of file satSolver.c.

{
    lit *i,*j;
    int maxvar;
    lbool* values;
    lit last;

    if (begin == end) return false;

    //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;
    }
    sat_solver_setnvars(s,maxvar+1);
//    sat_solver_setnvars(s, lit_var(*(end-1))+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 == lit_neg(last) || sig == values[lit_var(*i)])
            return true;   // 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 false;

    // add clause to internal storage
    if ( s->pStore )
    {
        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
        int RetValue = Sto_ManAddClause( s->pStore, begin, j );
        assert( RetValue );
    }

    if (j - begin == 1) // unit clause
        return enqueue(s,*begin,(clause*)0);

    // create new clause
    vecp_push(&s->clauses,clause_new(s,begin,j,0));


    s->stats.clauses++;
    s->stats.clauses_literals += j - begin;

    return true;
}

static void sat_solver_analyze	(	sat_solver *	s,
		clause *	c,
		veci *	learnt
	)			[static]

Definition at line 587 of file satSolver.c.

{
    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)] == sat_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)] == sat_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) = lit_neg(p);

    lits = veci_begin(learnt);
    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 || !sat_solver_lit_removable(s,lits[i],minl))
            lits[j++] = lits[i];
    }

    // update size of learnt + statistics
    s->stats.max_literals += veci_size(learnt);
    veci_resize(learnt,j);
    s->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
}

static void sat_solver_canceluntil	(	sat_solver *	s,
		int	level
	)			[static]

Definition at line 445 of file satSolver.c.

                                                             {
    lit*     trail;   
    lbool*   values;  
    clause** reasons; 
    int      bound;
    int      c;
    
    if (sat_solver_dlevel(s) <= level)
        return;

    trail   = s->trail;
    values  = s->assigns;
    reasons = s->reasons;
    bound   = (veci_begin(&s->trail_lim))[level];

    // added to cancel all assignments
//    if ( level == -1 )
//        bound = 0;

    for (c = s->qtail-1; c >= bound; c--) {
        int     x  = lit_var(trail[c]);
        values [x] = l_Undef;
        reasons[x] = (clause*)0;
    }

    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);
}

void sat_solver_delete

(

sat_solver *

s

)

Definition at line 1001 of file satSolver.c.

{

#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
    int i;
    for (i = 0; i < vecp_size(&s->clauses); i++)
        free(vecp_begin(&s->clauses)[i]);
    for (i = 0; i < vecp_size(&s->learnts); i++)
        free(vecp_begin(&s->learnts)[i]);
#else
    Sat_MmStepStop( s->pMem, 0 );
#endif

    // delete vectors
    vecp_delete(&s->clauses);
    vecp_delete(&s->learnts);
    veci_delete(&s->order);
    veci_delete(&s->trail_lim);
    veci_delete(&s->tagged);
    veci_delete(&s->stack);
    veci_delete(&s->model);
    veci_delete(&s->act_vars);
    free(s->binary);

    // delete arrays
    if (s->wlists != 0){
        int i;
        for (i = 0; i < s->size*2; i++)
            vecp_delete(&s->wlists[i]);

        // if one is different from null, all are
        free(s->wlists   );
        free(s->activity );
        free(s->factors  );
        free(s->assigns  );
        free(s->orderpos );
        free(s->reasons  );
        free(s->levels   );
        free(s->trail    );
        free(s->tags     );
    }

    sat_solver_store_free(s);
    free(s);
}

static int sat_solver_dlevel

(

sat_solver *

s

)

[inline, static]

Definition at line 100 of file satSolver.c.

{ return veci_size(&s->trail_lim); }

static bool sat_solver_lit_removable	(	sat_solver *	s,
		lit	l,
		int	minl
	)			[static]

Definition at line 524 of file satSolver.c.

{
    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 false;
                }
            }
        }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 false;
                    }
                }
            }
        }
    }

    return true;
}

int sat_solver_nclauses

(

sat_solver *

s

)

Definition at line 1254 of file satSolver.c.

{
    return vecp_size(&s->clauses);
}

int sat_solver_nconflicts

(

sat_solver *

s

)

Definition at line 1260 of file satSolver.c.

{
    return (int)s->stats.conflicts;
}

sat_solver* sat_solver_new

(

void

)

Definition at line 935 of file satSolver.c.

{
    sat_solver* s = (sat_solver*)malloc(sizeof(sat_solver));
    memset( s, 0, sizeof(sat_solver) );

    // initialize vectors
    vecp_new(&s->clauses);
    vecp_new(&s->learnts);
    veci_new(&s->order);
    veci_new(&s->trail_lim);
    veci_new(&s->tagged);
    veci_new(&s->stack);
    veci_new(&s->model);
    veci_new(&s->act_vars);

    // 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->stats.starts           = 0;
    s->stats.decisions        = 0;
    s->stats.propagations     = 0;
    s->stats.inspects         = 0;
    s->stats.conflicts        = 0;
    s->stats.clauses          = 0;
    s->stats.clauses_literals = 0;
    s->stats.learnts          = 0;
    s->stats.learnts_literals = 0;
    s->stats.max_literals     = 0;
    s->stats.tot_literals     = 0;

#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
    s->pMem = NULL;
#else
    s->pMem = Sat_MmStepStart( 10 );
#endif
    return s;
}

int sat_solver_nvars

(

sat_solver *

s

)

Definition at line 1248 of file satSolver.c.

{
    return s->size;
}

static double sat_solver_progress

(

sat_solver *

s

)

[static]

Definition at line 507 of file satSolver.c.

{
    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;
}

clause* sat_solver_propagate

(

sat_solver *

s

)

Definition at line 706 of file satSolver.c.

{
    lbool*  values = s->assigns;
    clause* confl  = (clause*)0;
    lit*    lits;

    //printf("sat_solver_propagate\n");
    while (confl == 0 && s->qtail - s->qhead > 0){
        lit  p  = s->trail[s->qhead++];
        vecp* ws = sat_solver_read_wlist(s,p);
        clause **begin = (clause**)vecp_begin(ws);
        clause **end   = begin + vecp_size(ws);
        clause **i, **j;

        s->stats.propagations++;
        s->simpdb_props--;

        //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
        for (i = j = begin; i < end; ){
            if (clause_is_lit(*i)){
//                s->stats.inspects2++;
                *j++ = *i;
                if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
                    confl = s->binary;
                    (clause_begin(confl))[1] = lit_neg(p);
                    (clause_begin(confl))[0] = clause_read_lit(*i++);
                    // Copy the remaining watches:
//                    s->stats.inspects2 += end - i;
                    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 = 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;
                            vecp_push(sat_solver_read_wlist(s,lit_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:
//                        s->stats.inspects2 += end - i;
                        while (i < end)
                            *j++ = *i++;
                    }
                }
            }
        next:
            i++;
        }

        s->stats.inspects += j - (clause**)vecp_begin(ws);
        vecp_resize(ws,j - (clause**)vecp_begin(ws));
    }

    return confl;
}

static vecp* sat_solver_read_wlist	(	sat_solver *	s,
		lit	l
	)			[inline, static]

Definition at line 101 of file satSolver.c.

{ return &s->wlists[l]; }

static void sat_solver_record	(	sat_solver *	s,
		veci *	cls
	)			[static]

Definition at line 479 of file satSolver.c.

{
    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);

    // add clause to internal storage
    if ( s->pStore )
    {
        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
        int RetValue = Sto_ManAddClause( s->pStore, begin, end );
        assert( RetValue );
    }

    assert(veci_size(cls) > 0);

    if (c != 0) {
        vecp_push(&s->learnts,c);
        act_clause_bump(s,c);
        s->stats.learnts++;
        s->stats.learnts_literals += veci_size(cls);
    }
}

void sat_solver_reducedb

(

sat_solver *

s

)

Definition at line 794 of file satSolver.c.

{
    int      i, j;
    double   extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
    clause** learnts = (clause**)vecp_begin(&s->learnts);
    clause** reasons = s->reasons;

    sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);

    for (i = j = 0; i < vecp_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 < vecp_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", vecp_size(&s->learnts) - j);


    vecp_resize(&s->learnts,j);
}

static lbool sat_solver_search	(	sat_solver *	s,
		sint64	nof_conflicts,
		sint64	nof_learnts
	)			[static]

Definition at line 822 of file satSolver.c.

{
    int*    levels          = s->levels;
    double  var_decay       = 0.95;
    double  clause_decay    = 0.999;
    double  random_var_freq = 0.02;

    sint64  conflictC       = 0;
    veci    learnt_clause;
    int     i;

    assert(s->root_level == sat_solver_dlevel(s));

    s->nRestarts++;
    s->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);

    // use activity factors in every even restart
    if ( (s->nRestarts & 1) && veci_size(&s->act_vars) > 0 )
        for ( i = 0; i < s->act_vars.size; i++ )
            act_var_bump_factor(s, s->act_vars.ptr[i]);

    for (;;){
        clause* confl = sat_solver_propagate(s);
        if (confl != 0){
            // CONFLICT
            int blevel;

#ifdef VERBOSEDEBUG
            printf(L_IND"**CONFLICT**\n", L_ind);
#endif
            s->stats.conflicts++; conflictC++;
            if (sat_solver_dlevel(s) == s->root_level){
                veci_delete(&learnt_clause);
                return l_False;
            }

            veci_resize(&learnt_clause,0);
            sat_solver_analyze(s, confl, &learnt_clause);
            blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
            blevel = s->root_level > blevel ? s->root_level : blevel;
            sat_solver_canceluntil(s,blevel);
            sat_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 = sat_solver_progress(s);
                sat_solver_canceluntil(s,s->root_level);
                veci_delete(&learnt_clause);
                return l_Undef; }

            if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit ||
                 s->nInsLimit  && s->stats.inspects  > s->nInsLimit )
            {
                // Reached bound on number of conflicts:
                s->progress_estimate = sat_solver_progress(s);
                sat_solver_canceluntil(s,s->root_level);
                veci_delete(&learnt_clause);
                return l_Undef; 
            }

            if (sat_solver_dlevel(s) == 0 && !s->fSkipSimplify)
                // Simplify the set of problem clauses:
                sat_solver_simplify(s);

            if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
                // Reduce the set of learnt clauses:
                sat_solver_reducedb(s);

            // New variable decision:
            s->stats.decisions++;
            next = order_select(s,(float)random_var_freq);

            if (next == var_Undef){
                // Model found:
                lbool* values = s->assigns;
                int i;
                veci_resize(&s->model, 0);
                for (i = 0; i < s->size; i++) 
                    veci_push(&s->model,(int)values[i]);
                sat_solver_canceluntil(s,s->root_level);
                veci_delete(&learnt_clause);

                /*
                veci apa; veci_new(&apa);
                for (i = 0; i < s->size; i++) 
                    veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i))));
                printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n");
                veci_delete(&apa);
                */

                return l_True;
            }

            assume(s,lit_neg(toLit(next)));
        }
    }

    return l_Undef; // cannot happen
}

void sat_solver_setnvars	(	sat_solver *	s,
		int	n
	)

Definition at line 362 of file satSolver.c.

{
    int var;

    if (s->cap < n){

        while (s->cap < n) s->cap = s->cap*2+1;

        s->wlists    = (vecp*)   realloc(s->wlists,   sizeof(vecp)*s->cap*2);
        s->activity  = (double*) realloc(s->activity, sizeof(double)*s->cap);
        s->factors   = (double*) realloc(s->factors,  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++){
        vecp_new(&s->wlists[2*var]);
        vecp_new(&s->wlists[2*var+1]);
        s->activity [var] = 0;
        s->factors  [var] = 0;
        s->assigns  [var] = l_Undef;
        s->orderpos [var] = veci_size(&s->order);
        s->reasons  [var] = (clause*)0;
        s->levels   [var] = 0;
        s->tags     [var] = l_Undef;
        
        /* does not hold because variables enqueued at top level will not be reinserted in the heap
           assert(veci_size(&s->order) == var); 
         */
        veci_push(&s->order,var);
        order_update(s, var);
    }

    s->size = n > s->size ? n : s->size;
}

bool sat_solver_simplify

(

sat_solver *

s

)

Definition at line 1113 of file satSolver.c.

{
    clause** reasons;
    int type;

    assert(sat_solver_dlevel(s) == 0);

    if (sat_solver_propagate(s) != 0)
        return false;

    if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
        return true;

    reasons = s->reasons;
    for (type = 0; type < 2; type++){
        vecp*    cs  = type ? &s->learnts : &s->clauses;
        clause** cls = (clause**)vecp_begin(cs);

        int i, j;
        for (j = i = 0; i < vecp_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];
        }
        vecp_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->stats.clauses_literals + s->stats.learnts_literals);

    return true;
}

int sat_solver_solve	(	sat_solver *	s,
		lit *	begin,
		lit *	end,
		sint64	nConfLimit,
		sint64	nInsLimit,
		sint64	nConfLimitGlobal,
		sint64	nInsLimitGlobal
	)

Definition at line 1150 of file satSolver.c.

{
    sint64  nof_conflicts = 100;
    sint64  nof_learnts   = sat_solver_nclauses(s) / 3;
    lbool   status        = l_Undef;
    lbool*  values        = s->assigns;
    lit*    i;

    // set the external limits
    s->nCalls++;
    s->nRestarts  = 0;
    s->nConfLimit = 0;
    s->nInsLimit  = 0;
    if ( nConfLimit )
        s->nConfLimit = s->stats.conflicts + nConfLimit;
    if ( nInsLimit )
        s->nInsLimit = s->stats.inspects + nInsLimit;
    if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) )
        s->nConfLimit = nConfLimitGlobal;
    if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
        s->nInsLimit = nInsLimitGlobal;

    //printf("solve: "); printlits(begin, end); printf("\n");
    for (i = begin; i < end; i++){
        switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
        case 1: /* l_True: */
            break;
        case 0: /* l_Undef */
            assume(s, *i);
            if (sat_solver_propagate(s) == NULL)
                break;
            // fallthrough
        case -1: /* l_False */
            sat_solver_canceluntil(s, 0);
            return l_False;
        }
    }
    s->nCalls2++;

    s->root_level = sat_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->stats.learnts == 0)? 0.0 :
            s->stats.learnts_literals / (double)s->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->stats.conflicts,
                (double)s->stats.clauses, 
                (double)s->stats.clauses_literals,
                (double)nof_learnts, 
                (double)s->stats.learnts, 
                (double)s->stats.learnts_literals,
                Ratio,
                s->progress_estimate*100);
            fflush(stdout);
        }
        status = sat_solver_search(s, nof_conflicts, nof_learnts);
        nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
        nof_learnts   = nof_learnts * 11 / 10; //*= 1.1;

        // quit the loop if reached an external limit
        if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
        {
//            printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
            break;
        }
        if ( s->nInsLimit  && s->stats.inspects > s->nInsLimit )
        {
//            printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
            break;
        }
    }
    if (s->verbosity >= 1)
        printf("==============================================================================\n");

    sat_solver_canceluntil(s,0);

    if ( status == l_False && s->pStore )
    {
        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
        int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL );
        assert( RetValue );
    }
    return status;
}

void sat_solver_sort	(	void **	array,
		int	size,
		int(*)(const void *, const void *)	comp
	)			[static]

Definition at line 1354 of file satSolver.c.

{
    double seed = 91648253;
    sortrnd(array,size,comp,&seed);
}

void sat_solver_store_alloc

(

sat_solver *

s

)

Definition at line 1268 of file satSolver.c.

{
    extern void * Sto_ManAlloc();
    assert( s->pStore == NULL );
    s->pStore = Sto_ManAlloc();
}

void sat_solver_store_free

(

sat_solver *

s

)

Definition at line 1281 of file satSolver.c.

{
    extern void Sto_ManFree( void * p );
    if ( s->pStore ) Sto_ManFree( s->pStore );
    s->pStore = NULL;
}

void sat_solver_store_mark_clauses_a

(

sat_solver *

s

)

Definition at line 1294 of file satSolver.c.

{
    extern void Sto_ManMarkClausesA( void * p );
    if ( s->pStore ) Sto_ManMarkClausesA( s->pStore );
}

void sat_solver_store_mark_roots

(

sat_solver *

s

)

Definition at line 1288 of file satSolver.c.

{
    extern void Sto_ManMarkRoots( void * p );
    if ( s->pStore ) Sto_ManMarkRoots( s->pStore );
}

void* sat_solver_store_release

(

sat_solver *

s

)

Definition at line 1300 of file satSolver.c.

{
    void * pTemp;
    if ( s->pStore == NULL )
        return NULL;
    pTemp = s->pStore;
    s->pStore = NULL;
    return pTemp;
}

void sat_solver_store_write	(	sat_solver *	s,
		char *	pFileName
	)

Definition at line 1275 of file satSolver.c.

{
    extern void Sto_ManDumpClauses( void * p, char * pFileName );
    if ( s->pStore ) Sto_ManDumpClauses( s->pStore, pFileName );
}

static void selectionsort	(	void **	array,
		int	size,
		int(*)(const void *, const void *)	comp
	)			[inline, static]

Definition at line 1313 of file satSolver.c.

{
    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(*)(const void *, const void *)	comp,
		double *	seed
	)			[static]

Definition at line 1329 of file satSolver.c.

{
    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);
    }
}

static void vecp_remove	(	vecp *	v,
		void *	e
	)			[inline, static]

Definition at line 102 of file satSolver.c.

{
    void** ws = vecp_begin(v);
    int    j  = 0;
    for (; ws[j] != e  ; j++);
    assert(j < vecp_size(v));
    for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1];
    vecp_resize(v,vecp_size(v)-1);
}