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

public abstract class QbfSolver
extends Object
implements BeliefSetConsistencyTester<PlFormula>

Abstract QBF sat solver to be implemented by concrete solvers.

Author:

Anna Gessler

Constructor Summary

Constructors

Constructor	Description
QbfSolver()	Default

Method Summary

Modifier and Type	Method	Description
boolean	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	isInstalled()	Return installation status
abstract boolean	isSatisfiable(Collection<PlFormula> formulas)	Checks whether the given set of formulas is satisfiable.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

QbfSolver

public QbfSolver()

Default

Method Details

isSatisfiable

public abstract boolean isSatisfiable(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 interface BeliefSetConsistencyTester<PlFormula>

Specified by:

isConsistent in interface ConsistencyTester<BeliefSet<PlFormula, ?>>

Parameters:

beliefSet - a belief base.

Returns:

"true" iff the given belief base is consistent.

isConsistent

public boolean isConsistent(Collection<PlFormula> formulas)

Description copied from interface: BeliefSetConsistencyTester

Checks whether the given collection of formulas is consistent.

Specified by:

isConsistent in interface BeliefSetConsistencyTester<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 interface BeliefSetConsistencyTester<PlFormula>

Parameters:

formula - a formulas.

Returns:

"true" iff the formula is consistent.

isInstalled

public abstract boolean isInstalled()

Return installation status

Returns:

installation status