org.sat4j.pb
Class SolverFactory

java.lang.Object
  org.sat4j.core.ASolverFactory<IPBSolver>
      org.sat4j.pb.SolverFactory

All Implemented Interfaces:

Serializable

public class SolverFactory
extends ASolverFactory<IPBSolver>

User friendly access to pre-constructed solvers.

Since:

2.0

Author:

leberre

See Also:

Serialized Form

Method Summary

IPBSolver	defaultSolver() To obtain the default solver of the library.
static SolverFactory	instance() Access to the single instance of the factory.
IPBSolver	lightSolver() To obtain a solver that is suitable for solving many small instances of SAT problems.
static IPBSolver	newBoth() Resolution and CuttingPlanes based solvers running in parallel.
static PBSolverResolution	newCompetMinPBResLongWLMixedConstraintsObjectiveExpSimp()
static PBSolverCP	newCompetPBCPMixedConstraintsLongMaxObjective()
static PBSolverCP	newCompetPBCPMixedConstraintsLongMinObjective()
static PBSolverCP	newCompetPBCPMixedConstraintsMinObjective()
static PBSolverCP	newCompetPBCPMixedConstraintsObjective()
static PBSolverCP	newCompetPBCPMixedConstraintsObjectiveLearnJustClauses()
static PBSolverCP	newCompetPBKillerClassic()
static PBSolverCP	newCompetPBKillerFixed()
static PBSolverCP	newCompetPBKillerRSAT()
static PBSolverResolution	newCompetPBResHTMixedConstraintsObjectiveExpSimp()
static PBSolverResolution	newCompetPBResLongHTMixedConstraintsObjectiveExpSimp()
static PBSolverResolution	newCompetPBResLongWLMixedConstraintsObjectiveExpSimp()
static PBSolverResolution	newCompetPBResMinHTMixedConstraintsObjective()
static PBSolverResolution	newCompetPBResMinHTMixedConstraintsObjectiveExpSimp()
static PBSolverResolution	newCompetPBResMixedConstraintsObjectiveExpSimp()
static PBSolverResolution	newCompetPBResMixedConstraintsObjectiveExpSimp(PBDataStructureFactory dsf)
static PBSolverResolution	newCompetPBResWLMixedConstraintsObjectiveExpSimp()
static IPBSolver	newCuttingPlanes() Cutting Planes based solver.
static IPBSolver	newCuttingPlanesAggressiveCleanup() Cutting Planes based solver.
static IPBSolver	newDefault() Default solver of the SolverFactory.
static IPBSolver	newDefaultNonNormalized() Default solver of the SolverFactory for instances not normalized.
static ISolver	newDimacsOutput()
static IPBSolver	newEclipseP2()
static IPBSolver	newLight() Small footprint SAT solver.
static PBSolverCP	newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause()
static PBSolverCP	newMiniOPBClauseAtLeastConstrMax()
static PBSolverCP	newMiniOPBClauseAtLeastMinPueblo()
static PBSolverCP	newMiniOPBClauseCardMin()
static PBSolverCP	newMiniOPBClauseCardMinPueblo()
static IPBSolver	newOPBStringSolver()
static PBSolverCP	newPBCPAllPB()
static PBSolverCP	newPBCPAllPBWL()
static PBSolverCP	newPBCPAllPBWLPueblo()
static PBSolverWithImpliedClause	newPBCPMixedConstrainsImplied()
static PBSolverCP	newPBCPMixedConstraints()
static PBSolverCautious	newPBCPMixedConstraintsCautious()
static PBSolverCautious	newPBCPMixedConstraintsCautious(int bound)
static PBSolverCP	newPBCPMixedConstraintsObjective()
static PBSolverCP	newPBCPMixedConstraintsObjectiveLearnJustClauses()
static PBSolverCP	newPBCPMixedConstraintsObjectiveNoLearning()
static PBSolverClause	newPBCPMixedConstraintsReduceToClause()
static PBSolverResCP	newPBCPMixedConstraintsResCP()
static PBSolverResCP	newPBCPMixedConstraintsResCP(long bound)
static PBSolverCP	newPBKillerClassic()
static PBSolverCP	newPBKillerFixed()
static PBSolverCP	newPBKillerRSAT()
static PBSolverResolution	newPBResAllPB()
static PBSolverResolution	newPBResAllPBWL()
static PBSolverResolution	newPBResAllPBWLPueblo()
static PBSolverResolution	newPBResHTMixedConstraintsObjective()
static PBSolverResolution	newPBResHTMixedConstraintsObjectiveExpSimp()
static PBSolverResolution	newPBResMinHTMixedConstraintsObjective()
static PBSolverResolution	newPBResMixedConstraintsObjective()
static IPBSolver	newResolution() Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
static PBSolverResolution	newResolutionGlucose() Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
static PBSolverResolution	newResolutionGlucoseExpSimp() Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
static PBSolverResolution	newResolutionGlucoseSimpleSimp() Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
static IPBSolver	newResolutionMaxMemory() Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
static IPBSolver	newResolutionSimpleRestarts() Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
static IPBSolver	newSimpleSimplification() Resolution based solver (i.e. classic SAT solver able to handle generic constraints.

Methods inherited from class org.sat4j.core.ASolverFactory

createSolverByName, solverNames

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

instance

public static SolverFactory instance()

Access to the single instance of the factory.

Returns:

the singleton of that class.

newPBResAllPB

public static PBSolverResolution newPBResAllPB()

Returns:

MiniSAT with Counter-based pseudo boolean constraints and clause learning.

newPBCPAllPB

public static PBSolverCP newPBCPAllPB()

Returns:

MiniSAT with Counter-based pseudo boolean constraints and constraint learning.

newOPBStringSolver

public static IPBSolver newOPBStringSolver()

Returns:

Solver used to display in a string the pb-instance in OPB format.

newPBCPMixedConstraints

public static PBSolverCP newPBCPMixedConstraints()

Returns:

MiniSAT with Counter-based pseudo boolean constraints and constraint learning. Clauses and cardinalities with watched literals are also handled (and learnt).

newPBCPMixedConstraintsObjective

public static PBSolverCP newPBCPMixedConstraintsObjective()

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.

newCompetPBCPMixedConstraintsObjective

public static PBSolverCP newCompetPBCPMixedConstraintsObjective()

newCompetPBCPMixedConstraintsMinObjective

public static PBSolverCP newCompetPBCPMixedConstraintsMinObjective()

newCompetPBCPMixedConstraintsLongMaxObjective

public static PBSolverCP newCompetPBCPMixedConstraintsLongMaxObjective()

newCompetPBCPMixedConstraintsLongMinObjective

public static PBSolverCP newCompetPBCPMixedConstraintsLongMinObjective()

newPBCPMixedConstraintsObjectiveLearnJustClauses

public static PBSolverCP newPBCPMixedConstraintsObjectiveLearnJustClauses()

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.

newCompetPBCPMixedConstraintsObjectiveLearnJustClauses

public static PBSolverCP newCompetPBCPMixedConstraintsObjectiveLearnJustClauses()

newPBKillerRSAT

public static PBSolverCP newPBKillerRSAT()

newPBKillerClassic

public static PBSolverCP newPBKillerClassic()

newPBKillerFixed

public static PBSolverCP newPBKillerFixed()

newCompetPBKillerRSAT

public static PBSolverCP newCompetPBKillerRSAT()

newCompetPBKillerClassic

public static PBSolverCP newCompetPBKillerClassic()

newCompetPBKillerFixed

public static PBSolverCP newCompetPBKillerFixed()

newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause

public static PBSolverCP 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

newPBCPMixedConstraintsObjectiveNoLearning

public static PBSolverCP newPBCPMixedConstraintsObjectiveNoLearning()

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.

newPBResMixedConstraintsObjective

public static PBSolverResolution newPBResMixedConstraintsObjective()

newCompetPBResWLMixedConstraintsObjectiveExpSimp

public static PBSolverResolution newCompetPBResWLMixedConstraintsObjectiveExpSimp()

newCompetPBResHTMixedConstraintsObjectiveExpSimp

public static PBSolverResolution newCompetPBResHTMixedConstraintsObjectiveExpSimp()

newCompetPBResLongHTMixedConstraintsObjectiveExpSimp

public static PBSolverResolution newCompetPBResLongHTMixedConstraintsObjectiveExpSimp()

newCompetPBResLongWLMixedConstraintsObjectiveExpSimp

public static PBSolverResolution newCompetPBResLongWLMixedConstraintsObjectiveExpSimp()

newCompetMinPBResLongWLMixedConstraintsObjectiveExpSimp

public static PBSolverResolution newCompetMinPBResLongWLMixedConstraintsObjectiveExpSimp()

newCompetPBResMixedConstraintsObjectiveExpSimp

public static PBSolverResolution newCompetPBResMixedConstraintsObjectiveExpSimp(PBDataStructureFactory dsf)

newPBResHTMixedConstraintsObjective

public static PBSolverResolution newPBResHTMixedConstraintsObjective()

newCompetPBResMinHTMixedConstraintsObjective

public static PBSolverResolution newCompetPBResMinHTMixedConstraintsObjective()

newPBResMinHTMixedConstraintsObjective

public static PBSolverResolution newPBResMinHTMixedConstraintsObjective()

newCompetPBResMixedConstraintsObjectiveExpSimp

public static PBSolverResolution newCompetPBResMixedConstraintsObjectiveExpSimp()

newPBResHTMixedConstraintsObjectiveExpSimp

public static PBSolverResolution newPBResHTMixedConstraintsObjectiveExpSimp()

newCompetPBResMinHTMixedConstraintsObjectiveExpSimp

public static PBSolverResolution newCompetPBResMinHTMixedConstraintsObjectiveExpSimp()

newPBCPMixedConstraintsReduceToClause

public static PBSolverClause newPBCPMixedConstraintsReduceToClause()

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.

newPBCPMixedConstraintsCautious

public static PBSolverCautious newPBCPMixedConstraintsCautious(int bound)

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 (if coefficients are larger than bound).

newPBCPMixedConstraintsCautious

public static PBSolverCautious newPBCPMixedConstraintsCautious()

newPBCPMixedConstraintsResCP

public static PBSolverResCP newPBCPMixedConstraintsResCP(long bound)

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 (if coefficients are larger than bound).

newPBCPMixedConstraintsResCP

public static PBSolverResCP newPBCPMixedConstraintsResCP()

newPBCPMixedConstrainsImplied

public static PBSolverWithImpliedClause newPBCPMixedConstrainsImplied()

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 PBSolverCP 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

newPBResAllPBWL

public static PBSolverResolution newPBResAllPBWL()

Returns:

MiniSAT with WL-based pseudo boolean constraints and clause learning.

newPBCPAllPBWL

public static PBSolverCP newPBCPAllPBWL()

Returns:

MiniSAT with WL-based pseudo boolean constraints and constraint learning.

newPBResAllPBWLPueblo

public static PBSolverResolution newPBResAllPBWLPueblo()

Returns:

MiniSAT with WL-based pseudo boolean constraints and clause learning.

newPBCPAllPBWLPueblo

public static PBSolverCP newPBCPAllPBWLPueblo()

Returns:

MiniSAT with WL-based pseudo boolean constraints and constraint learning.

newMiniOPBClauseCardMinPueblo

public static PBSolverCP newMiniOPBClauseCardMinPueblo()

Returns:

MiniSAT with WL-based pseudo boolean constraints and clauses, cardinalities, and constraint learning.

newMiniOPBClauseCardMin

public static PBSolverCP newMiniOPBClauseCardMin()

Returns:

MiniSAT with WL-based pseudo boolean constraints and clauses, cardinalities, and constraint learning.

newMiniOPBClauseAtLeastMinPueblo

public static PBSolverCP newMiniOPBClauseAtLeastMinPueblo()

Returns:

MiniSAT with WL-based pseudo boolean constraints and clauses, counter-based cardinalities, and constraint learning.

newCuttingPlanes

public static IPBSolver newCuttingPlanes()

Cutting Planes based solver. The inference during conflict analysis is based on cutting planes instead of resolution as in a SAT solver.

Returns:

the best available cutting planes based solver of the library.

newCuttingPlanesAggressiveCleanup

public static IPBSolver newCuttingPlanesAggressiveCleanup()

Cutting Planes based solver. The inference during conflict analysis is based on cutting planes instead of resolution as in a SAT solver.

Returns:

the best available cutting planes based solver of the library.

newResolution

public static IPBSolver newResolution()

Resolution based solver (i.e. classic SAT solver able to handle generic constraints. No specific inference mechanism.

Returns:

the best available resolution based solver of the library.

newBoth

public static IPBSolver newBoth()

Resolution and CuttingPlanes based solvers running in parallel. Does only make sense if run on a computer with several cores.

Returns:

a parallel solver using both resolution and cutting planes proof system.

newResolutionGlucose

public static PBSolverResolution newResolutionGlucose()

Resolution based solver (i.e. classic SAT solver able to handle generic constraints. No specific inference mechanism). Uses glucose based memory management. The reason simplification is now disabled by default because it slows down a lot when long PB or cardinality constraints are used.

Returns:

the best available resolution based solver of the library.

newResolutionGlucoseSimpleSimp

public static PBSolverResolution newResolutionGlucoseSimpleSimp()

Resolution based solver (i.e. classic SAT solver able to handle generic constraints. No specific inference mechanism). Uses glucose based memory management.

Returns:

the best available resolution based solver of the library.

newResolutionGlucoseExpSimp

public static PBSolverResolution newResolutionGlucoseExpSimp()

Resolution based solver (i.e. classic SAT solver able to handle generic constraints. No specific inference mechanism). Uses glucose based memory management. It uses the expensive reason simplification. If the problem contains long PB or cardinality constraints, it might be slowed down by such treatment.

Returns:

the best available resolution based solver of the library.

newSimpleSimplification

public static IPBSolver newSimpleSimplification()

Resolution based solver (i.e. classic SAT solver able to handle generic constraints. No specific inference mechanism). Uses glucose based memory management.

Returns:

the best available resolution based solver of the library.

newResolutionSimpleRestarts

public static IPBSolver newResolutionSimpleRestarts()

Resolution based solver (i.e. classic SAT solver able to handle generic constraints. No specific inference mechanism). Uses glucose based memory management. Uses a simple restart strategy (original Minisat's one).

Returns:

the best available resolution based solver of the library.

newResolutionMaxMemory

public static IPBSolver newResolutionMaxMemory()

Resolution based solver (i.e. classic SAT solver able to handle generic constraints. No specific inference mechanism). Keeps the constraints as long as there is enough memory available.

Returns:

the best available resolution based solver of the library.

newDefault

public static IPBSolver 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.

newDefaultNonNormalized

public static IPBSolver newDefaultNonNormalized()

Default solver of the SolverFactory for instances not normalized. 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 IPBSolver 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<IPBSolver>

Returns:

a solver from the factory

See Also:

ASolverFactory.lightSolver()

newLight

public static IPBSolver 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 IPBSolver 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<IPBSolver>

Returns:

a solver from the factory

See Also:

ASolverFactory.defaultSolver()

newDimacsOutput

public static ISolver newDimacsOutput()

newEclipseP2

public static IPBSolver newEclipseP2()