Class ConflictFreeInterpretationSatEncoding

java.lang.Object
org.tweetyproject.arg.adf.reasoner.sat.encodings.ConflictFreeInterpretationSatEncoding
All Implemented Interfaces:
RelativeSatEncoding, SatEncoding
public class ConflictFreeInterpretationSatEncoding extends Object implements SatEncoding, RelativeSatEncoding
This class implements a SAT encoding for conflict-free interpretations in an Abstract Dialectical Framework (ADF). It ensures that no argument is both satisfied and unsatisfied simultaneously, and properly links arguments with their acceptance conditions using Tseitin transformation.

The encoding also supports both absolute and relative encoding based on the current interpretation.

Author:
Mathias Hofer

  • Constructor Details

    • ConflictFreeInterpretationSatEncoding

      public ConflictFreeInterpretationSatEncoding(AbstractDialecticalFramework adf, PropositionalMapping mapping)
      Constructs a new ConflictFreeInterpretationSatEncoding for the given Abstract Dialectical Framework (ADF) and propositional mapping.
      Parameters:
      adf - the Abstract Dialectical Framework 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 conflict-free interpretation of the given ADF into a set of SAT clauses. These clauses ensure that no argument is both satisfied and unsatisfied at the same time and links arguments to their acceptance conditions.
      Specified by:
      encode in interface SatEncoding
      Parameters:
      consumer - the consumer that accepts the generated SAT clauses

    • encode

      public void encode(Consumer<Clause> consumer, Interpretation interpretation)
      Encodes the conflict-free interpretation of the given ADF into a set of SAT clauses based on the provided interpretation. This method adapts the encoding depending on whether an argument is satisfied, unsatisfied, or undecided.
      Specified by:
      encode in interface RelativeSatEncoding
      Parameters:
      consumer - the consumer that accepts the generated SAT clauses
      interpretation - the current interpretation of the ADF