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

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 Summary

Constructors

Constructor	Description
RefineUnequalSatEncoding(PropositionalMapping mapping)	Constructs a new RefineUnequalSatEncoding with the specified propositional mapping.

Method Summary

Modifier and Type	Method	Description
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.

Methods inherited from class java.lang.Object

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

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