Package net.sf.tweety.arg.adf.reasoner

Class SatEncoding

java.lang.Object

net.sf.tweety.arg.adf.reasoner.SatEncoding

public class SatEncoding
extends java.lang.Object

TODO: generalize? TODO: rewrite encoding in cnf

Author:

Mathias Hofer

Field Summary

Fields

Modifier and Type	Field	Description
private AbstractDialecticalFramework	adf	TODO: the adf is not immutable, therefore adding stuff to it after SatEncoding was created may fuck things up?
private java.util.Collection<Disjunction>	argsTrueXorFalse	This formula ensures that the propositions s_t and s_f for an argument s cannot both be true at the same time.
private Cache<Argument,Proposition>	falses
private Cache<Link,Proposition>	links
private Cache<Argument,Proposition>	trues

Constructor Summary

Constructors

Constructor	Description
SatEncoding(AbstractDialecticalFramework adf)

Method Summary

Modifier and Type	Method	Description
java.util.Collection<Disjunction>	bipolar()
java.util.Collection<Disjunction>	conflictFreeInterpretation()
Interpretation	interpretationFromWitness(Interpretation<PlBeliefSet,PlFormula> witness)
java.util.Collection<Disjunction>	kBipolar(Interpretation interpretation)
java.util.Collection<Disjunction>	largerInterpretation(Interpretation interpretation)	TODO define functionality
Disjunction	refineLarger(Interpretation interpretation)
Disjunction	refineUnequal(Interpretation interpretation)	TODO Define functionality
java.util.Collection<Disjunction>	verifyAdmissible(Interpretation interpretation)

Methods inherited from class java.lang.Object

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

Field Detail

falses

private Cache<Argument,Proposition> falses

trues

private Cache<Argument,Proposition> trues

links

private Cache<Link,Proposition> links

adf

private AbstractDialecticalFramework adf

TODO: the adf is not immutable, therefore adding stuff to it after SatEncoding was created may fuck things up?

argsTrueXorFalse

private java.util.Collection<Disjunction> argsTrueXorFalse

This formula ensures that the propositions s_t and s_f for an argument s cannot both be true at the same time. Store globally, since it does not depend on interpretations. TODO find better name, since it is not really xor (both can be false)

Constructor Detail

SatEncoding

public SatEncoding(AbstractDialecticalFramework adf)

Method Detail

refineLarger

public Disjunction refineLarger(Interpretation interpretation)

refineUnequal

public Disjunction refineUnequal(Interpretation interpretation)

TODO Define functionality

Parameters:

interpretation - some interpretation

Returns:

a clause

conflictFreeInterpretation

public java.util.Collection<Disjunction> conflictFreeInterpretation()

largerInterpretation

public java.util.Collection<Disjunction> largerInterpretation(Interpretation interpretation)

TODO define functionality

Parameters:

interpretation - some interpretation

Returns:

a collection of clauses

bipolar

public java.util.Collection<Disjunction> bipolar()

kBipolar

public java.util.Collection<Disjunction> kBipolar(Interpretation interpretation)

verifyAdmissible

public java.util.Collection<Disjunction> verifyAdmissible(Interpretation interpretation)

interpretationFromWitness

public Interpretation interpretationFromWitness(Interpretation<PlBeliefSet,PlFormula> witness)