org.sat4j.pb
Class SolverFactory

java.lang.Object
  extended by org.sat4j.core.ASolverFactory<IPBSolver>
      extended by 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
 PBSolver defaultSolver()
           
static SolverFactory instance()
          Access to the single instance of the factory.
 IPBSolver lightSolver()
           
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 PBSolver 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 PBSolverResolution newSAT()
          That solver is expected to perform better on satisfiable benchmarks.
static IPBSolver newSATUNSAT()
          Two solvers are running in //: one for solving SAT instances, the other one for solving unsat instances.
static IPBSolver newSimpleSimplification()
          Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
static PBSolverResolution newUNSAT()
          That solver is expected to perform better on unsatisfiable benchmarks.
 
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.

newSATUNSAT

public static IPBSolver newSATUNSAT()
Two solvers are running in //: one for solving SAT instances, the other one for solving unsat instances.

Returns:
a parallel solver for both SAT and UNSAT problems.

newSAT

public static PBSolverResolution newSAT()
That solver is expected to perform better on satisfiable benchmarks.

Returns:
a solver for satisfiable benchmarks.

newUNSAT

public static PBSolverResolution newUNSAT()
That solver is expected to perform better on unsatisfiable benchmarks.

Returns:
a solver for unsatisfiable benchmarks.

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 PBSolver 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 PBSolver defaultSolver()
Specified by:
defaultSolver in class ASolverFactory<IPBSolver>

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()
Specified by:
lightSolver in class ASolverFactory<IPBSolver>

newDimacsOutput

public static ISolver newDimacsOutput()

newEclipseP2

public static IPBSolver newEclipseP2()


Copyright © 2012 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.