MaxSatKAdmissibleReasoner

java.lang.Object

org.tweetyproject.arg.dung.reasoner.MaxSatKAdmissibleReasoner

All Implemented Interfaces:: KOptimisationReasoner, Reasoner<Integer,DungTheory,Argument>

public class MaxSatKAdmissibleReasoner extends Object implements KOptimisationReasoner

A MaxSAT-based implementation for solving the MaxAdm# problem from [Skiba,Thimm; 2024]

Author:: Matthias Thimm

Constructor Summary

Constructors

Constructor

Description

MaxSatKAdmissibleReasoner(MaxSatSolver solver)
Method Summary

Modifier and Type

Method

Description

static int

eval(DungTheory aaf, Collection<Argument> set)

Returns the maximal k such that the given extension is a k-adm# extension of the given AAF.

Integer

query(DungTheory aaf, Argument arg)

Queries the given belief base for the given formula.

Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details
- MaxSatKAdmissibleReasoner
  
  public MaxSatKAdmissibleReasoner(MaxSatSolver solver)
  
  Parameters:
  
  solver - the used MaxSAT solver
Method Details
- eval
  
  public static int eval(DungTheory aaf, Collection<Argument> set)
  
  Returns the maximal k such that the given extension is a k-adm# extension of the given AAF. Returns Integer.MIN_VALUE if the given set is not a k-adm# extension for any k (i.e., iff it is not conflict-free)
  
  Parameters:
  
  aaf - some AAF.
  
  set - some set of arguments.
  
  Returns:
  
  the maximal k such that the given extension is a k-adm# extension of the given AAF.
- query
  
  public Integer query(DungTheory aaf, Argument arg)
  
  Description copied from interface: Reasoner
  
  Queries the given belief base for the given formula.
  
  Specified by:
  
  query in interface KOptimisationReasoner
  
  Specified by:
  
  query in interface Reasoner<Integer,DungTheory,Argument>
  
  Parameters:
  
  aaf - a belief base
  
  arg - a formula
  
  Returns:
  
  the answer to the query