Minisat::Solver Class Reference

#include <Solver.h>

Inherited by Minisat::SimpSolver.

Data Structures
struct	VarData
struct	VarOrderLt
struct	Watcher
struct	WatcherDeleted

Public Member Functions
	Solver ()
virtual	~Solver ()
Var	newVar (bool polarity=true, bool dvar=true)
bool	addClause (const vec< Lit > &ps)
bool	addEmptyClause ()
bool	addClause (Lit p)
bool	addClause (Lit p, Lit q)
bool	addClause (Lit p, Lit q, Lit r)
bool	addClause_ (vec< Lit > &ps)
bool	simplify ()
bool	solve (const vec< Lit > &assumps)
lbool	solveLimited (const vec< Lit > &assumps)
bool	solve ()
bool	solve (Lit p)
bool	solve (Lit p, Lit q)
bool	solve (Lit p, Lit q, Lit r)
bool	okay () const
void	toDimacs (FILE *f, const vec< Lit > &assumps)
void	toDimacs (const char *file, const vec< Lit > &assumps)
void	toDimacs (FILE *f, Clause &c, vec< Var > &map, Var &max)
void	toDimacs (const char *file)
void	toDimacs (const char *file, Lit p)
void	toDimacs (const char *file, Lit p, Lit q)
void	toDimacs (const char *file, Lit p, Lit q, Lit r)
void	setPolarity (Var v, bool b)
void	setDecisionVar (Var v, bool b)
lbool	value (Var x) const
lbool	value (Lit p) const
lbool	modelValue (Var x) const
lbool	modelValue (Lit p) const
int	nAssigns () const
int	nClauses () const
int	nLearnts () const
int	nVars () const
int	nFreeVars () const
void	setConfBudget (int64_t x)
void	setPropBudget (int64_t x)
void	budgetOff ()
void	interrupt ()
void	clearInterrupt ()
virtual void	garbageCollect ()
void	checkGarbage (double gf)
void	checkGarbage ()

Data Fields
vec< lbool >	model
vec< Lit >	conflict
int	verbosity
double	var_decay
double	clause_decay
double	random_var_freq
double	random_seed
bool	luby_restart
int	ccmin_mode
int	phase_saving
bool	rnd_pol
bool	rnd_init_act
double	garbage_frac
int	restart_first
double	restart_inc
double	learntsize_factor
double	learntsize_inc
int	learntsize_adjust_start_confl
double	learntsize_adjust_inc
uint64_t	solves
uint64_t	starts
uint64_t	decisions
uint64_t	rnd_decisions
uint64_t	propagations
uint64_t	conflicts
uint64_t	dec_vars
uint64_t	clauses_literals
uint64_t	learnts_literals
uint64_t	max_literals
uint64_t	tot_literals

Protected Member Functions
void	insertVarOrder (Var x)
Lit	pickBranchLit ()
void	newDecisionLevel ()
void	uncheckedEnqueue (Lit p, CRef from=CRef_Undef)
bool	enqueue (Lit p, CRef from=CRef_Undef)
CRef	propagate ()
void	cancelUntil (int level)
void	analyze (CRef confl, vec< Lit > &out_learnt, int &out_btlevel)
void	analyzeFinal (Lit p, vec< Lit > &out_conflict)
bool	litRedundant (Lit p, uint32_t abstract_levels)
lbool	search (int nof_conflicts)
lbool	solve_ ()
void	reduceDB ()
void	removeSatisfied (vec< CRef > &cs)
void	rebuildOrderHeap ()
void	varDecayActivity ()
void	varBumpActivity (Var v, double inc)
void	varBumpActivity (Var v)
void	claDecayActivity ()
void	claBumpActivity (Clause &c)
void	attachClause (CRef cr)
void	detachClause (CRef cr, bool strict=false)
void	removeClause (CRef cr)
bool	locked (const Clause &c) const
bool	satisfied (const Clause &c) const
void	relocAll (ClauseAllocator &to)
int	decisionLevel () const
uint32_t	abstractLevel (Var x) const
CRef	reason (Var x) const
int	level (Var x) const
double	progressEstimate () const
bool	withinBudget () const

Static Protected Member Functions
static VarData	mkVarData (CRef cr, int l)
static double	drand (double &seed)
static int	irand (double &seed, int size)

Protected Attributes
bool	ok
vec< CRef >	clauses
vec< CRef >	learnts
double	cla_inc
vec< double >	activity
double	var_inc
OccLists< Lit, vec< Watcher > , WatcherDeleted >	watches
vec< lbool >	assigns
vec< char >	polarity
vec< char >	decision
vec< Lit >	trail
vec< int >	trail_lim
vec< VarData >	vardata
int	qhead
int	simpDB_assigns
int64_t	simpDB_props
vec< Lit >	assumptions
Heap< VarOrderLt >	order_heap
double	progress_estimate
bool	remove_satisfied
ClauseAllocator	ca
vec< char >	seen
vec< Lit >	analyze_stack
vec< Lit >	analyze_toclear
vec< Lit >	add_tmp
double	max_learnts
double	learntsize_adjust_confl
int	learntsize_adjust_cnt
int64_t	conflict_budget
int64_t	propagation_budget
bool	asynch_interrupt

Detailed Description

Definition at line 36 of file Solver.h.

Constructor & Destructor Documentation

Solver::Solver

(

)

Definition at line 51 of file Solver.cpp.

               :

    // Parameters (user settable):
    //
    verbosity        (0)
  , var_decay        (opt_var_decay)
  , clause_decay     (opt_clause_decay)
  , random_var_freq  (opt_random_var_freq)
  , random_seed      (opt_random_seed)
  , luby_restart     (opt_luby_restart)
  , ccmin_mode       (opt_ccmin_mode)
  , phase_saving     (opt_phase_saving)
  , rnd_pol          (false)
  , rnd_init_act     (opt_rnd_init_act)
  , garbage_frac     (opt_garbage_frac)
  , restart_first    (opt_restart_first)
  , restart_inc      (opt_restart_inc)

    // Parameters (the rest):
    //
  , learntsize_factor((double)1/(double)3), learntsize_inc(1.1)

    // Parameters (experimental):
    //
  , learntsize_adjust_start_confl (100)
  , learntsize_adjust_inc         (1.5)

    // Statistics: (formerly in 'SolverStats')
    //
  , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)
  , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)

  , ok                 (true)
  , cla_inc            (1)
  , var_inc            (1)
  , watches            (WatcherDeleted(ca))
  , qhead              (0)
  , simpDB_assigns     (-1)
  , simpDB_props       (0)
  , order_heap         (VarOrderLt(activity))
  , progress_estimate  (0)
  , remove_satisfied   (true)

    // Resource constraints:
    //
  , conflict_budget    (-1)
  , propagation_budget (-1)
  , asynch_interrupt   (false)
{}

Solver::~Solver ( )

virtual

Definition at line 102 of file Solver.cpp.

{
}

Member Function Documentation

uint32_t Minisat::Solver::abstractLevel ( Var  x ) const

inlineprotected

Definition at line 320 of file Solver.h.

{ return 1 << (level(x) & 31); }

bool Minisat::Solver::addClause ( const vec< Lit > &  ps )

inline

Definition at line 311 of file Solver.h.

{ ps.copyTo(add_tmp); return addClause_(add_tmp); }

bool Minisat::Solver::addClause ( Lit  p )

inline

Definition at line 313 of file Solver.h.

{ add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }

bool Minisat::Solver::addClause ( Lit  p, Lit  q  )

inline

Definition at line 314 of file Solver.h.

{ add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }

bool Minisat::Solver::addClause ( Lit  p, Lit  q, Lit  r  )

inline

Definition at line 315 of file Solver.h.

{ add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }

bool Solver::addClause_

(

vec< Lit > &

ps

)

Definition at line 132 of file Solver.cpp.

{
    assert(decisionLevel() == 0);
    if (!ok) return false;

    // Check if clause is satisfied and remove false/duplicate literals:
    sort(ps);
    Lit p; int i, j;
    for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
        if (value(ps[i]) == l_True || ps[i] == ~p)
            return true;
        else if (value(ps[i]) != l_False && ps[i] != p)
            ps[j++] = p = ps[i];
    ps.shrink(i - j);

    if (ps.size() == 0)
        return ok = false;
    else if (ps.size() == 1){
        uncheckedEnqueue(ps[0]);
        return ok = (propagate() == CRef_Undef);
    }else{
        CRef cr = ca.alloc(ps, false);
        clauses.push(cr);
        attachClause(cr);
    }

    return true;
}

bool Minisat::Solver::addEmptyClause ( )

inline

Definition at line 312 of file Solver.h.

{ add_tmp.clear(); return addClause_(add_tmp); }

void Solver::analyze ( CRef  confl, vec< Lit > &  out_learnt, int &  out_btlevel  )

protected

Definition at line 264 of file Solver.cpp.

{
    int pathC = 0;
    Lit p     = lit_Undef;

    // Generate conflict clause:
    //
    out_learnt.push();      // (leave room for the asserting literal)
    int index   = trail.size() - 1;

    do{
        assert(confl != CRef_Undef); // (otherwise should be UIP)
        Clause& c = ca[confl];

        if (c.learnt())
            claBumpActivity(c);

        for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
            Lit q = c[j];

            if (!seen[var(q)] && level(var(q)) > 0){
                varBumpActivity(var(q));
                seen[var(q)] = 1;
                if (level(var(q)) >= decisionLevel())
                    pathC++;
                else
                    out_learnt.push(q);
            }
        }
        
        // Select next clause to look at:
        while (!seen[var(trail[index--])]);
        p     = trail[index+1];
        confl = reason(var(p));
        seen[var(p)] = 0;
        pathC--;

    }while (pathC > 0);
    out_learnt[0] = ~p;

    // Simplify conflict clause:
    //
    int i, j;
    out_learnt.copyTo(analyze_toclear);
    if (ccmin_mode == 2){
        uint32_t abstract_level = 0;
        for (i = 1; i < out_learnt.size(); i++)
            abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict)

        for (i = j = 1; i < out_learnt.size(); i++)
            if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i], abstract_level))
                out_learnt[j++] = out_learnt[i];
        
    }else if (ccmin_mode == 1){
        for (i = j = 1; i < out_learnt.size(); i++){
            Var x = var(out_learnt[i]);

            if (reason(x) == CRef_Undef)
                out_learnt[j++] = out_learnt[i];
            else{
                Clause& c = ca[reason(var(out_learnt[i]))];
                for (int k = 1; k < c.size(); k++)
                    if (!seen[var(c[k])] && level(var(c[k])) > 0){
                        out_learnt[j++] = out_learnt[i];
                        break; }
            }
        }
    }else
        i = j = out_learnt.size();

    max_literals += out_learnt.size();
    out_learnt.shrink(i - j);
    tot_literals += out_learnt.size();

    // Find correct backtrack level:
    //
    if (out_learnt.size() == 1)
        out_btlevel = 0;
    else{
        int max_i = 1;
        // Find the first literal assigned at the next-highest level:
        for (int i = 2; i < out_learnt.size(); i++)
            if (level(var(out_learnt[i])) > level(var(out_learnt[max_i])))
                max_i = i;
        // Swap-in this literal at index 1:
        Lit p             = out_learnt[max_i];
        out_learnt[max_i] = out_learnt[1];
        out_learnt[1]     = p;
        out_btlevel       = level(var(p));
    }

    for (j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;    // ('seen[]' is now cleared)
}

void Solver::analyzeFinal ( Lit  p, vec< Lit > &  out_conflict  )

protected

Definition at line 399 of file Solver.cpp.

{
    out_conflict.clear();
    out_conflict.push(p);

    if (decisionLevel() == 0)
        return;

    seen[var(p)] = 1;

    for (int i = trail.size()-1; i >= trail_lim[0]; i--){
        Var x = var(trail[i]);
        if (seen[x]){
            if (reason(x) == CRef_Undef){
                assert(level(x) > 0);
                out_conflict.push(~trail[i]);
            }else{
                Clause& c = ca[reason(x)];
                for (int j = 1; j < c.size(); j++)
                    if (level(var(c[j])) > 0)
                        seen[var(c[j])] = 1;
            }
            seen[x] = 0;
        }
    }

    seen[var(p)] = 0;
}

void Solver::attachClause ( CRef  cr )

protected

Definition at line 162 of file Solver.cpp.

                                 {
    const Clause& c = ca[cr];
    assert(c.size() > 1);
    watches[~c[0]].push(Watcher(cr, c[1]));
    watches[~c[1]].push(Watcher(cr, c[0]));
    if (c.learnt()) learnts_literals += c.size();
    else            clauses_literals += c.size(); }

void Minisat::Solver::budgetOff ( )

inline

Definition at line 343 of file Solver.h.

{ conflict_budget = propagation_budget = -1; }

void Solver::cancelUntil ( int  level )

protected

Definition at line 207 of file Solver.cpp.

                                  {
    if (decisionLevel() > level){
        for (int c = trail.size()-1; c >= trail_lim[level]; c--){
            Var      x  = var(trail[c]);
            assigns [x] = l_Undef;
            if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
                polarity[x] = sign(trail[c]);
            insertVarOrder(x); }
        qhead = trail_lim[level];
        trail.shrink(trail.size() - trail_lim[level]);
        trail_lim.shrink(trail_lim.size() - level);
    } }

void Minisat::Solver::checkGarbage ( double  gf )

inline

Definition at line 305 of file Solver.h.

                                         {
    if (ca.wasted() > ca.size() * gf)
        garbageCollect(); }

void Minisat::Solver::checkGarbage ( void  )

inline

Definition at line 304 of file Solver.h.

{ checkGarbage(garbage_frac); }

void Minisat::Solver::claBumpActivity ( Clause &  c )

inlineprotected

Definition at line 297 of file Solver.h.

                                              {
        if ( (c.activity() += cla_inc) > 1e20 ) {
            // Rescale:
            for (int i = 0; i < learnts.size(); i++)
                ca[learnts[i]].activity() *= (float)1e-20;
            cla_inc *= 1e-20; } }

void Minisat::Solver::claDecayActivity ( )

inlineprotected

Definition at line 296 of file Solver.h.

{ cla_inc *= (1 / clause_decay); }

void Minisat::Solver::clearInterrupt ( )

inline

Definition at line 342 of file Solver.h.

{ asynch_interrupt = false; }

int Minisat::Solver::decisionLevel ( ) const

inlineprotected

Definition at line 319 of file Solver.h.

{ return trail_lim.size(); }

void Solver::detachClause ( CRef  cr, bool  strict = false  )

protected

Definition at line 171 of file Solver.cpp.

                                              {
    const Clause& c = ca[cr];
    assert(c.size() > 1);
    
    if (strict){
        remove(watches[~c[0]], Watcher(cr, c[1]));
        remove(watches[~c[1]], Watcher(cr, c[0]));
    }else{
        // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause)
        watches.smudge(~c[0]);
        watches.smudge(~c[1]);
    }

    if (c.learnt()) learnts_literals -= c.size();
    else            clauses_literals -= c.size(); }

static double Minisat::Solver::drand ( double &  seed )

inlinestaticprotected

Definition at line 262 of file Solver.h.

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

bool Minisat::Solver::enqueue ( Lit  p, CRef  from = CRef_Undef  )

inlineprotected

Definition at line 310 of file Solver.h.

{ return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }

void Solver::garbageCollect ( )

virtual

Reimplemented in Minisat::SimpSolver.

Definition at line 913 of file Solver.cpp.

{
    // Initialize the next region to a size corresponding to the estimated utilization degree. This
    // is not precise but should avoid some unnecessary reallocations for the new region:
    ClauseAllocator to(ca.size() - ca.wasted()); 

    relocAll(to);
    if (verbosity >= 2)
        printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n", 
               ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
    to.moveTo(ca);
}

void Minisat::Solver::insertVarOrder ( Var  x )

inlineprotected

Definition at line 280 of file Solver.h.

                                        {
    if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }

void Minisat::Solver::interrupt ( )

inline

Definition at line 341 of file Solver.h.

{ asynch_interrupt = true; }

static int Minisat::Solver::irand ( double &  seed, int  size  )

inlinestaticprotected

Definition at line 269 of file Solver.h.

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

int Minisat::Solver::level ( Var  x ) const

inlineprotected

Definition at line 278 of file Solver.h.

{ return vardata[x].level; }

bool Solver::litRedundant ( Lit  p, uint32_t  abstract_levels  )

protected

Definition at line 361 of file Solver.cpp.

{
    analyze_stack.clear(); analyze_stack.push(p);
    int top = analyze_toclear.size();
    while (analyze_stack.size() > 0){
        assert(reason(var(analyze_stack.last())) != CRef_Undef);
        Clause& c = ca[reason(var(analyze_stack.last()))]; analyze_stack.pop();

        for (int i = 1; i < c.size(); i++){
            Lit p  = c[i];
            if (!seen[var(p)] && level(var(p)) > 0){
                if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){
                    seen[var(p)] = 1;
                    analyze_stack.push(p);
                    analyze_toclear.push(p);
                }else{
                    for (int j = top; j < analyze_toclear.size(); j++)
                        seen[var(analyze_toclear[j])] = 0;
                    analyze_toclear.shrink(analyze_toclear.size() - top);
                    return false;
                }
            }
        }
    }

    return true;
}

bool Minisat::Solver::locked ( const Clause &  c ) const

inlineprotected

Definition at line 316 of file Solver.h.

{ return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; }

static VarData Minisat::Solver::mkVarData ( CRef  cr, int  l  )

inlinestaticprotected

Definition at line 146 of file Solver.h.

{ VarData d = {cr, l}; return d; }

lbool Minisat::Solver::modelValue ( Var  x ) const

inline

Definition at line 323 of file Solver.h.

{ return model[x]; }

lbool Minisat::Solver::modelValue ( Lit  p ) const

inline

Definition at line 324 of file Solver.h.

{ return model[var(p)] ^ sign(p); }

int Minisat::Solver::nAssigns ( ) const

inline

Definition at line 325 of file Solver.h.

{ return trail.size(); }

int Minisat::Solver::nClauses ( ) const

inline

Definition at line 326 of file Solver.h.

{ return clauses.size(); }

void Minisat::Solver::newDecisionLevel ( )

inlineprotected

Definition at line 317 of file Solver.h.

{ trail_lim.push(trail.size()); }

Var Solver::newVar	(	bool	polarity = true,
		bool	dvar = true
	)

Definition at line 114 of file Solver.cpp.

{
    int v = nVars();
    watches  .init(mkLit(v, false));
    watches  .init(mkLit(v, true ));
    assigns  .push(l_Undef);
    vardata  .push(mkVarData(CRef_Undef, 0));
    //activity .push(0);
    activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
    seen     .push(0);
    polarity .push(sign);
    decision .push();
    trail    .capacity(v+1);
    setDecisionVar(v, dvar);
    return v;
}

int Minisat::Solver::nFreeVars ( ) const

inline

Definition at line 329 of file Solver.h.

{ return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }

int Minisat::Solver::nLearnts ( ) const

inline

Definition at line 327 of file Solver.h.

{ return learnts.size(); }

int Minisat::Solver::nVars ( ) const

inline

Definition at line 328 of file Solver.h.

{ return vardata.size(); }

bool Minisat::Solver::okay ( ) const

inline

Definition at line 358 of file Solver.h.

{ return ok; }

Lit Solver::pickBranchLit ( )

protected

Definition at line 225 of file Solver.cpp.

{
    Var next = var_Undef;

    // Random decision:
    if (drand(random_seed) < random_var_freq && !order_heap.empty()){
        next = order_heap[irand(random_seed,order_heap.size())];
        if (value(next) == l_Undef && decision[next])
            rnd_decisions++; }

    // Activity based decision:
    while (next == var_Undef || value(next) != l_Undef || !decision[next])
        if (order_heap.empty()){
            next = var_Undef;
            break;
        }else
            next = order_heap.removeMin();

    return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]);
}

double Solver::progressEstimate ( ) const

protected

Definition at line 708 of file Solver.cpp.

{
    double  progress = 0;
    double  F = 1.0 / nVars();

    for (int i = 0; i <= decisionLevel(); i++){
        int beg = i == 0 ? 0 : trail_lim[i - 1];
        int end = i == decisionLevel() ? trail.size() : trail_lim[i];
        progress += pow(F, i) * (end - beg);
    }

    return progress / nVars();
}

CRef Solver::propagate ( )

protected

Definition at line 449 of file Solver.cpp.

{
    CRef    confl     = CRef_Undef;
    int     num_props = 0;
    watches.cleanAll();

    while (qhead < trail.size()){
        Lit            p   = trail[qhead++];     // 'p' is enqueued fact to propagate.
        vec<Watcher>&  ws  = watches[p];
        Watcher        *i, *j, *end;
        num_props++;

        for (i = j = (Watcher*)ws, end = i + ws.size();  i != end;){
            // Try to avoid inspecting the clause:
            Lit blocker = i->blocker;
            if (value(blocker) == l_True){
                *j++ = *i++; continue; }

            // Make sure the false literal is data[1]:
            CRef     cr        = i->cref;
            Clause&  c         = ca[cr];
            Lit      false_lit = ~p;
            if (c[0] == false_lit)
                c[0] = c[1], c[1] = false_lit;
            assert(c[1] == false_lit);
            i++;

            // If 0th watch is true, then clause is already satisfied.
            Lit     first = c[0];
            Watcher w     = Watcher(cr, first);
            if (first != blocker && value(first) == l_True){
                *j++ = w; continue; }

            // Look for new watch:
            for (int k = 2; k < c.size(); k++)
                if (value(c[k]) != l_False){
                    c[1] = c[k]; c[k] = false_lit;
                    watches[~c[1]].push(w);
                    goto NextClause; }

            // Did not find watch -- clause is unit under assignment:
            *j++ = w;
            if (value(first) == l_False){
                confl = cr;
                qhead = trail.size();
                // Copy the remaining watches:
                while (i < end)
                    *j++ = *i++;
            }else
                uncheckedEnqueue(first, cr);

        NextClause:;
        }
        ws.shrink(i - j);
    }
    propagations += num_props;
    simpDB_props -= num_props;

    return confl;
}

CRef Minisat::Solver::reason ( Var  x ) const

inlineprotected

Definition at line 277 of file Solver.h.

{ return vardata[x].reason; }

void Solver::rebuildOrderHeap ( )

protected

Definition at line 559 of file Solver.cpp.

{
    vec<Var> vs;
    for (Var v = 0; v < nVars(); v++)
        if (decision[v] && value(v) == l_Undef)
            vs.push(v);
    order_heap.build(vs);
}

void Solver::reduceDB ( )

protected

Definition at line 525 of file Solver.cpp.

{
    int     i, j;
    double  extra_lim = cla_inc / learnts.size();    // Remove any clause below this activity

    sort(learnts, reduceDB_lt(ca));
    // Don't delete binary or locked clauses. From the rest, delete clauses from the first half
    // and clauses with activity smaller than 'extra_lim':
    for (i = j = 0; i < learnts.size(); i++){
        Clause& c = ca[learnts[i]];
        if (c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim))
            removeClause(learnts[i]);
        else
            learnts[j++] = learnts[i];
    }
    learnts.shrink(i - j);
    checkGarbage();
}

void Solver::relocAll ( ClauseAllocator &  to )

protected

Definition at line 876 of file Solver.cpp.

{
    // All watchers:
    //
    // for (int i = 0; i < watches.size(); i++)
    watches.cleanAll();
    for (int v = 0; v < nVars(); v++)
        for (int s = 0; s < 2; s++){
            Lit p = mkLit(v, s);
            // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
            vec<Watcher>& ws = watches[p];
            for (int j = 0; j < ws.size(); j++)
                ca.reloc(ws[j].cref, to);
        }

    // All reasons:
    //
    int i;
    for (i = 0; i < trail.size(); i++){
        Var v = var(trail[i]);

        if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
            ca.reloc(vardata[v].reason, to);
    }

    // All learnt:
    //
    for (i = 0; i < learnts.size(); i++)
        ca.reloc(learnts[i], to);

    // All original:
    //
    for (i = 0; i < clauses.size(); i++)
        ca.reloc(clauses[i], to);
}

void Solver::removeClause ( CRef  cr )

protected

Definition at line 188 of file Solver.cpp.

                                 {
    Clause& c = ca[cr];
    detachClause(cr);
    // Don't leave pointers to free'd memory!
    if (locked(c)) vardata[var(c[0])].reason = CRef_Undef;
    c.mark(1); 
    ca._free(cr);
}

void Solver::removeSatisfied ( vec< CRef > &  cs )

protected

Definition at line 545 of file Solver.cpp.

{
    int i, j;
    for (i = j = 0; i < cs.size(); i++){
        Clause& c = ca[cs[i]];
        if (satisfied(c))
            removeClause(cs[i]);
        else
            cs[j++] = cs[i];
    }
    cs.shrink(i - j);
}

bool Solver::satisfied ( const Clause &  c ) const

protected

Definition at line 198 of file Solver.cpp.

                                            {
    for (int i = 0; i < c.size(); i++)
        if (value(c[i]) == l_True)
            return true;
    return false; }

lbool Solver::search ( int  nof_conflicts )

protected

Definition at line 614 of file Solver.cpp.

{
    assert(ok);
    int         backtrack_level;
    int         conflictC = 0;
    vec<Lit>    learnt_clause;
    starts++;

    for (;;){
        CRef confl = propagate();
        if (confl != CRef_Undef){
            // CONFLICT
            conflicts++; conflictC++;
            if (decisionLevel() == 0) return l_False;

            learnt_clause.clear();
            analyze(confl, learnt_clause, backtrack_level);
            cancelUntil(backtrack_level);

            if (learnt_clause.size() == 1){
                uncheckedEnqueue(learnt_clause[0]);
            }else{
                CRef cr = ca.alloc(learnt_clause, true);
                learnts.push(cr);
                attachClause(cr);
                claBumpActivity(ca[cr]);
                uncheckedEnqueue(learnt_clause[0], cr);
            }

            varDecayActivity();
            claDecayActivity();

            if (--learntsize_adjust_cnt == 0){
                learntsize_adjust_confl *= learntsize_adjust_inc;
                learntsize_adjust_cnt    = (int)learntsize_adjust_confl;
                max_learnts             *= learntsize_inc;

                if (verbosity >= 1)
                    printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", 
                           (int)conflicts, 
                           (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, 
                           (int)max_learnts, nLearnts(), ((double)((int64_t)learnts_literals))/nLearnts(), progressEstimate()*100);
            }

        }else{
            // NO CONFLICT
            if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){
                // Reached bound on number of conflicts:
                progress_estimate = progressEstimate();
                cancelUntil(0);
                return l_Undef; }

            // Simplify the set of problem clauses:
            if (decisionLevel() == 0 && !simplify())
                return l_False;

            if (learnts.size()-nAssigns() >= max_learnts)
                // Reduce the set of learnt clauses:
                reduceDB();

            Lit next = lit_Undef;
            while (decisionLevel() < assumptions.size()){
                // Perform user provided assumption:
                Lit p = assumptions[decisionLevel()];
                if (value(p) == l_True){
                    // Dummy decision level:
                    newDecisionLevel();
                }else if (value(p) == l_False){
                    analyzeFinal(~p, conflict);
                    return l_False;
                }else{
                    next = p;
                    break;
                }
            }

            if (next == lit_Undef){
                // New variable decision:
                decisions++;
                next = pickBranchLit();

                if (next == lit_Undef)
                    // Model found:
                    return l_True;
            }

            // Increase decision level and enqueue 'next'
            newDecisionLevel();
            uncheckedEnqueue(next);
        }
    }
}

void Minisat::Solver::setConfBudget ( int64_t  x )

inline

Definition at line 339 of file Solver.h.

{ conflict_budget    = conflicts    + x; }

void Minisat::Solver::setDecisionVar ( Var  v, bool  b  )

inline

Definition at line 331 of file Solver.h.

{ 
    if      ( b && !decision[v]) dec_vars++;
    else if (!b &&  decision[v]) dec_vars--;

    decision[v] = b;
    insertVarOrder(v);
}

void Minisat::Solver::setPolarity ( Var  v, bool  b  )

inline

Definition at line 330 of file Solver.h.

{ polarity[v] = b; }

void Minisat::Solver::setPropBudget ( int64_t  x )

inline

Definition at line 340 of file Solver.h.

{ propagation_budget = propagations + x; }

bool Solver::simplify

(

)

Definition at line 577 of file Solver.cpp.

{
    assert(decisionLevel() == 0);

    if (!ok || propagate() != CRef_Undef)
        return ok = false;

    if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
        return true;

    // Remove satisfied clauses:
    removeSatisfied(learnts);
    if (remove_satisfied)        // Can be turned off.
        removeSatisfied(clauses);
    checkGarbage();
    rebuildOrderHeap();

    simpDB_assigns = nAssigns();
    simpDB_props   = clauses_literals + learnts_literals;   // (shouldn't depend on stats really, but it will do for now)

    return true;
}

bool Minisat::Solver::solve ( const vec< Lit > &  assumps )

inline

Definition at line 356 of file Solver.h.

{ budgetOff(); assumps.copyTo(assumptions); return solve_() == l_True; }

bool Minisat::Solver::solve ( )

inline

Definition at line 352 of file Solver.h.

{ budgetOff(); assumptions.clear(); return solve_() == l_True; }

bool Minisat::Solver::solve ( Lit  p )

inline

Definition at line 353 of file Solver.h.

{ budgetOff(); assumptions.clear(); assumptions.push(p); return solve_() == l_True; }

bool Minisat::Solver::solve ( Lit  p, Lit  q  )

inline

Definition at line 354 of file Solver.h.

{ budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; }

bool Minisat::Solver::solve ( Lit  p, Lit  q, Lit  r  )

inline

Definition at line 355 of file Solver.h.

{ budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_() == l_True; }

lbool Solver::solve_ ( )

protected

Definition at line 751 of file Solver.cpp.

{
    model.clear();
    conflict.clear();
    if (!ok) return l_False;

    solves++;

    max_learnts               = nClauses() * learntsize_factor;
    learntsize_adjust_confl   = learntsize_adjust_start_confl;
    learntsize_adjust_cnt     = (int)learntsize_adjust_confl;
    lbool   status            = l_Undef;

    if (verbosity >= 1){
        printf("============================[ Search Statistics ]==============================\n");
        printf("| Conflicts |          ORIGINAL         |          LEARNT          | Progress |\n");
        printf("|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |\n");
        printf("===============================================================================\n");
    }

    // Search:
    int curr_restarts = 0;
    while (status == l_Undef){
        double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts);
        status = search(rest_base * restart_first);
        if (!withinBudget()) break;
        curr_restarts++;
    }

    if (verbosity >= 1)
        printf("===============================================================================\n");


    if (status == l_True){
        // Extend & copy model:
        model.growTo(nVars());
        for (int i = 0; i < nVars(); i++) model[i] = value(i);
    }else if (status == l_False && conflict.size() == 0)
        ok = false;

    cancelUntil(0);
    return status;
}

lbool Minisat::Solver::solveLimited ( const vec< Lit > &  assumps )

inline

Definition at line 357 of file Solver.h.

{ assumps.copyTo(assumptions); return solve_(); }

void Solver::toDimacs	(	FILE *	f,
		const vec< Lit > &	assumps
	)

Definition at line 831 of file Solver.cpp.

{
    // Handle case when solver is in contradictory state:
    if (!ok){
        fprintf(f, "p cnf 1 2\n1 0\n-1 0\n");
        return; }

    vec<Var> map; Var max = 0;

    // Cannot use removeClauses here because it is not safe
    // to deallocate them at this point. Could be improved.
    int i, cnt = 0;
    for (i = 0; i < clauses.size(); i++)
        if (!satisfied(ca[clauses[i]]))
            cnt++;
        
    for (i = 0; i < clauses.size(); i++)
        if (!satisfied(ca[clauses[i]])){
            Clause& c = ca[clauses[i]];
            for (int j = 0; j < c.size(); j++)
                if (value(c[j]) != l_False)
                    mapVar(var(c[j]), map, max);
        }

    // Assumptions are added as unit clauses:
    cnt += assumptions.size();

    fprintf(f, "p cnf %d %d\n", max, cnt);

    for (i = 0; i < assumptions.size(); i++){
        assert(value(assumptions[i]) != l_False);
        fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max)+1);
    }

    for (i = 0; i < clauses.size(); i++)
        toDimacs(f, ca[clauses[i]], map, max);

    if (verbosity > 0)
        printf("Wrote %d clauses with %d variables.\n", cnt, max);
}

void Solver::toDimacs	(	const char *	file,
		const vec< Lit > &	assumps
	)

Definition at line 821 of file Solver.cpp.

{
    FILE* f = fopen(file, "wr");
    if (f == NULL)
        fprintf(stderr, "could not open file %s\n", file), exit(1);
    toDimacs(f, assumps);
    fclose(f);
}

void Solver::toDimacs	(	FILE *	f,
		Clause &	c,
		vec< Var > &	map,
		Var &	max
	)

Definition at line 810 of file Solver.cpp.

{
    if (satisfied(c)) return;

    for (int i = 0; i < c.size(); i++)
        if (value(c[i]) != l_False)
            fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max)+1);
    fprintf(f, "0\n");
}

void Minisat::Solver::toDimacs ( const char *  file )

inline

Definition at line 360 of file Solver.h.

{ vec<Lit> as; toDimacs(file, as); }

void Minisat::Solver::toDimacs ( const char *  file, Lit  p  )

inline

Definition at line 361 of file Solver.h.

{ vec<Lit> as; as.push(p); toDimacs(file, as); }

void Minisat::Solver::toDimacs ( const char *  file, Lit  p, Lit  q  )

inline

Definition at line 362 of file Solver.h.

{ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }

void Minisat::Solver::toDimacs ( const char *  file, Lit  p, Lit  q, Lit  r  )

inline

Definition at line 363 of file Solver.h.

{ vec<Lit> as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); }

void Solver::uncheckedEnqueue ( Lit  p, CRef  from = CRef_Undef  )

protected

Definition at line 429 of file Solver.cpp.

{
    assert(value(p) == l_Undef);
    assigns[var(p)] = lbool(!sign(p));
    vardata[var(p)] = mkVarData(from, decisionLevel());
    trail.push_(p);
}

lbool Minisat::Solver::value ( Var  x ) const

inline

Definition at line 321 of file Solver.h.

{ return assigns[x]; }

lbool Minisat::Solver::value ( Lit  p ) const

inline

Definition at line 322 of file Solver.h.

{ return assigns[var(p)] ^ sign(p); }

void Minisat::Solver::varBumpActivity ( Var  v, double  inc  )

inlineprotected

Definition at line 285 of file Solver.h.

                                                     {
    if ( (activity[v] += inc) > 1e100 ) {
        // Rescale:
        for (int i = 0; i < nVars(); i++)
            activity[i] *= 1e-100;
        var_inc *= 1e-100; }

    // Update order_heap with respect to new activity:
    if (order_heap.inHeap(v))
        order_heap.decrease(v); }

void Minisat::Solver::varBumpActivity ( Var  v )

inlineprotected

Definition at line 284 of file Solver.h.

{ varBumpActivity(v, var_inc); }

void Minisat::Solver::varDecayActivity ( )

inlineprotected

Definition at line 283 of file Solver.h.

{ var_inc *= (1 / var_decay); }

bool Minisat::Solver::withinBudget ( ) const

inlineprotected

Definition at line 344 of file Solver.h.

                                           {
    return !asynch_interrupt &&
           (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&
           (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }

Field Documentation

vec<double> Minisat::Solver::activity

protected

Definition at line 175 of file Solver.h.

vec<Lit> Minisat::Solver::add_tmp

protected

Definition at line 201 of file Solver.h.

vec<Lit> Minisat::Solver::analyze_stack

protected

Definition at line 199 of file Solver.h.

vec<Lit> Minisat::Solver::analyze_toclear

protected

Definition at line 200 of file Solver.h.

vec<lbool> Minisat::Solver::assigns

protected

Definition at line 179 of file Solver.h.

vec<Lit> Minisat::Solver::assumptions

protected

Definition at line 188 of file Solver.h.

bool Minisat::Solver::asynch_interrupt

protected

Definition at line 211 of file Solver.h.

ClauseAllocator Minisat::Solver::ca

protected

Definition at line 193 of file Solver.h.

int Minisat::Solver::ccmin_mode

Definition at line 122 of file Solver.h.

double Minisat::Solver::cla_inc

protected

Definition at line 174 of file Solver.h.

double Minisat::Solver::clause_decay

Definition at line 118 of file Solver.h.

vec<CRef> Minisat::Solver::clauses

protected

Definition at line 172 of file Solver.h.

uint64_t Minisat::Solver::clauses_literals

Definition at line 139 of file Solver.h.

vec<Lit> Minisat::Solver::conflict

Definition at line 111 of file Solver.h.

int64_t Minisat::Solver::conflict_budget

protected

Definition at line 209 of file Solver.h.

uint64_t Minisat::Solver::conflicts

Definition at line 138 of file Solver.h.

uint64_t Minisat::Solver::dec_vars

Definition at line 139 of file Solver.h.

vec<char> Minisat::Solver::decision

protected

Definition at line 181 of file Solver.h.

uint64_t Minisat::Solver::decisions

Definition at line 138 of file Solver.h.

double Minisat::Solver::garbage_frac

Definition at line 126 of file Solver.h.

vec<CRef> Minisat::Solver::learnts

protected

Definition at line 173 of file Solver.h.

uint64_t Minisat::Solver::learnts_literals

Definition at line 139 of file Solver.h.

int Minisat::Solver::learntsize_adjust_cnt

protected

Definition at line 205 of file Solver.h.

double Minisat::Solver::learntsize_adjust_confl

protected

Definition at line 204 of file Solver.h.

double Minisat::Solver::learntsize_adjust_inc

Definition at line 134 of file Solver.h.

int Minisat::Solver::learntsize_adjust_start_confl

Definition at line 133 of file Solver.h.

double Minisat::Solver::learntsize_factor

Definition at line 130 of file Solver.h.

double Minisat::Solver::learntsize_inc

Definition at line 131 of file Solver.h.

bool Minisat::Solver::luby_restart

Definition at line 121 of file Solver.h.

double Minisat::Solver::max_learnts

protected

Definition at line 203 of file Solver.h.

uint64_t Minisat::Solver::max_literals

Definition at line 139 of file Solver.h.

vec<lbool> Minisat::Solver::model

Definition at line 110 of file Solver.h.

bool Minisat::Solver::ok

protected

Definition at line 171 of file Solver.h.

Heap<VarOrderLt> Minisat::Solver::order_heap

protected

Definition at line 189 of file Solver.h.

int Minisat::Solver::phase_saving

Definition at line 123 of file Solver.h.

vec<char> Minisat::Solver::polarity

protected

Definition at line 180 of file Solver.h.

double Minisat::Solver::progress_estimate

protected

Definition at line 190 of file Solver.h.

int64_t Minisat::Solver::propagation_budget

protected

Definition at line 210 of file Solver.h.

uint64_t Minisat::Solver::propagations

Definition at line 138 of file Solver.h.

int Minisat::Solver::qhead

protected

Definition at line 185 of file Solver.h.

double Minisat::Solver::random_seed

Definition at line 120 of file Solver.h.

double Minisat::Solver::random_var_freq

Definition at line 119 of file Solver.h.

bool Minisat::Solver::remove_satisfied

protected

Definition at line 191 of file Solver.h.

int Minisat::Solver::restart_first

Definition at line 128 of file Solver.h.

double Minisat::Solver::restart_inc

Definition at line 129 of file Solver.h.

uint64_t Minisat::Solver::rnd_decisions

Definition at line 138 of file Solver.h.

bool Minisat::Solver::rnd_init_act

Definition at line 125 of file Solver.h.

bool Minisat::Solver::rnd_pol

Definition at line 124 of file Solver.h.

vec<char> Minisat::Solver::seen

protected

Definition at line 198 of file Solver.h.

int Minisat::Solver::simpDB_assigns

protected

Definition at line 186 of file Solver.h.

int64_t Minisat::Solver::simpDB_props

protected

Definition at line 187 of file Solver.h.

uint64_t Minisat::Solver::solves

Definition at line 138 of file Solver.h.

uint64_t Minisat::Solver::starts

Definition at line 138 of file Solver.h.

uint64_t Minisat::Solver::tot_literals

Definition at line 139 of file Solver.h.

vec<Lit> Minisat::Solver::trail

protected

Definition at line 182 of file Solver.h.

vec<int> Minisat::Solver::trail_lim

protected

Definition at line 183 of file Solver.h.

double Minisat::Solver::var_decay

Definition at line 117 of file Solver.h.

double Minisat::Solver::var_inc

protected

Definition at line 176 of file Solver.h.

vec<VarData> Minisat::Solver::vardata

protected

Definition at line 184 of file Solver.h.

int Minisat::Solver::verbosity

Definition at line 116 of file Solver.h.

OccLists<Lit, vec<Watcher>, WatcherDeleted> Minisat::Solver::watches

protected

Definition at line 178 of file Solver.h.

---

The documentation for this class was generated from the following files:

• Solver.h
• Solver.cpp