org.sat4j.pb
Class SolverFactory

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

All Implemented Interfaces:

java.io.Serializable

public class SolverFactory
extends ASolverFactory<IPBSolver>

User friendly access to pre-constructed solvers.

Author:

leberre

See Also:

Serialized Form

Method Summary

IPBSolver	defaultSolver()
static SolverFactory	instance() Access to the single instance of the factory.
IPBSolver	lightSolver()
static PBSolverCP	newCompetPBCPMixedConstraintsObjective()
static PBSolverCP	newCompetPBCPMixedConstraintsObjectiveLearnJustClauses()
static PBSolverCP	newCompetPBKillerClassic()
static PBSolverCP	newCompetPBKillerFixed()
static PBSolverCP	newCompetPBKillerRSAT()
static PBSolverResolution	newCompetPBResHTMixedConstraintsObjective()
static PBSolverResolution	newCompetPBResHTMixedConstraintsObjectiveExpSimp()
static PBSolverResolution	newCompetPBResMinHTMixedConstraintsObjective()
static PBSolverResolution	newCompetPBResMinHTMixedConstraintsObjectiveExpSimp()
static PBSolverResolution	newCompetPBResMixedConstraintsObjectiveExpSimp()
static IPBSolver	newCuttingPlanes() 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 PBSolverCP	newMiniOPBCounterBasedClauseCardConstrMax()
static IPBSolver	newOPBStringSolver()
static PBSolverCP	newPBCPAllPB()
static PBSolverCP	newPBCPAllPBWL()
static PBSolverCP	newPBCPAllPBWLPueblo()
static PBSolverWithImpliedClause	newPBCPMixedConstrainsImplied()
static PBSolverCP	newPBCPMixedConstraints()
static PBSolverCP	newPBCPMixedConstraintsObjective()
static PBSolverCP	newPBCPMixedConstraintsObjectiveLearnJustClauses()
static PBSolverCP	newPBCPMixedConstraintsObjectiveNoLearning()
static PBSolverClause	newPBCPMixedConstraintsReduceToClause()
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.

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()

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()

newCompetPBResHTMixedConstraintsObjective

public static PBSolverResolution newCompetPBResHTMixedConstraintsObjective()

newPBResHTMixedConstraintsObjective

public static PBSolverResolution newPBResHTMixedConstraintsObjective()

newCompetPBResMinHTMixedConstraintsObjective

public static PBSolverResolution newCompetPBResMinHTMixedConstraintsObjective()

newPBResMinHTMixedConstraintsObjective

public static PBSolverResolution newPBResMinHTMixedConstraintsObjective()

newCompetPBResMixedConstraintsObjectiveExpSimp

public static PBSolverResolution newCompetPBResMixedConstraintsObjectiveExpSimp()

newCompetPBResHTMixedConstraintsObjectiveExpSimp

public static PBSolverResolution newCompetPBResHTMixedConstraintsObjectiveExpSimp()

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.

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

newMiniOPBCounterBasedClauseCardConstrMax

public static PBSolverCP newMiniOPBCounterBasedClauseCardConstrMax()

Returns:

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

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.

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.

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()

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()