Class TwoValuedModelSatEncoding

java.lang.Object
org.tweetyproject.arg.adf.reasoner.sat.encodings.TwoValuedModelSatEncoding
All Implemented Interfaces:
RelativeSatEncoding, SatEncoding
public class TwoValuedModelSatEncoding extends Object implements SatEncoding, RelativeSatEncoding
This class implements a SAT encoding for two-valued models in an Abstract Dialectical Framework (ADF). The encoding handles both fixed and unfixed arguments by generating SAT clauses that represent their acceptance conditions. It also provides a way to encode an interpretation as two-valued, where each argument is either satisfied or unsatisfied.

The generated clauses can be passed to a SAT solver for further processing.

Author:
Mathias Hofer

  • Constructor Details

    • TwoValuedModelSatEncoding

      public TwoValuedModelSatEncoding(AbstractDialecticalFramework adf, PropositionalMapping mapping)
      Constructs a new TwoValuedModelSatEncoding for the given Abstract Dialectical Framework (ADF) and propositional mapping.
      Parameters:
      adf - the Abstract Dialectical Framework (ADF) to encode, 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 two-valued model of the ADF into a set of SAT clauses and provides them to the given consumer. This method handles arguments that are not fixed in the interpretation, i.e., their truth value is unknown.
      Specified by:
      encode in interface SatEncoding
      Parameters:
      consumer - the consumer that will accept the generated SAT clauses

    • encode

      public void encode(Consumer<Clause> consumer, Interpretation interpretation)
      Encodes a specific two-valued interpretation of the ADF into a set of SAT clauses and provides them to the given consumer. The interpretation must be two-valued, meaning that all arguments are either satisfied or unsatisfied, with no undecided arguments.
      Specified by:
      encode in interface RelativeSatEncoding
      Parameters:
      consumer - the consumer that will accept the generated SAT clauses
      interpretation - the interpretation to be encoded, must be two-valued (no undecided arguments)
      Throws:
      IllegalArgumentException - if the interpretation contains undecided arguments