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

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 Summary

Constructors

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

Method Summary

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

Methods inherited from class java.lang.Object

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

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