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

Class RestrictedBipolarSatEncoding

java.lang.Object

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

All Implemented Interfaces:

SatEncoding

public class RestrictedBipolarSatEncoding
extends Object
implements SatEncoding

This class implements a SAT encoding for restricted bipolar Abstract Dialectical Frameworks (ADF) based on a given partial interpretation. It handles the relationships between arguments through attacking and supporting links.

This encoding ensures that for any given argument, the relationships established by the links are respected according to the partial interpretation provided.

Author:

Mathias Hofer

Constructor Summary

Constructors

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

Method Summary

Modifier and Type	Method	Description
void	encode(Consumer<Clause> consumer)	Encodes the restricted bipolar Abstract Dialectical Framework (ADF) into a set of SAT clauses based on the given partial interpretation.

Methods inherited from class java.lang.Object

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

Constructor Details

RestrictedBipolarSatEncoding

public RestrictedBipolarSatEncoding(AbstractDialecticalFramework adf,
 PropositionalMapping mapping,
 Interpretation partial)

Constructs a new RestrictedBipolarSatEncoding for the given Abstract Dialectical Framework (ADF), propositional mapping, and partial interpretation.

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

partial - the partial interpretation that restricts the SAT encoding, must not be null

Method Details

encode

public void encode(Consumer<Clause> consumer)

Encodes the restricted bipolar Abstract Dialectical Framework (ADF) into a set of SAT clauses based on the given partial interpretation. The clauses represent the attacking and supporting links between arguments, ensuring that the semantics of these links are encoded correctly.

Specified by:

encode in interface SatEncoding

Parameters:

consumer - the consumer that accepts the generated SAT clauses