Minisat::SimpSolver Class Reference

#include <SimpSolver.h>

Inherits Minisat::Solver.

Data Structures
struct	ClauseDeleted
struct	ElimLt

Public Member Functions
	SimpSolver ()
	~SimpSolver ()
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	substitute (Var v, Lit x)
void	setFrozen (Var v, bool b)
bool	isEliminated (Var v) const
bool	solve (const vec< Lit > &assumps, bool do_simp=true, bool turn_off_simp=false)
lbool	solveLimited (const vec< Lit > &assumps, bool do_simp=true, bool turn_off_simp=false)
bool	solve (bool do_simp=true, bool turn_off_simp=false)
bool	solve (Lit p, bool do_simp=true, bool turn_off_simp=false)
bool	solve (Lit p, Lit q, bool do_simp=true, bool turn_off_simp=false)
bool	solve (Lit p, Lit q, Lit r, bool do_simp=true, bool turn_off_simp=false)
bool	eliminate (bool turn_off_elim=false)
virtual void	garbageCollect ()
bool	simplify ()
bool	solve (const vec< Lit > &assumps)
bool	solve ()
bool	solve (Lit p)
bool	solve (Lit p, Lit q)
bool	solve (Lit p, Lit q, Lit r)
lbool	solveLimited (const vec< Lit > &assumps)
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 ()
void	checkGarbage (double gf)
void	checkGarbage ()

Data Fields
int	grow
int	clause_lim
int	subsumption_lim
double	simp_garbage_frac
bool	use_asymm
bool	use_rcheck
bool	use_elim
int	merges
int	asymm_lits
int	eliminated_vars
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
lbool	solve_ (bool do_simp=true, bool turn_off_simp=false)
bool	asymm (Var v, CRef cr)
bool	asymmVar (Var v)
void	updateElimHeap (Var v)
void	gatherTouchedClauses ()
bool	merge (const Clause &_ps, const Clause &_qs, Var v, vec< Lit > &out_clause)
bool	merge (const Clause &_ps, const Clause &_qs, Var v, int &size)
bool	backwardSubsumptionCheck (bool verbose=false)
bool	eliminateVar (Var v)
void	extendModel ()
void	removeClause (CRef cr)
bool	strengthenClause (CRef cr, Lit l)
void	cleanUpClauses ()
bool	implied (const vec< Lit > &c)
void	relocAll (ClauseAllocator &to)
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)
bool	locked (const Clause &c) const
bool	satisfied (const Clause &c) const
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
int	elimorder
bool	use_simplification
vec< uint32_t >	elimclauses
vec< char >	touched
OccLists< Var, vec< CRef > , ClauseDeleted >	occurs
vec< int >	n_occ
Heap< ElimLt >	elim_heap
Queue< CRef >	subsumption_queue
vec< char >	frozen
vec< char >	eliminated
int	bwdsub_assigns
int	n_touched
CRef	bwdsub_tmpunit
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 33 of file SimpSolver.h.

Constructor & Destructor Documentation

SimpSolver::SimpSolver

(

)

Definition at line 46 of file SimpSolver.cpp.

                       :
    grow               (opt_grow)
  , clause_lim         (opt_clause_lim)
  , subsumption_lim    (opt_subsumption_lim)
  , simp_garbage_frac  (opt_simp_garbage_frac)
  , use_asymm          (opt_use_asymm)
  , use_rcheck         (opt_use_rcheck)
  , use_elim           (opt_use_elim)
  , merges             (0)
  , asymm_lits         (0)
  , eliminated_vars    (0)
  , elimorder          (1)
  , use_simplification (true)
  , occurs             (ClauseDeleted(ca))
  , elim_heap          (ElimLt(n_occ))
  , bwdsub_assigns     (0)
  , n_touched          (0)
{
    vec<Lit> dummy(1,lit_Undef);
    ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
    bwdsub_tmpunit        = ca.alloc(dummy);
    remove_satisfied      = false;
}

SimpSolver::~SimpSolver

(

)

Definition at line 71 of file SimpSolver.cpp.

{
}

Member Function Documentation

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

inlineprotectedinherited

Definition at line 320 of file Solver.h.

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

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

inline

Definition at line 177 of file SimpSolver.h.

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

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

inline

Definition at line 179 of file SimpSolver.h.

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

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

inline

Definition at line 180 of file SimpSolver.h.

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

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

inline

Definition at line 181 of file SimpSolver.h.

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

bool SimpSolver::addClause_

(

vec< Lit > &

ps

)

Definition at line 135 of file SimpSolver.cpp.

{
#ifndef NDEBUG
    for (int i = 0; i < ps.size(); i++)
        assert(!isEliminated(var(ps[i])));
#endif

    int nclauses = clauses.size();

    if (use_rcheck && implied(ps))
        return true;

    if (!Solver::addClause_(ps))
        return false;

    if (use_simplification && clauses.size() == nclauses + 1){
        CRef          cr = clauses.last();
        const Clause& c  = ca[cr];

        // NOTE: the clause is added to the queue immediately and then
        // again during 'gatherTouchedClauses()'. If nothing happens
        // in between, it will only be checked once. Otherwise, it may
        // be checked twice unnecessarily. This is an unfortunate
        // consequence of how backward subsumption is used to mimic
        // forward subsumption.
        subsumption_queue.insert(cr);
        for (int i = 0; i < c.size(); i++){
            occurs[var(c[i])].push(cr);
            n_occ[toInt(c[i])]++;
            touched[var(c[i])] = 1;
            n_touched++;
            if (elim_heap.inHeap(var(c[i])))
                elim_heap.increase(var(c[i]));
        }
    }

    return true;
}

bool Minisat::SimpSolver::addEmptyClause ( )

inline

Definition at line 178 of file SimpSolver.h.

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

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

protectedinherited

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  )

protectedinherited

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

bool SimpSolver::asymm ( Var  v, CRef  cr  )

protected

Definition at line 394 of file SimpSolver.cpp.

{
    Clause& c = ca[cr];
    assert(decisionLevel() == 0);

    if (c.mark() || satisfied(c)) return true;

    trail_lim.push(trail.size());
    Lit l = lit_Undef;
    for (int i = 0; i < c.size(); i++)
        if (var(c[i]) != v && value(c[i]) != l_False)
            uncheckedEnqueue(~c[i]);
        else
            l = c[i];

    if (propagate() != CRef_Undef){
        cancelUntil(0);
        asymm_lits++;
        if (!strengthenClause(cr, l))
            return false;
    }else
        cancelUntil(0);

    return true;
}

bool SimpSolver::asymmVar ( Var  v )

protected

Definition at line 421 of file SimpSolver.cpp.

{
    assert(use_simplification);

    const vec<CRef>& cls = occurs.lookup(v);

    if (value(v) != l_Undef || cls.size() == 0)
        return true;

    for (int i = 0; i < cls.size(); i++)
        if (!asymm(v, cls[i]))
            return false;

    return backwardSubsumptionCheck();
}

void Solver::attachClause ( CRef  cr )

protectedinherited

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

bool SimpSolver::backwardSubsumptionCheck ( bool  verbose = false )

protected

Definition at line 327 of file SimpSolver.cpp.

{
    int cnt = 0;
    int subsumed = 0;
    int deleted_literals = 0;
    assert(decisionLevel() == 0);

    while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){

        // Empty subsumption queue and return immediately on user-interrupt:
        if (asynch_interrupt){
            subsumption_queue.clear();
            bwdsub_assigns = trail.size();
            break; }

        // Check top-level assignments by creating a dummy clause and placing it in the queue:
        if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
            Lit l = trail[bwdsub_assigns++];
            ca[bwdsub_tmpunit][0] = l;
            ca[bwdsub_tmpunit].calcAbstraction();
            subsumption_queue.insert(bwdsub_tmpunit); }

        CRef    cr = subsumption_queue.peek(); subsumption_queue.pop();
        Clause& c  = ca[cr];

        if (c.mark()) continue;

        if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
            printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);

        assert(c.size() > 1 || value(c[0]) == l_True);    // Unit-clauses should have been propagated before this point.

        // Find best variable to scan:
        Var best = var(c[0]);
        for (int i = 1; i < c.size(); i++)
            if (occurs[var(c[i])].size() < occurs[best].size())
                best = var(c[i]);

        // Search all candidates:
        vec<CRef>& _cs = occurs.lookup(best);
        CRef*       cs = (CRef*)_cs;

        for (int j = 0; j < _cs.size(); j++)
            if (c.mark())
                break;
            else if (!ca[cs[j]].mark() &&  cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){
                Lit l = c.subsumes(ca[cs[j]]);

                if (l == lit_Undef)
                    subsumed++, removeClause(cs[j]);
                else if (l != lit_Error){
                    deleted_literals++;

                    if (!strengthenClause(cs[j], ~l))
                        return false;

                    // Did current candidate get deleted from cs? Then check candidate at index j again:
                    if (var(l) == best)
                        j--;
                }
            }
    }

    return true;
}

void Minisat::Solver::budgetOff ( )

inlineinherited

Definition at line 343 of file Solver.h.

{ conflict_budget = propagation_budget = -1; }

void Solver::cancelUntil ( int  level )

protectedinherited

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 )

inlineinherited

Definition at line 305 of file Solver.h.

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

void Minisat::Solver::checkGarbage ( void  )

inlineinherited

Definition at line 304 of file Solver.h.

{ checkGarbage(garbage_frac); }

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

inlineprotectedinherited

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

inlineprotectedinherited

Definition at line 296 of file Solver.h.

{ cla_inc *= (1 / clause_decay); }

void SimpSolver::cleanUpClauses ( )

protected

Definition at line 667 of file SimpSolver.cpp.

{
    occurs.cleanAll();
    int i,j;
    for (i = j = 0; i < clauses.size(); i++)
        if (ca[clauses[i]].mark() == 0)
            clauses[j++] = clauses[i];
    clauses.shrink(i - j);
}

void Minisat::Solver::clearInterrupt ( )

inlineinherited

Definition at line 342 of file Solver.h.

{ asynch_interrupt = false; }

int Minisat::Solver::decisionLevel ( ) const

inlineprotectedinherited

Definition at line 319 of file Solver.h.

{ return trail_lim.size(); }

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

protectedinherited

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 )

inlinestaticprotectedinherited

Definition at line 262 of file Solver.h.

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

bool SimpSolver::eliminate

(

bool

turn_off_elim = false

)

Definition at line 582 of file SimpSolver.cpp.

{
    if (!simplify())
        return false;
    else if (!use_simplification)
        return true;

    // Main simplification loop:
    //
    while (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0){

        gatherTouchedClauses();
        // printf("  ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
        if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) && 
            !backwardSubsumptionCheck(true)){
            ok = false; goto cleanup; }

        // Empty elim_heap and return immediately on user-interrupt:
        if (asynch_interrupt){
            assert(bwdsub_assigns == trail.size());
            assert(subsumption_queue.size() == 0);
            assert(n_touched == 0);
            elim_heap.clear();
            goto cleanup; }

        // printf("  ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
        for (int cnt = 0; !elim_heap.empty(); cnt++){
            Var elim = elim_heap.removeMin();
            
            if (asynch_interrupt) break;

            if (isEliminated(elim) || value(elim) != l_Undef) continue;

            if (verbosity >= 2 && cnt % 100 == 0)
                printf("elimination left: %10d\r", elim_heap.size());

            if (use_asymm){
                // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
                bool was_frozen = frozen[elim];
                frozen[elim] = true;
                if (!asymmVar(elim)){
                    ok = false; goto cleanup; }
                frozen[elim] = was_frozen; }

            // At this point, the variable may have been set by assymetric branching, so check it
            // again. Also, don't eliminate frozen variables:
            if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){
                ok = false; goto cleanup; }

            checkGarbage(simp_garbage_frac);
        }

        assert(subsumption_queue.size() == 0);
    }
 cleanup:

    // If no more simplification is needed, free all simplification-related data structures:
    if (turn_off_elim){
        touched  .clear(true);
        occurs   .clear(true);
        n_occ    .clear(true);
        elim_heap.clear(true);
        subsumption_queue.clear(true);

        use_simplification    = false;
        remove_satisfied      = true;
        ca.extra_clause_field = false;

        // Force full cleanup (this is safe and desirable since it only happens once):
        rebuildOrderHeap();
        garbageCollect();
    }else{
        // Cheaper cleanup:
        cleanUpClauses(); // TODO: can we make 'cleanUpClauses()' not be linear in the problem size somehow?
        checkGarbage();
    }

    if (verbosity >= 1 && elimclauses.size() > 0)
        printf("|  Eliminated clauses:     %10.2f Mb                                      |\n", 
               double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));

    return ok;
}

bool SimpSolver::eliminateVar ( Var  v )

protected

Definition at line 471 of file SimpSolver.cpp.

{
    assert(!frozen[v]);
    assert(!isEliminated(v));
    assert(value(v) == l_Undef);
    int i;

    // Split the occurrences into positive and negative:
    //
    const vec<CRef>& cls = occurs.lookup(v);
    vec<CRef>        pos, neg;
    for (i = 0; i < cls.size(); i++)
        (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);

    // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
    // clause must exceed the limit on the maximal clause size (if it is set):
    //
    int cnt         = 0;
    int clause_size = 0;

    for (i = 0; i < pos.size(); i++)
        for (int j = 0; j < neg.size(); j++)
            if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) && 
                (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))
                return true;

    // Delete and store old clauses:
    eliminated[v] = true;
    setDecisionVar(v, false);
    eliminated_vars++;

    if (pos.size() > neg.size()){
        for (int i = 0; i < neg.size(); i++)
            mkElimClause(elimclauses, v, ca[neg[i]]);
        mkElimClause(elimclauses, mkLit(v));
    }else{
        for (int i = 0; i < pos.size(); i++)
            mkElimClause(elimclauses, v, ca[pos[i]]);
        mkElimClause(elimclauses, ~mkLit(v));
    }

    for (i = 0; i < cls.size(); i++)
        removeClause(cls[i]); 

    // Produce clauses in cross product:
    vec<Lit>& resolvent = add_tmp;
    for (i = 0; i < pos.size(); i++)
        for (int j = 0; j < neg.size(); j++)
            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent))
                return false;

    // Free occurs list for this variable:
    occurs[v].clear(true);
    
    // Free watchers lists for this variable, if possible:
    if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
    if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);

    return backwardSubsumptionCheck();
}

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

inlineprotectedinherited

Definition at line 310 of file Solver.h.

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

void SimpSolver::extendModel ( )

protected

Definition at line 565 of file SimpSolver.cpp.

{
    int i, j;
    Lit x;

    for (i = elimclauses.size()-1; i > 0; i -= j){
        for (j = elimclauses[i--]; j > 1; j--, i--)
            if (modelValue(toLit(elimclauses[i])) != l_False)
                goto next;

        x = toLit(elimclauses[i]);
        model[var(x)] = lbool(!sign(x));
    next:;
    }
}

void SimpSolver::garbageCollect ( )

virtual

Reimplemented from Minisat::Solver.

Definition at line 706 of file SimpSolver.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()); 

    cleanUpClauses();
    to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
    relocAll(to);
    Solver::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 SimpSolver::gatherTouchedClauses ( )

protected

Definition at line 278 of file SimpSolver.cpp.

{
    if (n_touched == 0) return;

    int i,j;
    for (i = j = 0; i < subsumption_queue.size(); i++)
        if (ca[subsumption_queue[i]].mark() == 0)
            ca[subsumption_queue[i]].mark(2);

    for (i = 0; i < touched.size(); i++)
        if (touched[i]){
            const vec<CRef>& cs = occurs.lookup(i);
            for (j = 0; j < cs.size(); j++)
                if (ca[cs[j]].mark() == 0){
                    subsumption_queue.insert(cs[j]);
                    ca[cs[j]].mark(2);
                }
            touched[i] = 0;
        }

    for (i = 0; i < subsumption_queue.size(); i++)
        if (ca[subsumption_queue[i]].mark() == 2)
            ca[subsumption_queue[i]].mark(0);

    n_touched = 0;
}

bool SimpSolver::implied ( const vec< Lit > &  c )

protected

Definition at line 306 of file SimpSolver.cpp.

{
    assert(decisionLevel() == 0);

    trail_lim.push(trail.size());
    for (int i = 0; i < c.size(); i++)
        if (value(c[i]) == l_True){
            cancelUntil(0);
            return false;
        }else if (value(c[i]) != l_False){
            assert(value(c[i]) == l_Undef);
            uncheckedEnqueue(~c[i]);
        }

    bool result = propagate() != CRef_Undef;
    cancelUntil(0);
    return result;
}

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

inlineprotectedinherited

Definition at line 280 of file Solver.h.

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

void Minisat::Solver::interrupt ( )

inlineinherited

Definition at line 341 of file Solver.h.

{ asynch_interrupt = true; }

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

inlinestaticprotectedinherited

Definition at line 269 of file Solver.h.

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

bool Minisat::SimpSolver::isEliminated ( Var  v ) const

inline

Definition at line 169 of file SimpSolver.h.

{ return eliminated[v]; }

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

inlineprotectedinherited

Definition at line 278 of file Solver.h.

{ return vardata[x].level; }

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

protectedinherited

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

inlineprotectedinherited

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

bool SimpSolver::merge ( const Clause &  _ps, const Clause &  _qs, Var  v, vec< Lit > &  out_clause  )

protected

Definition at line 217 of file SimpSolver.cpp.

{
    merges++;
    out_clause.clear();

    bool  ps_smallest = _ps.size() < _qs.size();
    const Clause& ps  =  ps_smallest ? _qs : _ps;
    const Clause& qs  =  ps_smallest ? _ps : _qs;
    int i, j;

    for (i = 0; i < qs.size(); i++){
        if (var(qs[i]) != v){
            for (j = 0; j < ps.size(); j++)
                if (var(ps[j]) == var(qs[i]))
                    if (ps[j] == ~qs[i])
                        return false;
                    else
                        goto next;
            out_clause.push(qs[i]);
        }
        next:;
    }

    for (i = 0; i < ps.size(); i++)
        if (var(ps[i]) != v)
            out_clause.push(ps[i]);

    return true;
}

bool SimpSolver::merge ( const Clause &  _ps, const Clause &  _qs, Var  v, int &  size  )

protected

Definition at line 249 of file SimpSolver.cpp.

{
    merges++;

    bool  ps_smallest = _ps.size() < _qs.size();
    const Clause& ps  =  ps_smallest ? _qs : _ps;
    const Clause& qs  =  ps_smallest ? _ps : _qs;
    const Lit*  __ps  = (const Lit*)ps;
    const Lit*  __qs  = (const Lit*)qs;

    size = ps.size()-1;

    for (int i = 0; i < qs.size(); i++){
        if (var(__qs[i]) != v){
            for (int j = 0; j < ps.size(); j++)
                if (var(__ps[j]) == var(__qs[i]))
                    if (__ps[j] == ~__qs[i])
                        return false;
                    else
                        goto next;
            size++;
        }
        next:;
    }

    return true;
}

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

inlinestaticprotectedinherited

Definition at line 146 of file Solver.h.

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

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

inlineinherited

Definition at line 323 of file Solver.h.

{ return model[x]; }

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

inlineinherited

Definition at line 324 of file Solver.h.

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

int Minisat::Solver::nAssigns ( ) const

inlineinherited

Definition at line 325 of file Solver.h.

{ return trail.size(); }

int Minisat::Solver::nClauses ( ) const

inlineinherited

Definition at line 326 of file Solver.h.

{ return clauses.size(); }

void Minisat::Solver::newDecisionLevel ( )

inlineprotectedinherited

Definition at line 317 of file Solver.h.

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

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

Definition at line 76 of file SimpSolver.cpp.

                                           {
    Var v = Solver::newVar(sign, dvar);

    frozen    .push((char)false);
    eliminated.push((char)false);

    if (use_simplification){
        n_occ     .push(0);
        n_occ     .push(0);
        occurs    .init(v);
        touched   .push(0);
        elim_heap .insert(v);
    }
    return v; }

int Minisat::Solver::nFreeVars ( ) const

inlineinherited

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

inlineinherited

Definition at line 327 of file Solver.h.

{ return learnts.size(); }

int Minisat::Solver::nVars ( ) const

inlineinherited

Definition at line 328 of file Solver.h.

{ return vardata.size(); }

bool Minisat::Solver::okay ( ) const

inlineinherited

Definition at line 358 of file Solver.h.

{ return ok; }

Lit Solver::pickBranchLit ( )

protectedinherited

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

protectedinherited

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

protectedinherited

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

inlineprotectedinherited

Definition at line 277 of file Solver.h.

{ return vardata[x].reason; }

void Solver::rebuildOrderHeap ( )

protectedinherited

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

protectedinherited

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 SimpSolver::relocAll ( ClauseAllocator &  to )

protected

Definition at line 682 of file SimpSolver.cpp.

{
    if (!use_simplification) return;

    // All occurs lists:
    //
    int i;
    for (i = 0; i < nVars(); i++){
        vec<CRef>& cs = occurs[i];
        for (int j = 0; j < cs.size(); j++)
            ca.reloc(cs[j], to);
    }

    // Subsumption queue:
    //
    for (i = 0; i < subsumption_queue.size(); i++)
        ca.reloc(subsumption_queue[i], to);

    // Temporary clause:
    //
    ca.reloc(bwdsub_tmpunit, to);
}

void SimpSolver::removeClause ( CRef  cr )

protected

Definition at line 175 of file SimpSolver.cpp.

{
    const Clause& c = ca[cr];

    if (use_simplification)
        for (int i = 0; i < c.size(); i++){
            n_occ[toInt(c[i])]--;
            updateElimHeap(var(c[i]));
            occurs.smudge(var(c[i]));
        }

    Solver::removeClause(cr);
}

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

protectedinherited

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

protectedinherited

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 )

protectedinherited

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 )

inlineinherited

Definition at line 339 of file Solver.h.

{ conflict_budget    = conflicts    + x; }

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

inlineinherited

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::SimpSolver::setFrozen ( Var  v, bool  b  )

inline

Definition at line 182 of file SimpSolver.h.

{ frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }

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

inlineinherited

Definition at line 330 of file Solver.h.

{ polarity[v] = b; }

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

inlineinherited

Definition at line 340 of file Solver.h.

{ propagation_budget = propagations + x; }

bool Solver::simplify ( )

inherited

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::SimpSolver::solve ( const vec< Lit > &  assumps, bool  do_simp = true, bool  turn_off_simp = false  )

inline

Definition at line 188 of file SimpSolver.h.

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

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

inlineinherited

Definition at line 356 of file Solver.h.

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

bool Minisat::SimpSolver::solve ( bool  do_simp = true, bool  turn_off_simp = false  )

inline

Definition at line 184 of file SimpSolver.h.

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

bool Minisat::Solver::solve ( )

inlineinherited

Definition at line 352 of file Solver.h.

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

bool Minisat::SimpSolver::solve ( Lit  p, bool  do_simp = true, bool  turn_off_simp = false  )

inline

Definition at line 185 of file SimpSolver.h.

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

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

inlineinherited

Definition at line 353 of file Solver.h.

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

bool Minisat::SimpSolver::solve ( Lit  p, Lit  q, bool  do_simp = true, bool  turn_off_simp = false  )

inline

Definition at line 186 of file SimpSolver.h.

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

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

inlineinherited

Definition at line 354 of file Solver.h.

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

bool Minisat::SimpSolver::solve ( Lit  p, Lit  q, Lit  r, bool  do_simp = true, bool  turn_off_simp = false  )

inline

Definition at line 187 of file SimpSolver.h.

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

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

inlineinherited

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 SimpSolver::solve_ ( bool  do_simp = true, bool  turn_off_simp = false  )

protected

Definition at line 93 of file SimpSolver.cpp.

{
    vec<Var> extra_frozen;
    lbool    result = l_True;

    do_simp &= use_simplification;

    if (do_simp){
        // Assumptions must be temporarily frozen to run variable elimination:
        for (int i = 0; i < assumptions.size(); i++){
            Var v = var(assumptions[i]);

            // If an assumption has been eliminated, remember it.
            assert(!isEliminated(v));

            if (!frozen[v]){
                // Freeze and store.
                setFrozen(v, true);
                extra_frozen.push(v);
            } }

        result = lbool(eliminate(turn_off_simp));
    }

    if (result == l_True)
        result = Solver::solve_();
    else if (verbosity >= 1)
        printf("===============================================================================\n");

    if (result == l_True)
        extendModel();

    if (do_simp)
        // Unfreeze the assumptions that were frozen:
        for (int i = 0; i < extra_frozen.size(); i++)
            setFrozen(extra_frozen[i], false);

    return result;
}

lbool Solver::solve_ ( )

protectedinherited

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::SimpSolver::solveLimited ( const vec< Lit > &  assumps, bool  do_simp = true, bool  turn_off_simp = false  )

inline

Definition at line 191 of file SimpSolver.h.

                                                                                               { 
    assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }

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

inlineinherited

Definition at line 357 of file Solver.h.

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

bool SimpSolver::strengthenClause ( CRef  cr, Lit  l  )

protected

Definition at line 190 of file SimpSolver.cpp.

{
    Clause& c = ca[cr];
    assert(decisionLevel() == 0);
    assert(use_simplification);

    // FIX: this is too inefficient but would be nice to have (properly implemented)
    // if (!find(subsumption_queue, &c))
    subsumption_queue.insert(cr);

    if (c.size() == 2){
        removeClause(cr);
        c.strengthen(l);
    }else{
        detachClause(cr, true);
        c.strengthen(l);
        attachClause(cr);
        remove(occurs[var(l)], cr);
        n_occ[toInt(l)]--;
        updateElimHeap(var(l));
    }

    return c.size() == 1 ? enqueue(c[0]) && propagate() == CRef_Undef : true;
}

bool SimpSolver::substitute	(	Var	v,
		Lit	x
	)

Definition at line 533 of file SimpSolver.cpp.

{
    assert(!frozen[v]);
    assert(!isEliminated(v));
    assert(value(v) == l_Undef);

    if (!ok) return false;

    eliminated[v] = true;
    setDecisionVar(v, false);
    const vec<CRef>& cls = occurs.lookup(v);
    
    vec<Lit>& subst_clause = add_tmp;
    for (int i = 0; i < cls.size(); i++){
        Clause& c = ca[cls[i]];

        subst_clause.clear();
        for (int j = 0; j < c.size(); j++){
            Lit p = c[j];
            subst_clause.push(var(p) == v ? x ^ sign(p) : p);
        }

        removeClause(cls[i]);

        if (!addClause_(subst_clause))
            return ok = false;
    }

    return true;
}

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

inherited

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  )

inherited

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  )

inherited

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 )

inlineinherited

Definition at line 360 of file Solver.h.

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

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

inlineinherited

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  )

inlineinherited

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  )

inlineinherited

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  )

protectedinherited

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

void Minisat::SimpSolver::updateElimHeap ( Var  v )

inlineprotected

Definition at line 170 of file SimpSolver.h.

                                            {
    assert(use_simplification);
    // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
    if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
        elim_heap.update(v); }

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

inlineinherited

Definition at line 321 of file Solver.h.

{ return assigns[x]; }

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

inlineinherited

Definition at line 322 of file Solver.h.

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

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

inlineprotectedinherited

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 )

inlineprotectedinherited

Definition at line 284 of file Solver.h.

{ varBumpActivity(v, var_inc); }

void Minisat::Solver::varDecayActivity ( )

inlineprotectedinherited

Definition at line 283 of file Solver.h.

{ var_inc *= (1 / var_decay); }

bool Minisat::Solver::withinBudget ( ) const

inlineprotectedinherited

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

protectedinherited

Definition at line 175 of file Solver.h.

vec<Lit> Minisat::Solver::add_tmp

protectedinherited

Definition at line 201 of file Solver.h.

vec<Lit> Minisat::Solver::analyze_stack

protectedinherited

Definition at line 199 of file Solver.h.

vec<Lit> Minisat::Solver::analyze_toclear

protectedinherited

Definition at line 200 of file Solver.h.

vec<lbool> Minisat::Solver::assigns

protectedinherited

Definition at line 179 of file Solver.h.

vec<Lit> Minisat::Solver::assumptions

protectedinherited

Definition at line 188 of file Solver.h.

int Minisat::SimpSolver::asymm_lits

Definition at line 96 of file SimpSolver.h.

bool Minisat::Solver::asynch_interrupt

protectedinherited

Definition at line 211 of file Solver.h.

int Minisat::SimpSolver::bwdsub_assigns

protected

Definition at line 137 of file SimpSolver.h.

CRef Minisat::SimpSolver::bwdsub_tmpunit

protected

Definition at line 142 of file SimpSolver.h.

ClauseAllocator Minisat::Solver::ca

protectedinherited

Definition at line 193 of file Solver.h.

int Minisat::Solver::ccmin_mode

inherited

Definition at line 122 of file Solver.h.

double Minisat::Solver::cla_inc

protectedinherited

Definition at line 174 of file Solver.h.

double Minisat::Solver::clause_decay

inherited

Definition at line 118 of file Solver.h.

int Minisat::SimpSolver::clause_lim

Definition at line 84 of file SimpSolver.h.

vec<CRef> Minisat::Solver::clauses

protectedinherited

Definition at line 172 of file Solver.h.

uint64_t Minisat::Solver::clauses_literals

inherited

Definition at line 139 of file Solver.h.

vec<Lit> Minisat::Solver::conflict

inherited

Definition at line 111 of file Solver.h.

int64_t Minisat::Solver::conflict_budget

protectedinherited

Definition at line 209 of file Solver.h.

uint64_t Minisat::Solver::conflicts

inherited

Definition at line 138 of file Solver.h.

uint64_t Minisat::Solver::dec_vars

inherited

Definition at line 139 of file Solver.h.

vec<char> Minisat::Solver::decision

protectedinherited

Definition at line 181 of file Solver.h.

uint64_t Minisat::Solver::decisions

inherited

Definition at line 138 of file Solver.h.

Heap<ElimLt> Minisat::SimpSolver::elim_heap

protected

Definition at line 133 of file SimpSolver.h.

vec<uint32_t> Minisat::SimpSolver::elimclauses

protected

Definition at line 128 of file SimpSolver.h.

vec<char> Minisat::SimpSolver::eliminated

protected

Definition at line 136 of file SimpSolver.h.

int Minisat::SimpSolver::eliminated_vars

Definition at line 97 of file SimpSolver.h.

int Minisat::SimpSolver::elimorder

protected

Definition at line 126 of file SimpSolver.h.

vec<char> Minisat::SimpSolver::frozen

protected

Definition at line 135 of file SimpSolver.h.

double Minisat::Solver::garbage_frac

inherited

Definition at line 126 of file Solver.h.

int Minisat::SimpSolver::grow

Definition at line 83 of file SimpSolver.h.

vec<CRef> Minisat::Solver::learnts

protectedinherited

Definition at line 173 of file Solver.h.

uint64_t Minisat::Solver::learnts_literals

inherited

Definition at line 139 of file Solver.h.

int Minisat::Solver::learntsize_adjust_cnt

protectedinherited

Definition at line 205 of file Solver.h.

double Minisat::Solver::learntsize_adjust_confl

protectedinherited

Definition at line 204 of file Solver.h.

double Minisat::Solver::learntsize_adjust_inc

inherited

Definition at line 134 of file Solver.h.

int Minisat::Solver::learntsize_adjust_start_confl

inherited

Definition at line 133 of file Solver.h.

double Minisat::Solver::learntsize_factor

inherited

Definition at line 130 of file Solver.h.

double Minisat::Solver::learntsize_inc

inherited

Definition at line 131 of file Solver.h.

bool Minisat::Solver::luby_restart

inherited

Definition at line 121 of file Solver.h.

double Minisat::Solver::max_learnts

protectedinherited

Definition at line 203 of file Solver.h.

uint64_t Minisat::Solver::max_literals

inherited

Definition at line 139 of file Solver.h.

int Minisat::SimpSolver::merges

Definition at line 95 of file SimpSolver.h.

vec<lbool> Minisat::Solver::model

inherited

Definition at line 110 of file Solver.h.

vec<int> Minisat::SimpSolver::n_occ

protected

Definition at line 132 of file SimpSolver.h.

int Minisat::SimpSolver::n_touched

protected

Definition at line 138 of file SimpSolver.h.

OccLists<Var, vec<CRef>, ClauseDeleted> Minisat::SimpSolver::occurs

protected

Definition at line 131 of file SimpSolver.h.

bool Minisat::Solver::ok

protectedinherited

Definition at line 171 of file Solver.h.

Heap<VarOrderLt> Minisat::Solver::order_heap

protectedinherited

Definition at line 189 of file Solver.h.

int Minisat::Solver::phase_saving

inherited

Definition at line 123 of file Solver.h.

vec<char> Minisat::Solver::polarity

protectedinherited

Definition at line 180 of file Solver.h.

double Minisat::Solver::progress_estimate

protectedinherited

Definition at line 190 of file Solver.h.

int64_t Minisat::Solver::propagation_budget

protectedinherited

Definition at line 210 of file Solver.h.

uint64_t Minisat::Solver::propagations

inherited

Definition at line 138 of file Solver.h.

int Minisat::Solver::qhead

protectedinherited

Definition at line 185 of file Solver.h.

double Minisat::Solver::random_seed

inherited

Definition at line 120 of file Solver.h.

double Minisat::Solver::random_var_freq

inherited

Definition at line 119 of file Solver.h.

bool Minisat::Solver::remove_satisfied

protectedinherited

Definition at line 191 of file Solver.h.

int Minisat::Solver::restart_first

inherited

Definition at line 128 of file Solver.h.

double Minisat::Solver::restart_inc

inherited

Definition at line 129 of file Solver.h.

uint64_t Minisat::Solver::rnd_decisions

inherited

Definition at line 138 of file Solver.h.

bool Minisat::Solver::rnd_init_act

inherited

Definition at line 125 of file Solver.h.

bool Minisat::Solver::rnd_pol

inherited

Definition at line 124 of file Solver.h.

vec<char> Minisat::Solver::seen

protectedinherited

Definition at line 198 of file Solver.h.

double Minisat::SimpSolver::simp_garbage_frac

Definition at line 87 of file SimpSolver.h.

int Minisat::Solver::simpDB_assigns

protectedinherited

Definition at line 186 of file Solver.h.

int64_t Minisat::Solver::simpDB_props

protectedinherited

Definition at line 187 of file Solver.h.

uint64_t Minisat::Solver::solves

inherited

Definition at line 138 of file Solver.h.

uint64_t Minisat::Solver::starts

inherited

Definition at line 138 of file Solver.h.

int Minisat::SimpSolver::subsumption_lim

Definition at line 86 of file SimpSolver.h.

Queue<CRef> Minisat::SimpSolver::subsumption_queue

protected

Definition at line 134 of file SimpSolver.h.

uint64_t Minisat::Solver::tot_literals

inherited

Definition at line 139 of file Solver.h.

vec<char> Minisat::SimpSolver::touched

protected

Definition at line 129 of file SimpSolver.h.

vec<Lit> Minisat::Solver::trail

protectedinherited

Definition at line 182 of file Solver.h.

vec<int> Minisat::Solver::trail_lim

protectedinherited

Definition at line 183 of file Solver.h.

bool Minisat::SimpSolver::use_asymm

Definition at line 89 of file SimpSolver.h.

bool Minisat::SimpSolver::use_elim

Definition at line 91 of file SimpSolver.h.

bool Minisat::SimpSolver::use_rcheck

Definition at line 90 of file SimpSolver.h.

bool Minisat::SimpSolver::use_simplification

protected

Definition at line 127 of file SimpSolver.h.

double Minisat::Solver::var_decay

inherited

Definition at line 117 of file Solver.h.

double Minisat::Solver::var_inc

protectedinherited

Definition at line 176 of file Solver.h.

vec<VarData> Minisat::Solver::vardata

protectedinherited

Definition at line 184 of file Solver.h.

int Minisat::Solver::verbosity

inherited

Definition at line 116 of file Solver.h.

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

protectedinherited

Definition at line 178 of file Solver.h.

---

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

• SimpSolver.h
• SimpSolver.cpp