Class RefineUnequalSatEncoding

java.lang.Object
org.tweetyproject.arg.adf.reasoner.sat.encodings.RefineUnequalSatEncoding
All Implemented Interfaces:
RelativeSatEncoding
public class RefineUnequalSatEncoding extends Object implements RelativeSatEncoding
This class implements a SAT encoding for refining unequal interpretations in an Abstract Dialectical Framework (ADF). It generates clauses based on the current interpretation, ensuring that the refinement does not result in the same interpretation as the input.

The encoding is used to enforce conditions on satisfied, unsatisfied, and undecided arguments within an ADF.

Author:
Mathias Hofer

  • Constructor Details

    • RefineUnequalSatEncoding

      public RefineUnequalSatEncoding(PropositionalMapping mapping)
      Constructs a new RefineUnequalSatEncoding with the specified propositional mapping.
      Parameters:
      mapping - the mapping from arguments to propositional variables, must not be null

  • Method Details

    • encode

      public void encode(Consumer<Clause> consumer, Interpretation interpretation)
      Encodes the given interpretation into a set of SAT clauses that represent the refinement of the interpretation, ensuring that the resulting interpretation is not equal to the input interpretation.
      Specified by:
      encode in interface RelativeSatEncoding
      Parameters:
      consumer - the clause consumer that accepts the generated clauses
      interpretation - the interpretation to be refined and encoded