org.sat4j.minisat
Class SolverFactory
java.lang.Object
org.sat4j.core.ASolverFactory
org.sat4j.minisat.SolverFactory
- All Implemented Interfaces:
- java.io.Serializable
public class SolverFactory
- extends ASolverFactory
- implements java.io.Serializable
User friendly access to pre-constructed solvers.
- Author:
- leberre
- See Also:
- Serialized Form
| Methods inherited from class java.lang.Object |
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
instance
public static SolverFactory instance()
- Access to the single instance of the factory.
- Returns:
- the singleton for that class.
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)
newMiniLearningHeapEZSimpNoRestarts
public static ISolver newMiniLearningHeapEZSimpNoRestarts()
- Returns:
- a default MiniLearning without restarts.
newMiniLearningHeapEZSimpLongRestarts
public static ISolver newMiniLearningHeapEZSimpLongRestarts()
- Returns:
- a default MiniLearning with restarts beginning at 1000 conflicts.
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.
newMiniSATHeapEZSimp
public static ISolver newMiniSATHeapEZSimp()
- Returns:
- a SAT solver very close to the original MiniSAT sat solver
including easy reason simplification.
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 structures 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.
newMiniOPBClauseCardConstrMax
public static ISolver newMiniOPBClauseCardConstrMax()
- Returns:
- MiniSAT with Counter-based pseudo boolean constraints and
constraint learning. Clauses and cardinalities with watched
literals are also handled (and learnt).
newMiniOPBClauseCardConstrMaxSpecificOrder
public static ISolver newMiniOPBClauseCardConstrMaxSpecificOrder()
- Returns:
- MiniSAT with Counter-based pseudo boolean constraints and
constraint learning. Clauses and cardinalities with watched
literals are also handled (and learnt). A specific heuristics
taking into account the objective value is used.
newMiniOPBClauseCardConstrMaxReduceToClause
public static ISolver newMiniOPBClauseCardConstrMaxReduceToClause()
- Returns:
- MiniSAT with Counter-based pseudo boolean constraints and
constraint learning. Clauses and cardinalities with watched
literals are also handled (and learnt). A reduction of
PB-constraints to clauses is made in order to simplify cutting
planes.
newMiniOPBClauseCardConstrMaxReduceToCard
public static ISolver newMiniOPBClauseCardConstrMaxReduceToCard()
- Returns:
- MiniSAT with Counter-based pseudo boolean constraints and
constraint learning. Clauses and cardinalities with watched
literals are also handled (and learnt). A reduction of
PB-constraints to cardinalities is made in order to simplify
cutting planes.
newMiniOPBClauseCardConstrMaxImplied
public static ISolver newMiniOPBClauseCardConstrMaxImplied()
- Returns:
- MiniSAT with Counter-based pseudo boolean constraints and
constraint learning. Clauses and cardinalities with watched
literals are also handled (and learnt). a pre-processing is
applied which adds implied clauses from PB-constraints.
newMiniOPBClauseAtLeastConstrMax
public static ISolver newMiniOPBClauseAtLeastConstrMax()
- Returns:
- MiniSAT with Counter-based pseudo boolean constraints,
counter-based cardinalities, watched clauses and constraint
learning.
newMiniOPBCounterBasedClauseCardConstrMax
public static ISolver newMiniOPBCounterBasedClauseCardConstrMax()
- Returns:
- MiniSAT with Counter-based pseudo boolean constraints and
clauses, watched cardinalities, 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.
newMinimalOPBMinPueblo
public static ISolver newMinimalOPBMinPueblo()
- Returns:
- MiniSAT with WL-based pseudo boolean constraints and clause
learning.
newMiniOPBMinPueblo
public static ISolver newMiniOPBMinPueblo()
- Returns:
- MiniSAT with WL-based pseudo boolean constraints and constraint
learning.
newMiniOPBClauseCardMinPueblo
public static ISolver newMiniOPBClauseCardMinPueblo()
- Returns:
- MiniSAT with WL-based pseudo boolean constraints and clauses,
cardinalities, and constraint learning.
newMiniOPBClauseCardMin
public static ISolver newMiniOPBClauseCardMin()
- Returns:
- MiniSAT with WL-based pseudo boolean constraints and clauses,
cardinalities, and constraint learning.
newMiniOPBClauseAtLeastMinPueblo
public static ISolver newMiniOPBClauseAtLeastMinPueblo()
- Returns:
- MiniSAT with WL-based pseudo boolean constraints and clauses,
counter-based cardinalities, 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()
newAdaptiveSolver
public static ISolver newAdaptiveSolver()
- A SAT solver that adapts its data structures according to the problem
to solve.
- Returns:
- a MiniLearningHeapEZSimp solver decorated with a SATRaceDecorator.
newDefault
public static ISolver newDefault()
- Default solver of the SolverFactory. This solver is meant to be used on
challenging SAT benchmarks.
- Returns:
- the best "general purpose" SAT solver available in the factory.
- See Also:
the same method, polymorphic, to be called from an
instance of ASolverFactory.
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()
newLight
public static ISolver newLight()
- Small footprint SAT solver.
- Returns:
- a SAT solver suitable for solving small/easy SAT benchmarks.
- See Also:
the same method, polymorphic, to be called from an
instance of ASolverFactory.
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()