Package org.tweetyproject.arg.adf.reasoner.sat.encodings

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 Summary

Constructors

Constructor	Description
ConflictFreeInterpretationSatEncoding(AbstractDialecticalFramework adf, PropositionalMapping mapping)	Constructs a new ConflictFreeInterpretationSatEncoding for the given Abstract Dialectical Framework (ADF) and propositional mapping.

Method Summary

Modifier and Type	Method	Description
void	encode(Consumer<Clause> consumer)	Encodes the conflict-free interpretation of the given ADF into a set of SAT clauses.
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.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

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