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

Class ConflictFreeMaximizer

java.lang.Object

org.tweetyproject.arg.adf.reasoner.sat.processor.ConflictFreeMaximizer

All Implemented Interfaces:

AutoCloseable, InterpretationProcessor

public abstract class ConflictFreeMaximizer
extends Object
implements InterpretationProcessor

The ConflictFreeMaximizer is an abstract class responsible for maximizing conflict-free interpretations in an abstract dialectical framework (ADF). It processes interpretations and ensures that they are conflict-free by utilizing SAT solver states and encoding mechanisms. The maximizer has two main modes: restricted and unrestricted, determined by the concrete subclasses.

Author:

Mathias Hofer

Method Summary

Modifier and Type	Method	Description
void	close()
Interpretation	process(Interpretation interpretation)	Processes the given interpretation by maximizing it into a conflict-free interpretation.
static InterpretationProcessor	restricted(Supplier<SatSolverState> stateSupplier, AbstractDialecticalFramework adf, PropositionalMapping mapping, Interpretation prefix)	Creates and returns a restricted InterpretationProcessor that maximizes interpretations based on a given partial interpretation (prefix).
static InterpretationProcessor	unrestricted(Supplier<SatSolverState> stateSupplier, AbstractDialecticalFramework adf, PropositionalMapping mapping)	Creates and returns an unrestricted InterpretationProcessor that maximizes interpretations without any restrictions on the partial interpretation.
void	updateState(SatSolverState state, Interpretation maximal)	Updates the SAT solver state to prevent smaller interpretations from being computed in the future.

Methods inherited from class java.lang.Object

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

Method Details

restricted

public static InterpretationProcessor restricted(Supplier<SatSolverState> stateSupplier,
 AbstractDialecticalFramework adf,
 PropositionalMapping mapping,
 Interpretation prefix)

Creates and returns a restricted InterpretationProcessor that maximizes interpretations based on a given partial interpretation (prefix). This processor restricts conflict-free maximization to interpretations that are consistent with the given partial interpretation.

Parameters:

stateSupplier - a supplier that provides new instances of SatSolverState

adf - the abstract dialectical framework to be processed

mapping - the propositional mapping used for encoding

prefix - the partial interpretation to restrict the maximization

Returns:

an InterpretationProcessor for restricted conflict-free maximization

unrestricted

public static InterpretationProcessor unrestricted(Supplier<SatSolverState> stateSupplier,
 AbstractDialecticalFramework adf,
 PropositionalMapping mapping)

Creates and returns an unrestricted InterpretationProcessor that maximizes interpretations without any restrictions on the partial interpretation.

Parameters:

stateSupplier - a supplier that provides new instances of SatSolverState

adf - the abstract dialectical framework to be processed

mapping - the propositional mapping used for encoding

Returns:

an InterpretationProcessor for unrestricted conflict-free maximization

process

public Interpretation process(Interpretation interpretation)

Processes the given interpretation by maximizing it into a conflict-free interpretation. This method uses a SAT solver to find the largest conflict-free interpretation that satisfies the given propositional mapping.

Specified by:

process in interface InterpretationProcessor

Parameters:

interpretation - the interpretation to be maximized

Returns:

the maximized conflict-free interpretation

updateState

public void updateState(SatSolverState state,
 Interpretation maximal)

Updates the SAT solver state to prevent smaller interpretations from being computed in the future. This method is called after a maximal conflict-free interpretation is found, to ensure that smaller interpretations are not revisited.

Specified by:

updateState in interface InterpretationProcessor

Parameters:

state - the SAT solver state to be updated

maximal - the maximal interpretation that has been found

close

public void close()

Specified by:

close in interface AutoCloseable

Specified by:

close in interface InterpretationProcessor