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

Class BipolarSatEncoding

java.lang.Object

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

All Implemented Interfaces:

SatEncoding

public class BipolarSatEncoding
extends Object
implements SatEncoding

This class implements a SAT encoding for bipolar Abstract Dialectical Frameworks (ADF). The encoding handles both attacking and supporting links between arguments, ensuring that the argument semantics are encoded properly into propositional clauses.

In a bipolar ADF, arguments are connected by two types of links: attacking and supporting. This encoding creates SAT clauses that reflect these relationships.

Author:

Mathias Hofer

Constructor Summary

Constructors

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

Method Summary

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

Methods inherited from class java.lang.Object

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

Constructor Details

BipolarSatEncoding

public BipolarSatEncoding(AbstractDialecticalFramework adf,
 PropositionalMapping mapping)

Constructs a new BipolarSatEncoding for the given Abstract Dialectical Framework (ADF) and propositional mapping.

Parameters:

adf - the Abstract Dialectical Framework (ADF) 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 bipolar Abstract Dialectical Framework (ADF) into a set of SAT clauses. These clauses represent the relationships between arguments, specifically the attacking and supporting links. The clauses are then passed to the provided consumer.

Specified by:

encode in interface SatEncoding

Parameters:

consumer - the consumer that accepts the generated SAT clauses