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<ILits>	newCompetMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause()
static PBSolverWithImpliedClause	newCompetPBCPMixedConstrainsImplied()
static PBSolverCP<ILits>	newCompetPBCPMixedConstraints()
static PBSolverCP<ILits>	newCompetPBCPMixedConstraintsObjective()
static PBSolverCP<ILits>	newCompetPBCPMixedConstraintsObjectiveLearnJustClauses()
static PBSolverCP<ILits>	newCompetPBCPMixedConstraintsObjectiveNoLearning()
static PBSolverClause	newCompetPBCPMixedConstraintsReduceToClause()
static PBSolverCP<ILits>	newCompetPBKillerClassic()
static PBSolverCP<ILits>	newCompetPBKillerFixed()
static PBSolverCP<ILits>	newCompetPBKillerRSAT()
static PBSolverResolution	newCompetPBResMixedConstraintsObjective()
static PBSolverResolution	newCompetPBResMixedConstraintsObjectiveExpSimp()
static IPBSolver	newDefault() Default solver of the SolverFactory.
static ISolver	newDimacsOutput()
static IPBSolver	newEclipseP2()
static IPBSolver	newLight() Small footprint SAT solver.
static PBSolverCP<ILits>	newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause()
static PBSolverCP<ILits>	newMiniOPBClauseAtLeastConstrMax()
static PBSolverCP<ILits>	newMiniOPBClauseAtLeastMinPueblo()
static PBSolverCP<ILits>	newMiniOPBClauseCardMin()
static PBSolverCP<ILits>	newMiniOPBClauseCardMinPueblo()
static PBSolverCP<ILits>	newMiniOPBCounterBasedClauseCardConstrMax()
static IPBSolver	newOPBStringSolver()
static PBSolverCP<ILits>	newPBCPAllPB()
static PBSolverCP<ILits>	newPBCPAllPBWL()
static PBSolverCP<ILits>	newPBCPAllPBWLPueblo()
static PBSolverWithImpliedClause	newPBCPMixedConstrainsImplied()
static PBSolverCP<ILits>	newPBCPMixedConstraints()
static PBSolverCP<ILits>	newPBCPMixedConstraintsObjective()
static PBSolverCP<ILits>	newPBCPMixedConstraintsObjectiveLearnJustClauses()
static PBSolverCP<ILits>	newPBCPMixedConstraintsObjectiveNoLearning()
static PBSolverClause	newPBCPMixedConstraintsReduceToClause()
static PBSolverCP<ILits>	newPBKillerClassic()
static PBSolverCP<ILits>	newPBKillerFixed()
static PBSolverCP<ILits>	newPBKillerRSAT()
static PBSolverResolution	newPBResAllPB()
static PBSolverResolution	newPBResAllPBWL()
static PBSolverResolution	newPBResAllPBWLPueblo()
static PBSolverResolution	newPBResMixedConstraintsObjective()

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

Returns:

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

newCompetPBCPMixedConstraints

public static PBSolverCP<ILits> newCompetPBCPMixedConstraints()

newPBCPMixedConstraintsObjective

public static PBSolverCP<ILits> 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<ILits> newCompetPBCPMixedConstraintsObjective()

newPBCPMixedConstraintsObjectiveLearnJustClauses

public static PBSolverCP<ILits> 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<ILits> newCompetPBCPMixedConstraintsObjectiveLearnJustClauses()

newPBKillerRSAT

public static PBSolverCP<ILits> newPBKillerRSAT()

newPBKillerClassic

public static PBSolverCP<ILits> newPBKillerClassic()

newPBKillerFixed

public static PBSolverCP<ILits> newPBKillerFixed()

newCompetPBKillerRSAT

public static PBSolverCP<ILits> newCompetPBKillerRSAT()

newCompetPBKillerClassic

public static PBSolverCP<ILits> newCompetPBKillerClassic()

newCompetPBKillerFixed

public static PBSolverCP<ILits> newCompetPBKillerFixed()

newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause

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

newCompetMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause

public static PBSolverCP<ILits> newCompetMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause()

newPBCPMixedConstraintsObjectiveNoLearning

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

newCompetPBCPMixedConstraintsObjectiveNoLearning

public static PBSolverCP<ILits> newCompetPBCPMixedConstraintsObjectiveNoLearning()

newPBResMixedConstraintsObjective

public static PBSolverResolution newPBResMixedConstraintsObjective()

newCompetPBResMixedConstraintsObjective

public static PBSolverResolution newCompetPBResMixedConstraintsObjective()

newCompetPBResMixedConstraintsObjectiveExpSimp

public static PBSolverResolution newCompetPBResMixedConstraintsObjectiveExpSimp()

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.

newCompetPBCPMixedConstraintsReduceToClause

public static PBSolverClause newCompetPBCPMixedConstraintsReduceToClause()

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.

newCompetPBCPMixedConstrainsImplied

public static PBSolverWithImpliedClause newCompetPBCPMixedConstrainsImplied()

newMiniOPBClauseAtLeastConstrMax

public static PBSolverCP<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 PBSolverCP<ILits> 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<ILits> 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<ILits> newPBCPAllPBWLPueblo()

Returns:

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

newMiniOPBClauseCardMinPueblo

public static PBSolverCP<ILits> newMiniOPBClauseCardMinPueblo()

Returns:

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

newMiniOPBClauseCardMin

public static PBSolverCP<ILits> newMiniOPBClauseCardMin()

Returns:

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

newMiniOPBClauseAtLeastMinPueblo

public static PBSolverCP<ILits> newMiniOPBClauseAtLeastMinPueblo()

Returns:

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

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.

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