SemOpt  $Revision:72+[d9d7a33b5c20+]$
prefSAT.cpp File Reference

Functions computing the preferred extensions of an AF according to the algorithm described in TAFA-13. More...

#include "semopt.h"

Go to the source code of this file.

Functions

int PiGreek (SATFormulae *sat, AF *af, int encoding)
 Function computing the labelling constraints encoding in a SATFormulae given an AF and the type of encoding desired.
void aSolution (vector< int > *res, dArray *vals, AF *af)
 Given a solution returned by a SAT Solver, and given a dArray of the same size of the number of arguments af, if the argument whose number is num is labelled IN, then it writes 1 in the position num of the given dArray, 0 otherwise.
void INARGS (vector< int > *assign, vector< Argument * > *toarg, vector< Argument * > *closeworld, AF *af)
 Given a solution returned by a SAT Solver, it fills in two vector of Argument where the first contains the pointers to the Argument that are labelled IN in the solution, and the second containing all the other Argument.
int PrefSat (dMatrix *preferred_extensions, AF *af, int encoding, int(*SatSolver)(stringstream *, int, int, vector< int > *))
 This is the function that in TAFA-13 is described by Algorithm 1.

Detailed Description

Functions computing the preferred extensions of an AF according to the algorithm described in TAFA-13.

Author
Federico Cerutti f.cer.nosp@m.utti.nosp@m.@abdn.nosp@m..ac..nosp@m.uk

Definition in file prefSAT.cpp.

Function Documentation

void aSolution ( vector< int > *  res,
dArray vals,
AF af 
)

Given a solution returned by a SAT Solver, and given a dArray of the same size of the number of arguments af, if the argument whose number is num is labelled IN, then it writes 1 in the position num of the given dArray, 0 otherwise.

Parameters
[in]resA pointer to a vector<int> which represents the results of the SAT Solver
[out]valsA pointer to a dArray whose size is equals to the number of Argument
[in]afA pointer to the AF considered in this case
Return values
void
See Also
PrefSat for an explanation of the parameter res

Definition at line 204 of file prefSAT.cpp.

References AF::getArgumentByNumber(), and Argument::InVar().

Referenced by PrefSat().

void INARGS ( vector< int > *  assign,
vector< Argument * > *  toarg,
vector< Argument * > *  closeworld,
AF af 
)

Given a solution returned by a SAT Solver, it fills in two vector of Argument where the first contains the pointers to the Argument that are labelled IN in the solution, and the second containing all the other Argument.

Parameters
[in]assignA pointer to a vector<int> which represents the results of the SAT Solver
[out]toargA pointer to a vector<Argument *> which represents (in the TAFA-13 terminology) the set of arguments $INARGS(\mbox{\texttt{assign}}) \subseteq \mathcal{A}$
[out]closeworldA pointer to a vector<Argument *> which represents (in the TAFA-13 terminology) the set of arguments $(\mathcal{A} \setminus INARGS(\mbox{\texttt{assign}})) \subseteq \mathcal{A}$
[in]afA pointer to the AF considered in this case
Return values
void
See Also
PrefSat for an explanation of the parameter assign

Definition at line 230 of file prefSAT.cpp.

References AF::getArgumentByNumber(), and AF::numArgs().

Referenced by PrefSat().

int PiGreek ( SATFormulae sat,
AF af,
int  encoding 
)

Function computing the labelling constraints encoding in a SATFormulae given an AF and the type of encoding desired.

Parameters
[out]satA pointer to an initialised SATFormulae object which will contains the SAT formuale of the given AF
[in]afThe pointer to the object instance of AF which represents the argumentation framework from which we want to derive the labellings contraints
[in]encodingAn int representing the type of encoding desired according to the given table
encoding Chosen encodings according to TAFA-13
0 $C_1$
1 $C_2$
2 $C_3$
3 $C_1^a$
4 $C_1^b$
5 $C_1^c$
Return values
intThe number of OrClause added to the parameter sat

Definition at line 35 of file prefSAT.cpp.

References OrClause::addHeadVariable(), OrClause::appendVariable(), SetArguments::begin(), OrClause::clone(), debug, SetArguments::empty(), SetArguments::end(), AF::getArgumentByNumber(), Argument::getName(), AF::getPredecessors(), Argument::InVar(), Argument::NotInVar(), Argument::NotOutVar(), Argument::NotUndecVar(), AF::numArgs(), Argument::OutVar(), and Argument::UndecVar().

Referenced by PrefSat().

int PrefSat ( dMatrix preferred_extensions,
AF af,
int  encoding,
int(*)(stringstream *, int, int, vector< int > *)  SatSolver 
)

This is the function that in TAFA-13 is described by Algorithm 1.

This function has been rewritten for adhering to Algorithm 1 of TAFA-13, but the one used for the empirical evaluation in TAFA-13 was slightly different as it adopts some straightforward optimisations

Parameters
[out]preferred_extensionsPointer to a dMatrix which will contain the computed preferred extensions. E.g., if the set of arguments is $\mathcal{A} = \{a_1, a_2, a_3, a_4, a_5\}$, then if preferred_extensions will result:
0 1 2 3 4
1 0 1 0 0
1 1 0 0 0
0 0 1 1 1
then the preferred extensions of the AF are:
  1. $\{a_1, a_3\}$
  2. $\{a_1, a_2\}$
  3. $\{a_3, a_4, a_5\}$
[in]afA pointer to the AF considered in this case
[in]encodingAn integer representing the desired encoding, see PiGreek for an explanation
[in]SatSolverA pointer to a function which acts as a SAT Solver, whose signature must be:
    int name-function(stringstream *, int, int, vector<int> *);
returning an int which will be equal to 20 if no solution has been found, and accepting as input:
  1. a pointer to an object strigstream that contains the representation of a CNF in the DIMACS format (see the rules for SAT competition 2011 for instance)
  2. the number of variables of the CNF
  3. the number of clause (OrClause) in the CNF
  4. a pointer to a vector<int> already whose memory is already allocated and that is an out parameter which will contain the result of the SAT Solver computation. For instance, if the number of variables is 9, then this vector should be of the form:
    0 1 2 3 4 5 6 7 8
    1 0 1 0 0 0 0 1 0
    whose semantics is that the first, third, and eighth variables are assigned to True, while the others are assigned to False in this Satisfiability problem
Return values
int0 if the preferred extensions are correctely computed, 1 if the SatSolver is not specified,
See Also
PiGreek for explanation of the parameter encoding

Definition at line 288 of file prefSAT.cpp.

References OrClause::appendVariable(), aSolution(), debug, INARGS(), AF::numArgs(), and PiGreek().