Class QbfSolver
java.lang.Object
org.tweetyproject.logics.qbf.reasoner.QbfSolver
- All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>
,ConsistencyTester<BeliefSet<PlFormula,?>>
- Direct Known Subclasses:
CadetSolver
,CaqeSolver
,GhostQSolver
,QuteSolver
Abstract QBF sat solver to be implemented by concrete solvers.
- Author:
- Anna Gessler
-
Constructor Summary
-
Method Summary
Modifier and TypeMethodDescriptionboolean
isConsistent(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(Collection<PlFormula> formulas)
Checks whether the given set of formulas is satisfiable.
-
Constructor Details
-
QbfSolver
public QbfSolver()
-
-
Method Details
-
isSatisfiable
Checks whether the given set of formulas is satisfiable.- Parameters:
formulas
- a set of formulas.- Returns:
- "true" if the set is consistent.
-
isConsistent
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
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
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.
-