Class KBipolarStateProcessor

java.lang.Object
org.tweetyproject.arg.adf.reasoner.sat.processor.KBipolarStateProcessor
All Implemented Interfaces:
StateProcessor
public final class KBipolarStateProcessor extends Object implements StateProcessor
The KBipolarStateProcessor class is responsible for processing the state of an AbstractDialecticalFramework (ADF) by encoding its bipolar and k-bipolar structure into logical clauses. These clauses can then be used for SAT solving or other reasoning tasks.

The processor uses two different SAT encodings:

This class is designed to work with propositional mappings between arguments and their respective logical representations.

It ensures that the appropriate encoding is applied based on the structure of the ADF. If the ADF is not completely bipolar, the k-bipolar encoding is applied in addition to the bipolar encoding.

Author:
Mathias Hofer

  • Constructor Details

    • KBipolarStateProcessor

      public KBipolarStateProcessor(AbstractDialecticalFramework adf, PropositionalMapping mapping)
      Constructs a new KBipolarStateProcessor for the given Abstract Dialectical Framework (ADF) and propositional mapping. The processor initializes both the bipolar and k-bipolar SAT encodings.
      Parameters:
      adf - the Abstract Dialectical Framework (ADF) to process, must not be null
      mapping - the propositional mapping for the arguments and links in the ADF, must not be null

  • Method Details

    • process

      public void process(Consumer<Clause> consumer)
      Processes the state of the ADF and encodes the relationships into logical clauses.

      First, the bipolar relationships are encoded. If the ADF is not fully bipolar, the k-bipolar relationships are encoded as well.

      Specified by:
      process in interface StateProcessor
      Parameters:
      consumer - a Consumer that accepts the generated Clause objects