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

Class PreferredVerifier

java.lang.Object

org.tweetyproject.arg.adf.reasoner.sat.verifier.PreferredVerifier

All Implemented Interfaces:

AutoCloseable, Verifier

public final class PreferredVerifier
extends Object
implements Verifier

The PreferredVerifier is a verifier class that checks whether a given interpretation is a preferred interpretation within an abstract dialectical framework (ADF). It utilizes a SAT solver to verify if the interpretation satisfies certain properties, such as being conflict-free and maximal.

Author:

Sebastian

Constructor Summary

Constructors

Constructor	Description
PreferredVerifier(Supplier<SatSolverState> stateSupplier, AbstractDialecticalFramework adf, PropositionalMapping mapping)	Constructs a PreferredVerifier with the given SAT solver state supplier, abstract dialectical framework, and propositional mapping.

Method Summary

Modifier and Type	Method	Description
void	close()	Closes the SAT solver state and releases any resources associated with it.
void	prepare()	Prepares the SAT solver state by encoding the bipolarity and conflict-free conditions of the abstract dialectical framework.
boolean	verify(Interpretation interpretation)	Verifies whether the given interpretation is a preferred interpretation within the framework.

Methods inherited from class java.lang.Object

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

Constructor Details

PreferredVerifier

public PreferredVerifier(Supplier<SatSolverState> stateSupplier,
 AbstractDialecticalFramework adf,
 PropositionalMapping mapping)

Constructs a PreferredVerifier with the given SAT solver state supplier, abstract dialectical framework, and propositional mapping. The SAT solver state is initialized using the provided supplier.

Parameters:

stateSupplier - a supplier that provides new instances of SatSolverState, must not be null

adf - the abstract dialectical framework to be processed, must not be null

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

Throws:

NullPointerException - if any of the parameters are null

Method Details

prepare

public void prepare()

Prepares the SAT solver state by encoding the bipolarity and conflict-free conditions of the abstract dialectical framework. This method should be called before attempting to verify any interpretation.

Specified by:

prepare in interface Verifier

verify

public boolean verify(Interpretation interpretation)

Verifies whether the given interpretation is a preferred interpretation within the framework. This method fixes the already decided arguments in the SAT solver state, attempts to decide any remaining undecided arguments, and checks whether the interpretation is maximal.

Specified by:

verify in interface Verifier

Parameters:

interpretation - the interpretation to be verified

Returns:

true if the interpretation is preferred (i.e., maximal and conflict-free), false otherwise

close

public void close()

Closes the SAT solver state and releases any resources associated with it. This method should be called when the verifier is no longer needed to ensure proper resource management.

Specified by:

close in interface AutoCloseable

Specified by:

close in interface Verifier