Package net.sf.tweety.logics.qbf.reasoner

Class QbfSolver

java.lang.Object

net.sf.tweety.logics.qbf.reasoner.QbfSolver

All Implemented Interfaces:

BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>

Direct Known Subclasses:

CadetSolver, CaqeSolver, GhostQSolver, QuteSolver

public abstract class QbfSolver
extends java.lang.Object
implements BeliefSetConsistencyTester<PlFormula>

Abstract QBF sat solver to be implemented by concrete solvers.

Author:

Anna Gessler

Field Summary

Fields

Modifier and Type	Field	Description
protected Shell	bash	Shell for running solvers.

Constructor Summary

Constructors

Constructor	Description
QbfSolver()

Method Summary

Modifier and Type	Method	Description
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.

Methods inherited from class java.lang.Object

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

Field Detail

bash

protected Shell bash

Shell for running solvers.

Constructor Detail

QbfSolver

public QbfSolver()

Method Detail

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 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(java.util.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.