#include <Solver.h>

Inheritance diagram for Minisat::Solver:

Collaboration diagram for Minisat::Solver:

[legend]

Classes
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 ()

Public Attributes
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 37 of file Solver.h.

Constructor & Destructor Documentation

◆ Solver()

Solver::Solver ( )

Definition at line 53 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::~Solver ( )

virtual

Definition at line 104 of file Solver.cpp.

105{

106}

Member Function Documentation

◆ abstractLevel()

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

inlineprotected

Definition at line 321 of file Solver.h.

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

Minisat::Solver::level

int level(Var x) const

Definition Solver.h:279

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addClause() [1/4]

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

inline

Definition at line 312 of file Solver.h.

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

Minisat::Solver::addClause_

bool addClause_(vec< Lit > &ps)

Definition Solver.cpp:134

Minisat::Solver::add_tmp

vec< Lit > add_tmp

Definition Solver.h:202

Here is the call graph for this function:

◆ addClause() [2/4]

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

inline

Definition at line 314 of file Solver.h.

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

p

Cube * p

Definition exorList.c:222

Here is the call graph for this function:

◆ addClause() [3/4]

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

inline

Definition at line 315 of file Solver.h.

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

Here is the call graph for this function:

◆ addClause() [4/4]

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

inline

Definition at line 316 of file Solver.h.

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

Here is the call graph for this function:

◆ addClause_()

bool Solver::addClause_ ( vec< Lit > & ps )

Definition at line 134 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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addEmptyClause()

bool Minisat::Solver::addEmptyClause ( )

inline

Definition at line 313 of file Solver.h.

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

Here is the call graph for this function:

◆ analyze()

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

protected

Definition at line 266 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)
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ analyzeFinal()

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

protected

Definition at line 401 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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ attachClause()

void Solver::attachClause ( CRef cr )

protected

Definition at line 164 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(); }

Here is the caller graph for this function:

◆ budgetOff()

void Minisat::Solver::budgetOff ( )

inline

Definition at line 344 of file Solver.h.

344{ conflict_budget = propagation_budget = -1; }

Here is the caller graph for this function:

◆ cancelUntil()

void Solver::cancelUntil ( int level )

protected

Definition at line 209 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);
    } }

Here is the call graph for this function:

Here is the caller graph for this function:

◆ checkGarbage() [1/2]

void Minisat::Solver::checkGarbage ( void )

inline

Definition at line 305 of file Solver.h.

305{ checkGarbage(garbage_frac); }

Minisat::Solver::checkGarbage

void checkGarbage()

Definition Solver.h:305

Here is the call graph for this function:

Here is the caller graph for this function:

◆ checkGarbage() [2/2]

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

inline

Definition at line 306 of file Solver.h.

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

Here is the call graph for this function:

◆ claBumpActivity()

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

inlineprotected

Definition at line 298 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; } }

Here is the call graph for this function:

Here is the caller graph for this function:

◆ claDecayActivity()

void Minisat::Solver::claDecayActivity ( )

inlineprotected

Definition at line 297 of file Solver.h.

297{ cla_inc *= (1 / clause_decay); }

Here is the caller graph for this function:

◆ clearInterrupt()

void Minisat::Solver::clearInterrupt ( )

inline

Definition at line 343 of file Solver.h.

343{ asynch_interrupt = false; }

◆ decisionLevel()

int Minisat::Solver::decisionLevel ( ) const

inlineprotected

Definition at line 320 of file Solver.h.

320{ return trail_lim.size(); }

Here is the caller graph for this function:

◆ detachClause()

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

protected

Definition at line 173 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(); }

Here is the caller graph for this function:

◆ drand()

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

inlinestaticprotected

Definition at line 263 of file Solver.h.

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

Here is the caller graph for this function:

◆ enqueue()

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

inlineprotected

Definition at line 311 of file Solver.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ garbageCollect()

void Solver::garbageCollect ( )

virtual

Reimplemented in Minisat::SimpSolver.

Definition at line 915 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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ insertVarOrder()

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

inlineprotected

Definition at line 281 of file Solver.h.

281 {

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

Minisat::Solver::decision

vec< char > decision

Definition Solver.h:182

Here is the caller graph for this function:

◆ interrupt()

void Minisat::Solver::interrupt ( )

inline

Definition at line 342 of file Solver.h.

342{ asynch_interrupt = true; }

◆ irand()

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

inlinestaticprotected

Definition at line 270 of file Solver.h.

270 {

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

Minisat::Solver::drand

static double drand(double &seed)

Definition Solver.h:263

NewBdd::size

unsigned long long size

Definition giaNewBdd.h:39

Here is the call graph for this function:

Here is the caller graph for this function:

◆ level()

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

inlineprotected

Definition at line 279 of file Solver.h.

279{ return vardata[x].level; }

Minisat::Solver::vardata

vec< VarData > vardata

Definition Solver.h:185

Here is the caller graph for this function:

◆ litRedundant()

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

protected

Definition at line 363 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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ locked()

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

inlineprotected

Definition at line 317 of file Solver.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ mkVarData()

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

inlinestaticprotected

Definition at line 147 of file Solver.h.

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

Minisat::Solver::VarData

Definition Solver.h:146

Here is the caller graph for this function:

◆ modelValue() [1/2]

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

inline

Definition at line 325 of file Solver.h.

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

Minisat::Solver::model

vec< lbool > model

Definition Solver.h:111

Here is the call graph for this function:

◆ modelValue() [2/2]

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

inline

Definition at line 324 of file Solver.h.

324{ return model[x]; }

Here is the caller graph for this function:

◆ nAssigns()

int Minisat::Solver::nAssigns ( ) const

inline

Definition at line 326 of file Solver.h.

326{ return trail.size(); }

Here is the caller graph for this function:

◆ nClauses()

int Minisat::Solver::nClauses ( ) const

inline

Definition at line 327 of file Solver.h.

327{ return clauses.size(); }

Here is the caller graph for this function:

◆ newDecisionLevel()

void Minisat::Solver::newDecisionLevel ( )

inlineprotected

Definition at line 318 of file Solver.h.

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

Here is the caller graph for this function:

◆ newVar()

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

Definition at line 116 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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ nFreeVars()

int Minisat::Solver::nFreeVars ( ) const

inline

Definition at line 330 of file Solver.h.

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

◆ nLearnts()

int Minisat::Solver::nLearnts ( ) const

inline

Definition at line 328 of file Solver.h.

328{ return learnts.size(); }

Here is the caller graph for this function:

◆ nVars()

int Minisat::Solver::nVars ( ) const

inline

Definition at line 329 of file Solver.h.

329{ return vardata.size(); }

Here is the caller graph for this function:

◆ okay()

bool Minisat::Solver::okay ( ) const

inline

Definition at line 359 of file Solver.h.

359{ return ok; }

◆ pickBranchLit()

Lit Solver::pickBranchLit ( )

protected

Definition at line 227 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]);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ progressEstimate()

double Solver::progressEstimate ( ) const

protected

Definition at line 710 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();
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ propagate()

CRef Solver::propagate ( )

protected

Definition at line 451 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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ reason()

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

inlineprotected

Definition at line 278 of file Solver.h.

278{ return vardata[x].reason; }

Here is the caller graph for this function:

◆ rebuildOrderHeap()

void Solver::rebuildOrderHeap ( )

protected

Definition at line 561 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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ reduceDB()

void Solver::reduceDB ( )

protected

Definition at line 527 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();
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ relocAll()

void Solver::relocAll ( ClauseAllocator & to )

protected

Definition at line 878 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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ removeClause()

void Solver::removeClause ( CRef cr )

protected

Definition at line 190 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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ removeSatisfied()

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

protected

Definition at line 547 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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ satisfied()

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

protected

Definition at line 200 of file Solver.cpp.

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

Here is the caller graph for this function:

◆ search()

lbool Solver::search ( int nof_conflicts )

protected

Definition at line 616 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);
        }
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setConfBudget()

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

inline

Definition at line 340 of file Solver.h.

340{ conflict_budget = conflicts + x; }

◆ setDecisionVar()

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

inline

Definition at line 332 of file Solver.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setPolarity()

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

inline

Definition at line 331 of file Solver.h.

331{ polarity[v] = b; }

◆ setPropBudget()

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

inline

Definition at line 341 of file Solver.h.

341{ propagation_budget = propagations + x; }

◆ simplify()

bool Solver::simplify ( )

Definition at line 579 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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ solve() [1/5]

bool Minisat::Solver::solve ( )

inline

Definition at line 353 of file Solver.h.

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

Minisat::Solver::budgetOff

void budgetOff()

Definition Solver.h:344

Minisat::Solver::solve_

lbool solve_()

Definition Solver.cpp:753

Here is the call graph for this function:

◆ solve() [2/5]

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

inline

Definition at line 357 of file Solver.h.

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

Here is the call graph for this function:

◆ solve() [3/5]

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

inline

Definition at line 354 of file Solver.h.

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

Here is the call graph for this function:

◆ solve() [4/5]

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

inline

Definition at line 355 of file Solver.h.

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

Here is the call graph for this function:

◆ solve() [5/5]

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

inline

Definition at line 356 of file Solver.h.

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

Here is the call graph for this function:

◆ solve_()

lbool Solver::solve_ ( )

protected

Definition at line 753 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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ solveLimited()

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

inline

Definition at line 358 of file Solver.h.

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

Here is the call graph for this function:

◆ toDimacs() [1/7]

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

inline

Definition at line 361 of file Solver.h.

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

Minisat::Solver::toDimacs

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

Definition Solver.cpp:833

file

struct file file

Definition file.h:21

Here is the call graph for this function:

◆ toDimacs() [2/7]

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

Definition at line 823 of file Solver.cpp.

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

Here is the call graph for this function:

◆ toDimacs() [3/7]

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

inline

Definition at line 362 of file Solver.h.

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

Here is the call graph for this function:

◆ toDimacs() [4/7]

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

inline

Definition at line 363 of file Solver.h.

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

Here is the call graph for this function:

◆ toDimacs() [5/7]

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

inline

Definition at line 364 of file Solver.h.

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

Here is the call graph for this function:

◆ toDimacs() [6/7]

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

Definition at line 812 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");
}

Here is the call graph for this function:

◆ toDimacs() [7/7]

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

Definition at line 833 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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ uncheckedEnqueue()

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

protected

Definition at line 431 of file Solver.cpp.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ value() [1/2]

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

inline

Definition at line 323 of file Solver.h.

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

Here is the call graph for this function:

◆ value() [2/2]

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

inline

Definition at line 322 of file Solver.h.

322{ return assigns[x]; }

Here is the caller graph for this function:

◆ varBumpActivity() [1/2]

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

inlineprotected

Definition at line 285 of file Solver.h.

285{ varBumpActivity(v, var_inc); }

Here is the call graph for this function:

◆ varBumpActivity() [2/2]

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

inlineprotected

Definition at line 286 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); }

Here is the call graph for this function:

Here is the caller graph for this function:

◆ varDecayActivity()

void Minisat::Solver::varDecayActivity ( )

inlineprotected

Definition at line 284 of file Solver.h.

284{ var_inc *= (1 / var_decay); }

Here is the caller graph for this function:

◆ withinBudget()

bool Minisat::Solver::withinBudget ( ) const

inlineprotected

Definition at line 345 of file Solver.h.

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

Here is the caller graph for this function:

Member Data Documentation

◆ activity

vec<double> Minisat::Solver::activity

protected

Definition at line 176 of file Solver.h.

◆ add_tmp

vec<Lit> Minisat::Solver::add_tmp

protected

Definition at line 202 of file Solver.h.

◆ analyze_stack

vec<Lit> Minisat::Solver::analyze_stack

protected

Definition at line 200 of file Solver.h.

◆ analyze_toclear

vec<Lit> Minisat::Solver::analyze_toclear

protected

Definition at line 201 of file Solver.h.

◆ assigns

vec<lbool> Minisat::Solver::assigns

protected

Definition at line 180 of file Solver.h.

◆ assumptions

vec<Lit> Minisat::Solver::assumptions

protected

Definition at line 189 of file Solver.h.

◆ asynch_interrupt

bool Minisat::Solver::asynch_interrupt

protected

Definition at line 212 of file Solver.h.

◆ ca

ClauseAllocator Minisat::Solver::ca

protected

Definition at line 194 of file Solver.h.

◆ ccmin_mode

int Minisat::Solver::ccmin_mode

Definition at line 123 of file Solver.h.

◆ cla_inc

double Minisat::Solver::cla_inc

protected

Definition at line 175 of file Solver.h.

◆ clause_decay

double Minisat::Solver::clause_decay

Definition at line 119 of file Solver.h.

◆ clauses

vec<CRef> Minisat::Solver::clauses

protected

Definition at line 173 of file Solver.h.

◆ clauses_literals

uint64_t Minisat::Solver::clauses_literals

Definition at line 140 of file Solver.h.

◆ conflict

vec<Lit> Minisat::Solver::conflict

Definition at line 112 of file Solver.h.

◆ conflict_budget

int64_t Minisat::Solver::conflict_budget

protected

Definition at line 210 of file Solver.h.

◆ conflicts

uint64_t Minisat::Solver::conflicts

Definition at line 139 of file Solver.h.

◆ dec_vars

uint64_t Minisat::Solver::dec_vars

Definition at line 140 of file Solver.h.

◆ decision

vec<char> Minisat::Solver::decision

protected

Definition at line 182 of file Solver.h.

◆ decisions

uint64_t Minisat::Solver::decisions

Definition at line 139 of file Solver.h.

◆ garbage_frac

double Minisat::Solver::garbage_frac

Definition at line 127 of file Solver.h.

◆ learnts

vec<CRef> Minisat::Solver::learnts

protected

Definition at line 174 of file Solver.h.

◆ learnts_literals

uint64_t Minisat::Solver::learnts_literals

Definition at line 140 of file Solver.h.

◆ learntsize_adjust_cnt

int Minisat::Solver::learntsize_adjust_cnt

protected

Definition at line 206 of file Solver.h.

◆ learntsize_adjust_confl

double Minisat::Solver::learntsize_adjust_confl

protected

Definition at line 205 of file Solver.h.

◆ learntsize_adjust_inc

double Minisat::Solver::learntsize_adjust_inc

Definition at line 135 of file Solver.h.

◆ learntsize_adjust_start_confl

int Minisat::Solver::learntsize_adjust_start_confl

Definition at line 134 of file Solver.h.

◆ learntsize_factor

double Minisat::Solver::learntsize_factor

Definition at line 131 of file Solver.h.

◆ learntsize_inc

double Minisat::Solver::learntsize_inc

Definition at line 132 of file Solver.h.

◆ luby_restart

bool Minisat::Solver::luby_restart

Definition at line 122 of file Solver.h.

◆ max_learnts

double Minisat::Solver::max_learnts

protected

Definition at line 204 of file Solver.h.

◆ max_literals

uint64_t Minisat::Solver::max_literals

Definition at line 140 of file Solver.h.

◆ model

vec<lbool> Minisat::Solver::model

Definition at line 111 of file Solver.h.

◆ ok

bool Minisat::Solver::ok

protected

Definition at line 172 of file Solver.h.

◆ order_heap

Heap<VarOrderLt> Minisat::Solver::order_heap

protected

Definition at line 190 of file Solver.h.

◆ phase_saving

int Minisat::Solver::phase_saving

Definition at line 124 of file Solver.h.

◆ polarity

vec<char> Minisat::Solver::polarity

protected

Definition at line 181 of file Solver.h.

◆ progress_estimate

double Minisat::Solver::progress_estimate

protected

Definition at line 191 of file Solver.h.

◆ propagation_budget

int64_t Minisat::Solver::propagation_budget

protected

Definition at line 211 of file Solver.h.

◆ propagations

uint64_t Minisat::Solver::propagations

Definition at line 139 of file Solver.h.

◆ qhead

int Minisat::Solver::qhead

protected

Definition at line 186 of file Solver.h.

◆ random_seed

double Minisat::Solver::random_seed

Definition at line 121 of file Solver.h.

◆ random_var_freq

double Minisat::Solver::random_var_freq

Definition at line 120 of file Solver.h.

◆ remove_satisfied

bool Minisat::Solver::remove_satisfied

protected

Definition at line 192 of file Solver.h.

◆ restart_first

int Minisat::Solver::restart_first

Definition at line 129 of file Solver.h.

◆ restart_inc

double Minisat::Solver::restart_inc

Definition at line 130 of file Solver.h.

◆ rnd_decisions

uint64_t Minisat::Solver::rnd_decisions

Definition at line 139 of file Solver.h.

◆ rnd_init_act

bool Minisat::Solver::rnd_init_act

Definition at line 126 of file Solver.h.

◆ rnd_pol

bool Minisat::Solver::rnd_pol

Definition at line 125 of file Solver.h.

◆ seen

vec<char> Minisat::Solver::seen

protected

Definition at line 199 of file Solver.h.

◆ simpDB_assigns

int Minisat::Solver::simpDB_assigns

protected

Definition at line 187 of file Solver.h.

◆ simpDB_props

int64_t Minisat::Solver::simpDB_props

protected

Definition at line 188 of file Solver.h.

◆ solves

uint64_t Minisat::Solver::solves

Definition at line 139 of file Solver.h.

◆ starts

uint64_t Minisat::Solver::starts

Definition at line 139 of file Solver.h.

◆ tot_literals

uint64_t Minisat::Solver::tot_literals

Definition at line 140 of file Solver.h.

◆ trail

vec<Lit> Minisat::Solver::trail

protected

Definition at line 183 of file Solver.h.

◆ trail_lim

vec<int> Minisat::Solver::trail_lim

protected

Definition at line 184 of file Solver.h.

◆ var_decay

double Minisat::Solver::var_decay

Definition at line 118 of file Solver.h.

◆ var_inc

double Minisat::Solver::var_inc

protected

Definition at line 177 of file Solver.h.

◆ vardata

vec<VarData> Minisat::Solver::vardata

protected

Definition at line 185 of file Solver.h.

◆ verbosity

int Minisat::Solver::verbosity

Definition at line 117 of file Solver.h.

◆ watches

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

protected

Definition at line 179 of file Solver.h.

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

src/sat/bsat2/Solver.h
src/sat/bsat2/Solver.cpp

Classes

Public Member Functions

Public Attributes

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ Solver()

◆ ~Solver()

Member Function Documentation

◆ abstractLevel()

◆ addClause() [1/4]

◆ addClause() [2/4]

◆ addClause() [3/4]

◆ addClause() [4/4]

◆ addClause_()

◆ addEmptyClause()

◆ analyze()

◆ analyzeFinal()

◆ attachClause()

◆ budgetOff()

◆ cancelUntil()

◆ checkGarbage() [1/2]

◆ checkGarbage() [2/2]

◆ claBumpActivity()

◆ claDecayActivity()

◆ clearInterrupt()

◆ decisionLevel()

◆ detachClause()

◆ drand()

◆ enqueue()

◆ garbageCollect()

◆ insertVarOrder()

◆ interrupt()

◆ irand()

◆ level()

◆ litRedundant()

◆ locked()

◆ mkVarData()

◆ modelValue() [1/2]

◆ modelValue() [2/2]

◆ nAssigns()

◆ nClauses()

◆ newDecisionLevel()

◆ newVar()

◆ nFreeVars()

◆ nLearnts()

◆ nVars()

◆ okay()

◆ pickBranchLit()

◆ progressEstimate()

◆ propagate()

◆ reason()

◆ rebuildOrderHeap()

◆ reduceDB()

◆ relocAll()

◆ removeClause()

◆ removeSatisfied()

◆ satisfied()

◆ search()

◆ setConfBudget()

◆ setDecisionVar()

◆ setPolarity()

◆ setPropBudget()

◆ simplify()

◆ solve() [1/5]

◆ solve() [2/5]

◆ solve() [3/5]

◆ solve() [4/5]

◆ solve() [5/5]

◆ solve_()

◆ solveLimited()

◆ toDimacs() [1/7]

◆ toDimacs() [2/7]

◆ toDimacs() [3/7]

◆ toDimacs() [4/7]

◆ toDimacs() [5/7]

◆ toDimacs() [6/7]

◆ toDimacs() [7/7]