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

Class KBipolarSatEncoding

java.lang.Object

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

All Implemented Interfaces:

SatEncoding

public final class KBipolarSatEncoding
extends Object
implements SatEncoding

The KBipolarSatEncoding class provides an encoding of a bipolar argumentation framework into a propositional formula for SAT solving. It implements the SatEncoding interface and processes the Abstract Dialectical Framework (ADF) along with a propositional mapping of arguments. The encoding considers the undecided arguments and uses Tseitin transformation to generate the propositional formula that is fed into a SAT solver.

Author:

Mathias Hofer

Constructor Summary

Constructors

Constructor	Description
KBipolarSatEncoding(AbstractDialecticalFramework adf, PropositionalMapping mapping)	Constructs a KBipolarSatEncoding instance with the given ADF and propositional mapping.

Method Summary

Modifier and Type	Method	Description
void	encode(Consumer<Clause> consumer)	Encodes the acceptance conditions of the arguments in the ADF into a SAT formula using a given consumer.

Methods inherited from class java.lang.Object

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

Constructor Details

KBipolarSatEncoding

public KBipolarSatEncoding(AbstractDialecticalFramework adf,
 PropositionalMapping mapping)

Constructs a KBipolarSatEncoding instance with the given ADF and propositional mapping.

Parameters:

adf - the abstract dialectical framework, must not be null

mapping - the propositional mapping used for the encoding, must not be null

Throws:

NullPointerException - if adf or mapping is null

Method Details

encode

public void encode(Consumer<Clause> consumer)

Encodes the acceptance conditions of the arguments in the ADF into a SAT formula using a given consumer. The encoding involves generating clauses based on the undecided arguments and their dependencies, and applying Tseitin transformation to handle complex acceptance conditions.

Specified by:

encode in interface SatEncoding

Parameters:

consumer - the consumer to accept the generated SAT clauses