Logo Search packages:      
Sourcecode: sat4j version File versions

org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> Class Reference

Inheritance diagram for org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>:

org::sat4j::specs::ISolver org::sat4j::minisat::core::UnitPropagationListener org::sat4j::minisat::core::ActivityListener org::sat4j::minisat::core::Learner org::sat4j::specs::IProblem org::sat4j::minisat::core::VarActivityListener org::sat4j::minisat::core::ConstrActivityListener

List of all members.

Detailed Description

The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.


Definition at line 81 of file Solver.java.

Public Member Functions

void addAllClauses (IVec< IVecInt > clauses) throws ContradictionException
IConstr addAtLeast (IVecInt literals, int degree) throws ContradictionException
IConstr addAtMost (IVecInt literals, int degree) throws ContradictionException
IConstr addClause (IVecInt literals) throws ContradictionException
void analyze (Constr confl, Pair results)
boolean assume (int p)
void claBumpActivity (Constr confl)
void clearLearntClauses ()
int decisionLevel ()
boolean enqueue (int p, Constr from)
boolean enqueue (int p)
void expireTimeout ()
int[] findModel (IVecInt assumps) throws TimeoutException
int[] findModel () throws TimeoutException
DataStructureFactory< L > getDSFactory ()
IConstr getIthConstr (int i)
IOrder< L > getOrder ()
IVecInt getOutLearnt ()
Map< String, Number > getStat ()
SolverStats getStats ()
int getTimeout ()
getVocabulary ()
boolean isDBSimplificationAllowed ()
boolean isSatisfiable (IVecInt assumps, boolean global) throws TimeoutException
boolean isSatisfiable (IVecInt assumps) throws TimeoutException
boolean isSatisfiable (boolean global) throws TimeoutException
boolean isSatisfiable () throws TimeoutException
void learn (Constr c)
boolean model (int var)
int[] model ()
int nConstraints ()
int newVar (int howmany)
int newVar ()
int nVars ()
void printInfos (PrintWriter out, String prefix)
void printStat (PrintWriter out, String prefix)
void printStat (PrintStream out, String prefix)
Constr propagate ()
boolean removeConstr (IConstr co)
void reset ()
final void setDataStructureFactory (D dsf)
void setDBSimplificationAllowed (boolean status)
void setExpectedNumberOfClauses (int nb)
void setOrder (IOrder< L > h)
void setRestartStrategy (RestartStrategy restarter)
void setSearchListener (SearchListener sl)
void setSearchParams (SearchParams sp)
void setSimplifier (ISimplifier simp)
void setSimplifier (String simp)
void setTimeout (int t)
void setTimeoutMs (long t)
void setTimeoutOnConflicts (int count)
boolean simplifyDB ()
 Solver (AssertingClauseGenerator acg, LearningStrategy< L, D > learner, D dsf, SearchParams params, IOrder< L > order, RestartStrategy restarter)
 Solver (AssertingClauseGenerator acg, LearningStrategy< L, D > learner, D dsf, IOrder< L > order, RestartStrategy restarter)
String toString ()
String toString (String prefix)
void varBumpActivity (int p)

Static Public Member Functions

static int decode2dimacs (int p)

Public Attributes


Static Public Attributes

static final ISimplifier NO_SIMPLIFICATION

Protected Member Functions

IConstr addConstr (Constr constr)
void analyzeAtRootLevel (Constr conflict)
void cancelUntil (int level)
void decayActivities ()
IVecInt dimacs2internal (IVecInt in)
int nAssigns ()
void reduceDB (double lim)
void reduceDB ()
void undoOne ()

Protected Attributes

final AssertingClauseGenerator analyzer
int rootLevel
final IVecInt trail = new VecInt()
final IVecInt trailLim = new VecInt()

Package Functions

void modelFound ()
void record (Constr constr)
Lbool search (long nofConflicts)

Private Member Functions

boolean analyzeRemovable (int p)
void cancel ()
void cancelLearntLiterals ()
void claDecayActivity ()
void claRescalActivity ()
void expensiveSimplification (IVecInt outLearnt)
void simpleSimplification (IVecInt outLearnt)
void sortOnActivity ()

Private Attributes

final IVecInt __dimacs_out = new VecInt()
final Pair analysisResult = new Pair()
final IVecInt analyzestack = new VecInt()
final IVecInt analyzetoclear = new VecInt()
double claDecay = 1.0
double claInc = 1.0
final ActivityComparator comparator = new ActivityComparator()
ConflictTimer conflictCount
final IVec< Constrconstrs = new Vec<Constr>()
final Map< String, Integer > constrTypes = new HashMap<String, Integer>()
boolean[] fullmodel
boolean isDBSimplificationAllowed = false
int learnedLiterals = 0
final LearningStrategy< L, D > learner
final IVec< Constrlearnts = new Vec<Constr>()
int[] model = null
boolean[] mseen = new boolean[0]
boolean needToReduceDB
IOrder< L > order
final IVecInt outLearnt = new VecInt()
SearchParams params
final IVecInt preason = new VecInt()
int qhead = 0
RestartStrategy restarter
ISimplifier simplifier = NO_SIMPLIFICATION
SearchListener slistener = new NullSearchListener()
final SolverStats stats = new SolverStats()
boolean timeBasedTimeout = true
double timebegin = 0
long timeout = Integer.MAX_VALUE
transient Timer timer
volatile boolean undertimeout

Static Private Attributes

static final double CLAUSE_RESCALE_FACTOR = 1e-20
static final long serialVersionUID = 1L


interface  ISimplifier

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

Generated by  Doxygen 1.6.0   Back to index