public abstract class SatSolver extends java.lang.Object implements BeliefSetConsistencyTester<PropositionalFormula>, ConsistencyWitnessProvider<PlBeliefSet,PropositionalFormula>
Modifier and Type | Field and Description |
---|---|
private static SatSolver |
defaultSatSolver
The default SAT solver.
|
private static java.io.File |
tempFolder
For temporary files.
|
Constructor and Description |
---|
SatSolver() |
Modifier and Type | Method and Description |
---|---|
protected static Pair<java.lang.String,java.util.List<PropositionalFormula>> |
convertToDimacs(java.util.Collection<PropositionalFormula> formulas)
Converts the given set of formulas to their string representation in
Dimacs CNF.
|
protected static java.lang.String |
convertToDimacs(java.util.Collection<PropositionalFormula> formulas,
java.util.List<Proposition> props)
Converts the given set of formulas to their string representation in
Dimacs CNF.
|
protected static Pair<java.io.File,java.util.List<PropositionalFormula>> |
createTmpDimacsFile(java.util.Collection<PropositionalFormula> formulas)
Creates a temporary file in Dimacs format and also returns a mapping between formulas and clauses.
|
protected static java.io.File |
createTmpDimacsFile(java.util.Collection<PropositionalFormula> formulas,
java.util.List<Proposition> props)
Creates a temporary file in Dimacs format with the given proposition2variable mapping.
|
static SatSolver |
getDefaultSolver()
Returns the default SAT solver.
If a default SAT solver has been configured this solver
is returned by this method.
|
Interpretation<PlBeliefSet,PropositionalFormula> |
getWitness(BeliefSet<PropositionalFormula> bs)
If the belief set is consistent this method
returns some model of it or, if it is inconsistent, null.
|
abstract Interpretation<PlBeliefSet,PropositionalFormula> |
getWitness(java.util.Collection<PropositionalFormula> formulas)
If the collection of formulas is consistent this method
returns some model of it or, if it is inconsistent, null.
|
Interpretation<PlBeliefSet,PropositionalFormula> |
getWitness(PropositionalFormula formula)
If the formula is consistent this method
returns some model of it or, if it is inconsistent, null.
|
static boolean |
hasDefaultSolver()
Returns "true" if a default SAT solver is configured.
|
boolean |
isConsistent(BeliefSet<PropositionalFormula> beliefSet)
Checks whether the given belief base is consistent.
|
boolean |
isConsistent(java.util.Collection<PropositionalFormula> formulas)
Checks whether the given collection of formulas is consistent.
|
boolean |
isConsistent(PropositionalFormula formula)
Checks whether the given formula is consistent.
|
abstract boolean |
isSatisfiable(java.util.Collection<PropositionalFormula> formulas)
Checks whether the given set of formulas is satisfiable.
|
static void |
setDefaultSolver(SatSolver solver)
Sets the default SAT solver.
|
static void |
setTempFolder(java.io.File tempFolder)
Set the folder for temporary files created by SAT solver.
|
private static SatSolver defaultSatSolver
private static java.io.File tempFolder
public static void setDefaultSolver(SatSolver solver)
solver
- some SAT solverpublic static void setTempFolder(java.io.File tempFolder)
tempFolder
- some temp folder.public static boolean hasDefaultSolver()
public static SatSolver getDefaultSolver()
net.sf.tweety.pl.sat.Sat4jSolver
)
is returned as a fallback and a message is
printed to stderr pointing out that no default SAT solver is configured.protected static java.lang.String convertToDimacs(java.util.Collection<PropositionalFormula> formulas, java.util.List<Proposition> props)
convertToDimacs(.)
for
obtaining a map between those.formulas
- a collection of formulasa
- list of propositions (=signature) where the indices are used for writing the clauses.protected static Pair<java.lang.String,java.util.List<PropositionalFormula>> convertToDimacs(java.util.Collection<PropositionalFormula> formulas)
formulas
- a collection of formulas.protected static java.io.File createTmpDimacsFile(java.util.Collection<PropositionalFormula> formulas, java.util.List<Proposition> props) throws java.io.IOException
formulas
- a collection of formulasa
- list of propositions (=signature) where the indices are used for writing the clauses.java.io.IOException
- if something went wrong while creating a temporary file.protected static Pair<java.io.File,java.util.List<PropositionalFormula>> createTmpDimacsFile(java.util.Collection<PropositionalFormula> formulas) throws java.io.IOException
formulas
- a collection of formulasa
- list of propositions (=signature) where the indices are used for writing the clauses
(a list of collections of formulas (all from the given set); the interpretation of this list
is that the generated clause no K originated from the propositional formula given at index k).java.io.IOException
- if something went wrong while creating a temporary file.public abstract Interpretation<PlBeliefSet,PropositionalFormula> getWitness(java.util.Collection<PropositionalFormula> formulas)
getWitness
in interface ConsistencyWitnessProvider<PlBeliefSet,PropositionalFormula>
public abstract boolean isSatisfiable(java.util.Collection<PropositionalFormula> formulas)
formulas
- a set of formulas.public boolean isConsistent(BeliefSet<PropositionalFormula> beliefSet)
ConsistencyTester
isConsistent
in interface BeliefSetConsistencyTester<PropositionalFormula>
isConsistent
in interface ConsistencyTester<BeliefSet<PropositionalFormula>>
beliefSet
- a belief base.public boolean isConsistent(java.util.Collection<PropositionalFormula> formulas)
BeliefSetConsistencyTester
isConsistent
in interface BeliefSetConsistencyTester<PropositionalFormula>
formulas
- a collection of formulas.public boolean isConsistent(PropositionalFormula formula)
BeliefSetConsistencyTester
isConsistent
in interface BeliefSetConsistencyTester<PropositionalFormula>
formula
- a formulas.public Interpretation<PlBeliefSet,PropositionalFormula> getWitness(PropositionalFormula formula)
ConsistencyWitnessProvider
getWitness
in interface ConsistencyWitnessProvider<PlBeliefSet,PropositionalFormula>
public Interpretation<PlBeliefSet,PropositionalFormula> getWitness(BeliefSet<PropositionalFormula> bs)
ConsistencyWitnessProvider
getWitness
in interface ConsistencyWitnessProvider<PlBeliefSet,PropositionalFormula>