Package net.sf.tweety.logics.pl.sat
Class SatSolver
- java.lang.Object
-
- net.sf.tweety.logics.pl.sat.SatSolver
-
- All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>
,ConsistencyTester<BeliefSet<PlFormula,?>>
,ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
- Direct Known Subclasses:
IncrementalSatSolver
,LingelingSolver
,MaxSatSolver
,Sat4jSolver
,SimpleDpllSolver
public abstract class SatSolver extends java.lang.Object implements BeliefSetConsistencyTester<PlFormula>, ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
Abstract class for specifying SAT solvers.- Author:
- Matthias Thimm
-
-
Constructor Summary
Constructors Constructor Description SatSolver()
-
Method Summary
Modifier and Type Method Description static Pair<java.lang.String,java.util.List<PlFormula>>
convertToDimacs(java.util.Collection<PlFormula> formulas)
Converts the given set of formulas to their string representation in Dimacs CNF.static java.lang.String
convertToDimacs(java.util.Collection<PlFormula> formulas, java.util.List<Proposition> props)
Converts the given set of formulas to their string representation in Dimacs CNF.static SatSolver
getDefaultSolver()
Returns the default SAT solver.
If a default SAT solver has been configured this solver is returned by this method.abstract Interpretation<PlBeliefSet,PlFormula>
getWitness(java.util.Collection<PlFormula> formulas)
If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.Interpretation<PlBeliefSet,PlFormula>
getWitness(BeliefSet<PlFormula,?> bs)
If the belief set is consistent this method returns some model of it or, if it is inconsistent, null.Interpretation<PlBeliefSet,PlFormula>
getWitness(PlFormula 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(java.util.Collection<PlFormula> formulas)
Checks whether the given collection of formulas is consistent.boolean
isConsistent(BeliefSet<PlFormula,?> beliefSet)
Checks whether the given belief base is consistent.boolean
isConsistent(PlFormula formula)
Checks whether the given formula is consistent.abstract boolean
isSatisfiable(java.util.Collection<PlFormula> 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.
-
-
-
Method Detail
-
setDefaultSolver
public static void setDefaultSolver(SatSolver solver)
Sets the default SAT solver.- Parameters:
solver
- some SAT solver
-
setTempFolder
public static void setTempFolder(java.io.File tempFolder)
Set the folder for temporary files created by SAT solver.- Parameters:
tempFolder
- some temp folder.
-
hasDefaultSolver
public static boolean hasDefaultSolver()
Returns "true" if a default SAT solver is configured.- Returns:
- "true" if a default SAT solver is configured.
-
getDefaultSolver
public static SatSolver getDefaultSolver()
Returns the default SAT solver.
If a default SAT solver has been configured this solver is returned by this method. If no default solver is configured, the Sat4j solver (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.- Returns:
- the default SAT solver.
-
convertToDimacs
public static java.lang.String convertToDimacs(java.util.Collection<PlFormula> formulas, java.util.List<Proposition> props)
Converts the given set of formulas to their string representation in Dimacs CNF. Note that a single formula may be represented as multiple clauses, so there is no simple correspondence between the formulas of the set and the Dimacs representation. UseconvertToDimacs(.)
for obtaining a map between those.- Parameters:
formulas
- a collection of formulasprops
- a list of propositions (=signature) where the indices are used for writing the clauses.- Returns:
- a string in Dimacs CNF.
-
convertToDimacs
public static Pair<java.lang.String,java.util.List<PlFormula>> convertToDimacs(java.util.Collection<PlFormula> formulas)
Converts the given set of formulas to their string representation in Dimacs CNF. The return value is a pair of
1.) the string representation
2.) 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.- Parameters:
formulas
- a collection of formulas.- Returns:
- a string in Dimacs CNF and a mapping between clauses and original formulas.
-
getWitness
public abstract Interpretation<PlBeliefSet,PlFormula> getWitness(java.util.Collection<PlFormula> formulas)
If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.- Specified by:
getWitness
in interfaceConsistencyWitnessProvider<PlBeliefSet,PlFormula>
- Parameters:
formulas
- a set of formulas- Returns:
- some model of the formulas or null.
-
isSatisfiable
public abstract boolean isSatisfiable(java.util.Collection<PlFormula> formulas)
Checks whether the given set of formulas is satisfiable.- Parameters:
formulas
- a set of formulas.- Returns:
- "true" if the set is consistent.
-
isConsistent
public boolean isConsistent(BeliefSet<PlFormula,?> beliefSet)
Description copied from interface:ConsistencyTester
Checks whether the given belief base is consistent.- Specified by:
isConsistent
in interfaceBeliefSetConsistencyTester<PlFormula>
- Specified by:
isConsistent
in interfaceConsistencyTester<BeliefSet<PlFormula,?>>
- Parameters:
beliefSet
- a belief base.- Returns:
- "true" iff the given belief base is consistent.
-
isConsistent
public boolean isConsistent(java.util.Collection<PlFormula> formulas)
Description copied from interface:BeliefSetConsistencyTester
Checks whether the given collection of formulas is consistent.- Specified by:
isConsistent
in interfaceBeliefSetConsistencyTester<PlFormula>
- Parameters:
formulas
- a collection of formulas.- Returns:
- "true" iff the given collection of formulas is consistent.
-
isConsistent
public boolean isConsistent(PlFormula formula)
Description copied from interface:BeliefSetConsistencyTester
Checks whether the given formula is consistent.- Specified by:
isConsistent
in interfaceBeliefSetConsistencyTester<PlFormula>
- Parameters:
formula
- a formulas.- Returns:
- "true" iff the formula is consistent.
-
getWitness
public Interpretation<PlBeliefSet,PlFormula> getWitness(PlFormula formula)
Description copied from interface:ConsistencyWitnessProvider
If the formula is consistent this method returns some model of it or, if it is inconsistent, null.- Specified by:
getWitness
in interfaceConsistencyWitnessProvider<PlBeliefSet,PlFormula>
- Parameters:
formula
- a formula- Returns:
- some model of the formula or null.
-
getWitness
public Interpretation<PlBeliefSet,PlFormula> getWitness(BeliefSet<PlFormula,?> bs)
Description copied from interface:ConsistencyWitnessProvider
If the belief set is consistent this method returns some model of it or, if it is inconsistent, null.- Specified by:
getWitness
in interfaceConsistencyWitnessProvider<PlBeliefSet,PlFormula>
- Parameters:
bs
- a belief set- Returns:
- some model of the belief set or null.
-
-