Class BipolarSatEncoding

java.lang.Object
org.tweetyproject.arg.adf.reasoner.sat.encodings.BipolarSatEncoding
All Implemented Interfaces:
SatEncoding
public class BipolarSatEncoding extends Object implements SatEncoding
This class implements a SAT encoding for bipolar Abstract Dialectical Frameworks (ADF). The encoding handles both attacking and supporting links between arguments, ensuring that the argument semantics are encoded properly into propositional clauses.

In a bipolar ADF, arguments are connected by two types of links: attacking and supporting. This encoding creates SAT clauses that reflect these relationships.

Author:
Mathias Hofer

  • Constructor Details

    • BipolarSatEncoding

      public BipolarSatEncoding(AbstractDialecticalFramework adf, PropositionalMapping mapping)
      Constructs a new BipolarSatEncoding for the given Abstract Dialectical Framework (ADF) and propositional mapping.
      Parameters:
      adf - the Abstract Dialectical Framework (ADF) for which the SAT encoding is created, must not be null
      mapping - the propositional mapping for the arguments and links, must not be null

  • Method Details

    • encode

      public void encode(Consumer<Clause> consumer)
      Encodes the bipolar Abstract Dialectical Framework (ADF) into a set of SAT clauses. These clauses represent the relationships between arguments, specifically the attacking and supporting links. The clauses are then passed to the provided consumer.
      Specified by:
      encode in interface SatEncoding
      Parameters:
      consumer - the consumer that accepts the generated SAT clauses