Package net.sf.tweety.arg.dung.reasoner
Class AbstractSatExtensionReasoner
- java.lang.Object
-
- net.sf.tweety.arg.dung.reasoner.AbstractDungReasoner
-
- net.sf.tweety.arg.dung.reasoner.AbstractExtensionReasoner
-
- net.sf.tweety.arg.dung.reasoner.AbstractSatExtensionReasoner
-
- All Implemented Interfaces:
ModelProvider<Argument,DungTheory,Extension>
,QualitativeReasoner<DungTheory,Argument>
,Reasoner<java.lang.Boolean,DungTheory,Argument>
- Direct Known Subclasses:
SatCompleteReasoner
,SatStableReasoner
public abstract class AbstractSatExtensionReasoner extends AbstractExtensionReasoner
Uses a provided SAT solver to solve reasoning problems in AAFs.- Author:
- Matthias Thimm
-
-
Constructor Summary
Constructors Constructor Description AbstractSatExtensionReasoner(SatSolver solver)
Instantiates a new reasoner that uses the given SAT solver
-
Method Summary
Modifier and Type Method Description Extension
getModel(DungTheory bbase)
Returns a single (dedicated) model of the given belief base.java.util.Collection<Extension>
getModels(DungTheory bbase)
Returns a characterizing model of the given belief basePlBeliefSet
getPropositionalCharacterisation(DungTheory aaf)
Creates a propositional representation of the set of labelings of the given Dung theory that are consistent with the given semantics.-
Methods inherited from class net.sf.tweety.arg.dung.reasoner.AbstractExtensionReasoner
getSimpleReasonerForSemantics, query, query
-
-
-
-
Constructor Detail
-
AbstractSatExtensionReasoner
public AbstractSatExtensionReasoner(SatSolver solver)
Instantiates a new reasoner that uses the given SAT solver- Parameters:
solver
- some AT solver
-
-
Method Detail
-
getModels
public java.util.Collection<Extension> getModels(DungTheory bbase)
Description copied from interface:ModelProvider
Returns a characterizing model of the given belief base- Specified by:
getModels
in interfaceModelProvider<Argument,DungTheory,Extension>
- Specified by:
getModels
in classAbstractExtensionReasoner
- Parameters:
bbase
- some belief base- Returns:
- the (selected) models of the belief base
-
getPropositionalCharacterisation
public PlBeliefSet getPropositionalCharacterisation(DungTheory aaf)
Creates a propositional representation of the set of labelings of the given Dung theory that are consistent with the given semantics. This means that for every argument A in the theory three propositions are created: in_A, out_A, undec_A. For every attack A->B the formula "in_A => out_B" is added to the belief set. Depending on the actual semantics further propositional formulas are added. For example, for any admissable semantics and unattacked argument A, the constraint "\top=>in_A" is added; another constraint added for admissable semantics is, given any argument A and attackers B1...BN, add the constraint in_A => out_B1 ^ ... ^ out_BN.- Parameters:
aaf
- a Dung Thery- Returns:
- a propositional belief set.
-
getModel
public Extension getModel(DungTheory bbase)
Description copied from interface:ModelProvider
Returns a single (dedicated) model of the given belief base. If the implemented method allows for more than one dedicated model, the selection may be non-deterministic.- Specified by:
getModel
in interfaceModelProvider<Argument,DungTheory,Extension>
- Specified by:
getModel
in classAbstractExtensionReasoner
- Parameters:
bbase
- some belief base- Returns:
- a selected model of the belief base.
-
-