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 |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
instance
public static SolverFactory instance()
- Access to the single instance of the factory.
- Returns:
- the singleton of that class.
newMiniLearning
public static Solver<ILits> newMiniLearning()
- Returns:
- a "default" "minilearning" solver learning clauses of size
smaller than 10 % of the total number of variables
newMiniLearningHeap
public static Solver<ILits> 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 Solver<ILits> newMiniLearningHeapEZSimp()
newMiniLearningHeapExpSimp
public static Solver<ILits> newMiniLearningHeapExpSimp()
newMiniLearningHeapRsatExpSimp
public static Solver<ILits> newMiniLearningHeapRsatExpSimp()
newMiniLearningHeapRsatExpSimpBiere
public static Solver<ILits> newMiniLearningHeapRsatExpSimpBiere()
newMiniLearningHeapRsatExpSimpLuby
public static Solver<ILits> newMiniLearningHeapRsatExpSimpLuby()
newMiniLearning
public static Solver<ILits> 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 <L extends ILits> Solver<L> newMiniLearning(DataStructureFactory<L> 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 <L extends ILits> Solver<L> newMiniLearningHeap(DataStructureFactory<L> 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 Solver<ILits2> 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 Solver<ILits2> newMiniLearning2Heap()
newMiniLearning23
public static Solver<ILits23> 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 Solver<ILits> 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 Solver<ILits> 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 Solver<ILits2> newMiniLearning2NewOrder()
newMiniLearningPure
public static Solver<ILits> 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 Solver<ILits> 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 <L extends ILits> Solver<L> newMiniLearning(DataStructureFactory<L> 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 <L extends ILits> Solver<L> newMiniLearning(DataStructureFactory<L> dsf,
IOrder<L> 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 Solver<ILits> newMiniLearningEZSimp()
newMiniLearningEZSimp
public static <L extends ILits> Solver<L> newMiniLearningEZSimp(DataStructureFactory<L> dsf)
newMiniLearningHeapEZSimpNoRestarts
public static Solver<ILits> newMiniLearningHeapEZSimpNoRestarts()
- Returns:
- a default MiniLearning without restarts.
newMiniLearningHeapEZSimpLongRestarts
public static Solver<ILits> newMiniLearningHeapEZSimpLongRestarts()
- Returns:
- a default MiniLearning with restarts beginning at 1000 conflicts.
newActiveLearning
public static Solver<ILits> 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 Solver<ILits> newMiniSAT()
- Returns:
- a SAT solver very close to the original MiniSAT sat solver.
newMiniSATNoRestarts
public static Solver<ILits> newMiniSATNoRestarts()
- Returns:
- MiniSAT without restarts.
newMiniSAT2
public static Solver<ILits2> newMiniSAT2()
- Returns:
- MiniSAT with a special data structure from Lawrence Ryan thesis
for managing binary clauses.
newMiniSAT23
public static Solver<ILits23> newMiniSAT23()
- Returns:
- MiniSAT with a special data structure from Lawrence Ryan thesis
for managing binary and ternary clauses.
newMiniSAT
public static <L extends ILits> Solver<L> newMiniSAT(DataStructureFactory<L> dsf)
- Parameters:
dsf - the data structure used for representing clauses and lits
- Returns:
- MiniSAT the data structure dsf.
newMiniSATHeap
public static Solver<ILits> newMiniSATHeap()
- Returns:
- a SAT solver very close to the original MiniSAT sat solver.
newMiniSATHeapEZSimp
public static Solver<ILits> newMiniSATHeapEZSimp()
- Returns:
- a SAT solver very close to the original MiniSAT sat solver
including easy reason simplification.
newMiniSATHeapExpSimp
public static Solver<ILits> newMiniSATHeapExpSimp()
newMiniSAT2Heap
public static Solver<ILits2> newMiniSAT2Heap()
- Returns:
- MiniSAT with a special data structure from Lawrence Ryan thesis
for managing binary clauses.
newMiniSAT23Heap
public static Solver<ILits23> newMiniSAT23Heap()
- Returns:
- MiniSAT with a special data structure from Lawrence Ryan thesis
for managing binary and ternary clauses.
newMiniSATHeap
public static <L extends ILits> Solver<L> newMiniSATHeap(DataStructureFactory<L> dsf)
newMiniCard
public static Solver<ILits> newMiniCard()
- Returns:
- MiniSAT with data structures to handle cardinality constraints.
newMinimalOPBMax
public static Solver<ILits> newMinimalOPBMax()
- Returns:
- MiniSAT with Counter-based pseudo boolean constraints and clause
learning.
newMiniOPBMax
public static Solver<ILits> newMiniOPBMax()
- Returns:
- MiniSAT with Counter-based pseudo boolean constraints and
constraint learning.
newMiniOPBClauseCardConstrMax
public static Solver<ILits> 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 Solver<ILits> 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.
newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncremental
public static Solver<ILits> newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncremental()
- Returns:
- MiniLearning 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. Conflict
analysis with full cutting plane inference.
newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalLearnJustClauses
public static Solver<ILits> newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalLearnJustClauses()
- Returns:
- MiniLearning 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. Conflict
analysis with full cutting plane inference. Only clauses are
recorded.
newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause
public static Solver<ILits> newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause()
- Returns:
- MiniLearning 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. Conflict
analysis reduces to clauses to avoid computations
newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalNoLearning
public static Solver<ILits> newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalNoLearning()
- Returns:
- MiniLearning 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. The PB
constraints are not learnt (watched), just used for backjumping.
newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalMerging
public static Solver<ILits> newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalMerging()
- Returns:
- MiniLearning 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. Conflict
analysis uses fusion rule
newMinimalOPBClauseCardConstrMaxSpecificOrder
public static Solver<ILits> newMinimalOPBClauseCardConstrMaxSpecificOrder()
newMiniOPBClauseCardConstrMaxReduceToClause
public static Solver<ILits> 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.
newMiniOPBClauseCardConstrMaxImplied
public static Solver<ILits> 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 Solver<ILits> newMiniOPBClauseAtLeastConstrMax()
- Returns:
- MiniSAT with Counter-based pseudo boolean constraints,
counter-based cardinalities, watched clauses and constraint
learning. methods isAssertive() and getBacktrackLevel() are
totally incremental. Conflicts for PB-constraints use a Map
structure
newMiniOPBCounterBasedClauseCardConstrMax
public static Solver<ILits> newMiniOPBCounterBasedClauseCardConstrMax()
- Returns:
- MiniSAT with Counter-based pseudo boolean constraints and
clauses, watched cardinalities, and constraint learning.
newMinimalOPBMin
public static Solver<ILits> newMinimalOPBMin()
- Returns:
- MiniSAT with WL-based pseudo boolean constraints and clause
learning.
newMiniOPBMin
public static Solver<ILits> newMiniOPBMin()
- Returns:
- MiniSAT with WL-based pseudo boolean constraints and constraint
learning.
newMinimalOPBMinPueblo
public static Solver<ILits> newMinimalOPBMinPueblo()
- Returns:
- MiniSAT with WL-based pseudo boolean constraints and clause
learning.
newMiniOPBMinPueblo
public static Solver<ILits> newMiniOPBMinPueblo()
- Returns:
- MiniSAT with WL-based pseudo boolean constraints and constraint
learning.
newMiniOPBClauseCardMinPueblo
public static Solver<ILits> newMiniOPBClauseCardMinPueblo()
- Returns:
- MiniSAT with WL-based pseudo boolean constraints and clauses,
cardinalities, and constraint learning.
newMiniOPBClauseCardMin
public static Solver<ILits> newMiniOPBClauseCardMin()
- Returns:
- MiniSAT with WL-based pseudo boolean constraints and clauses,
cardinalities, and constraint learning.
newMiniOPBClauseAtLeastMinPueblo
public static Solver<ILits> newMiniOPBClauseAtLeastMinPueblo()
- Returns:
- MiniSAT with WL-based pseudo boolean constraints and clauses,
counter-based cardinalities, and constraint learning.
newRelsat
public static Solver<ILits> newRelsat()
- Returns:
- MiniSAT with decision UIP clause generator.
newBackjumping
public static Solver<ILits> newBackjumping()
- Returns:
- MiniSAT with VSIDS heuristics, FirstUIP clause generator for
backjumping but no learning.
newMini3SAT
public static Solver<ILits23> 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 Solver<ILits23> newMini3SATb()
- Returns:
- a Mini3SAT with full learning.
- See Also:
newMini3SAT()
newMiniMaxSAT
public static Solver<ILits> newMiniMaxSAT()
- Builds a SAT solver for the MAX sat evaluation. Full clause learning, no
restarts,
- Returns:
- a
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()
newDimacsOutput
public static ISolver newDimacsOutput()
Copyright © 2007 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.