Class KBipolarSatEncoding

java.lang.Object
org.tweetyproject.arg.adf.reasoner.sat.encodings.KBipolarSatEncoding
All Implemented Interfaces:
SatEncoding
public final class KBipolarSatEncoding extends Object implements SatEncoding
The KBipolarSatEncoding class provides an encoding of a bipolar argumentation framework into a propositional formula for SAT solving. It implements the SatEncoding interface and processes the Abstract Dialectical Framework (ADF) along with a propositional mapping of arguments. The encoding considers the undecided arguments and uses Tseitin transformation to generate the propositional formula that is fed into a SAT solver.
Author:
Mathias Hofer

  • Constructor Details

    • KBipolarSatEncoding

      public KBipolarSatEncoding(AbstractDialecticalFramework adf, PropositionalMapping mapping)
      Constructs a KBipolarSatEncoding instance with the given ADF and propositional mapping.
      Parameters:
      adf - the abstract dialectical framework, must not be null
      mapping - the propositional mapping used for the encoding, must not be null
      Throws:
      NullPointerException - if adf or mapping is null

  • Method Details

    • encode

      public void encode(Consumer<Clause> consumer)
      Encodes the acceptance conditions of the arguments in the ADF into a SAT formula using a given consumer. The encoding involves generating clauses based on the undecided arguments and their dependencies, and applying Tseitin transformation to handle complex acceptance conditions.
      Specified by:
      encode in interface SatEncoding
      Parameters:
      consumer - the consumer to accept the generated SAT clauses