org.sat4j.minisat
Class SolverFactory
java.lang.Object
org.sat4j.core.ASolverFactory
org.sat4j.minisat.SolverFactory
public class SolverFactory
- extends ASolverFactory
User friendly access to pre-constructed solvers.
- Author:
- leberre
| Methods inherited from class java.lang.Object |
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
SolverFactory
public SolverFactory()
newMiniLearning
public static ISolver newMiniLearning()
- Returns:
- a "default" "minilearning" solver learning clauses of size
smaller than 10 % of the total number of variables
newMiniLearningHeap
public static ISolver newMiniLearningHeap()
- Returns:
- a "default" "minilearning" solver learning clauses of size
smaller than 10 % of the total number of variables with a heap
based var order.
newMiniLearningHeapEZSimp
public static ISolver newMiniLearningHeapEZSimp()
newMiniLearning
public static ISolver newMiniLearning(int n)
- Parameters:
n - the maximal size of the clauses to learn as a percentage of
the initial number of variables
- Returns:
- a "minilearning" solver learning clauses of size smaller than n
of the total number of variables
newMiniLearning
public static ISolver newMiniLearning(DataStructureFactory dsf)
- Parameters:
dsf - a specific data structure factory
- Returns:
- a default "minilearning" solver using a specific data structure
factory, learning clauses of length smaller or equals to 10 % of
the number of variables.
newMiniLearningHeap
public static ISolver newMiniLearningHeap(DataStructureFactory dsf)
- Parameters:
dsf - a specific data structure factory
- Returns:
- a default "minilearning" solver using a specific data structure
factory, learning clauses of length smaller or equals to 10 % of
the number of variables and a heap based VSIDS heuristics
newMiniLearning2
public static ISolver newMiniLearning2()
- Returns:
- a default minilearning solver using a specific data structure
described in Lawrence Ryan thesis to handle binary clauses.
- See Also:
newMiniLearning()
newMiniLearning2Heap
public static ISolver newMiniLearning2Heap()
newMiniLearning23
public static ISolver newMiniLearning23()
- Returns:
- a default minilearning solver using a specific data structures
described in Lawrence Ryan thesis to handle binary and ternary
clauses.
- See Also:
newMiniLearning()
newMiniLearningCB
public static ISolver newMiniLearningCB()
- Returns:
- a default minilearning SAT solver using counter-based clause
representation (i.e. all the literals of a clause are watched)
newMiniLearningCBWL
public static ISolver newMiniLearningCBWL()
- Returns:
- a default minilearning SAT solver using counter-based clause
representation (i.e. all the literals of a clause are watched)
for the ORIGINAL clauses and watched-literals clause
representation for learnt clauses.
newMiniLearning2NewOrder
public static ISolver newMiniLearning2NewOrder()
newMiniLearningPure
public static ISolver newMiniLearningPure()
- Returns:
- a default minilearning SAT solver choosing periodically to branch
on "pure watched" literals if any. (a pure watched literal l is a
literal that is watched on at least one clause such that its
negation is not watched at all. It is not necessarily a watched
literal.)
newMiniLearningCBWLPure
public static ISolver newMiniLearningCBWLPure()
- Returns:
- a default minilearning SAT solver choosing periodically to branch
on literal "pure in the original set of clauses" if any.
newMiniLearning
public static ISolver newMiniLearning(DataStructureFactory dsf,
int n)
- Parameters:
dsf - the data structure factory used to represent literals and
clausesn - the maximum size of learnt clauses as percentage of the
original number of variables.
- Returns:
- a SAT solver with learning limited to clauses of length smaller
or equal to n, the dsf data structure, the FirstUIP clause
generator and a sort of VSIDS heuristics.
newMiniLearning
public static ISolver newMiniLearning(DataStructureFactory dsf,
IOrder order)
- Parameters:
dsf - the data structure factory used to represent literals and
clausesorder - the heuristics
- Returns:
- a SAT solver with learning limited to clauses of length smaller
or equal to 10 percent of the total number of variables, the dsf
data structure, the FirstUIP clause generator and order as
heuristics.
newMiniLearningEZSimp
public static ISolver newMiniLearningEZSimp()
newMiniLearningEZSimp
public static ISolver newMiniLearningEZSimp(DataStructureFactory dsf)
newMiniLearningNoRestarts
public static ISolver newMiniLearningNoRestarts()
- Returns:
- a default MiniLearning without restarts.
newActiveLearning
public static ISolver newActiveLearning()
- Returns:
- a SAT solver using First UIP clause generator, watched literals,
VSIDS like heuristics learning only clauses having a great number
of active variables, i.e. variables with an activity strictly
greater than one.
newMiniSAT
public static ISolver newMiniSAT()
- Returns:
- a SAT solver very close to the original MiniSAT sat solver.
newMiniSATNoRestarts
public static ISolver newMiniSATNoRestarts()
- Returns:
- MiniSAT without restarts.
newMiniSAT2
public static ISolver newMiniSAT2()
- Returns:
- MiniSAT with a special data structure from Lawrence Ryan thesis
for managing binary clauses.
newMiniSAT23
public static ISolver newMiniSAT23()
- Returns:
- MiniSAT with a special data structure from Lawrence Ryan thesis
for managing binary and ternary clauses.
newMiniSAT
public static ISolver newMiniSAT(DataStructureFactory dsf)
- Parameters:
dsf - the data structure used for representing clauses and lits
- Returns:
- MiniSAT the data structure dsf.
newMiniSATHeap
public static ISolver newMiniSATHeap()
- Returns:
- a SAT solver very close to the original MiniSAT sat solver.
newMiniSAT2Heap
public static ISolver newMiniSAT2Heap()
- Returns:
- MiniSAT with a special data structure from Lawrence Ryan thesis
for managing binary clauses.
newMiniSAT23Heap
public static ISolver newMiniSAT23Heap()
- Returns:
- MiniSAT with a special data structure from Lawrence Ryan thesis
for managing binary and ternary clauses.
newMiniSATHeap
public static ISolver newMiniSATHeap(DataStructureFactory dsf)
newMiniCard
public static ISolver newMiniCard()
- Returns:
- MiniSAT with data strcutures to handle cardinality constraints.
newMinimalOPBMax
public static ISolver newMinimalOPBMax()
- Returns:
- MiniSAT with Counter-based pseudo boolean constraints and clause
learning.
newMiniOPBMax
public static ISolver newMiniOPBMax()
- Returns:
- MiniSAT with Counter-based pseudo boolean constraints and
constraint learning.
newMinimalOPBMin
public static ISolver newMinimalOPBMin()
- Returns:
- MiniSAT with WL-based pseudo boolean constraints and clause
learning.
newMiniOPBMin
public static ISolver newMiniOPBMin()
- Returns:
- MiniSAT with WL-based pseudo boolean constraints and constraint
learning.
newRelsat
public static ISolver newRelsat()
- Returns:
- MiniSAT with decision UIP clause generator.
newBackjumping
public static ISolver newBackjumping()
- Returns:
- MiniSAT with VSIDS heuristics, FirstUIP clause generator for
backjumping but no learning.
newMini3SAT
public static ISolver newMini3SAT()
- Returns:
- a SAT solver with learning limited to clauses of length smaller
or equals to 3, with a specific data structure for binary and
ternary clauses as found in Lawrence Ryan thesis, without
restarts, with a Jeroslow/Wang kind of heuristics.
newMini3SATb
public static ISolver newMini3SATb()
- Returns:
- a Mini3SAT with full learning.
- See Also:
newMini3SAT()
defaultSolver
public ISolver defaultSolver()
- Description copied from class:
ASolverFactory
- To obtain the default solver of the library.
The solver is suitable to solve huge SAT benchmarks.
It should reflect state-of-the-art SAT technologies.
For solving small/easy SAT benchmarks, use lightSolver() instead.
- Specified by:
defaultSolver in class ASolverFactory
- Returns:
- a solver from the factory
- See Also:
ASolverFactory.lightSolver()
lightSolver
public ISolver lightSolver()
- Description copied from class:
ASolverFactory
- To obtain a solver that is suitable for solving
many small instances of SAT problems.
The solver is not using sophisticated but costly
reasoning and avoids to allocate too much memory.
For solving bigger SAT benchmarks, use defaultSolver() instead.
- Specified by:
lightSolver in class ASolverFactory
- Returns:
- a solver from the factory
- See Also:
ASolverFactory.defaultSolver()