Class AbstractSatExtensionReasoner

    • Field Detail

      • solver

        protected SatSolver solver
        A SAT solver
    • Constructor Detail

      • AbstractSatExtensionReasoner

        public AbstractSatExtensionReasoner​(SatSolver solver)
        Instantiates a new reasoner that uses the given SAT solver
        Parameters:
        solver - some AT solver
    • Method Detail

      • 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.
      • getPropositionalCharacterisationBySemantics

        protected abstract PlBeliefSet getPropositionalCharacterisationBySemantics​(DungTheory aaf,
                                                                                   java.util.Map<Argument,​Proposition> in,
                                                                                   java.util.Map<Argument,​Proposition> out,
                                                                                   java.util.Map<Argument,​Proposition> undec)
        Returns the semantic-specific propositional characterization of the underlying Dung theory, see getPropositionalCharacterisation.
        Parameters:
        aaf - the Dung theory
        in - propositional variables of in arguments.
        out - propositional variables of out arguments.
        undec - propositional variables of undec arguments.
        Returns:
        the semantic-specific propositional characterization of the underlying Dung theory, see getPropositionalCharacterisation.