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

Class RestrictedKBipolarSatEncoding

java.lang.Object

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

All Implemented Interfaces:

SatEncoding

public final class RestrictedKBipolarSatEncoding
extends Object
implements SatEncoding

The RestrictedKBipolarSatEncoding class implements a SAT encoding specifically for restricted bipolar Abstract Dialectical Frameworks (ADFs). It leverages partial interpretations and completes undecided arguments in a two-valued manner. The class uses Tseitin transformations to generate propositional clauses.

This encoding is restricted because it only applies the encoding to arguments that have undecided dependencies. It also filters completions where the interpretation contradicts the partial interpretation.

Author:

Mathias Hofer

Constructor Summary

Constructors

Constructor	Description
RestrictedKBipolarSatEncoding(AbstractDialecticalFramework adf, PropositionalMapping mapping, Interpretation partial)	Constructs a new RestrictedKBipolarSatEncoding with the specified Abstract Dialectical Framework, propositional mapping, and partial interpretation.

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

RestrictedKBipolarSatEncoding

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

Constructs a new RestrictedKBipolarSatEncoding with the specified Abstract Dialectical Framework, propositional mapping, and partial interpretation.

Parameters:

adf - the Abstract Dialectical Framework

mapping - the propositional mapping for arguments and links

partial - the partial interpretation to be used during encoding

Method Details

encode

public void encode(Consumer<Clause> consumer)

Encodes the bipolar Abstract Dialectical Framework (ADF) into a set of SAT clauses. The encoding is restricted to arguments that have undecided dependencies. The encoding applies the Tseitin transformation to convert the acceptance conditions of these arguments into propositional clauses.

Specified by:

encode in interface SatEncoding

Parameters:

consumer - the consumer that accepts the generated SAT clauses