[Solved]: Modeling the problem of finding all stable sets of an argumentation framework as SAT

Problem Detail: 

As a continuation of my previous question i will try to explain my problem and how i am trying to convert my algorithm to a problem that can be expressed in a CNF form.

Problem: Find all stable sets of an argumentation framework according to Dung's proposed framework.

Brief theory: Having an argumentation framework AF, with A the set of all arguments and R the set of the relations, a stable set is a set which attacks all arguments not in their set and there is no attack relation between arguments in the stable set. Example:

Let's say we have an argumentation framework AF ,A={1,2,3,4}(arguments of AF) and attack relations R{1,3} and R{2,4}. It's obvious that the set {1,2} is a stable extension of the framework because:

a)it attacks all arguments not in their set (3 and 4)

b)it's conflict free(no attacks between arguments in the set) because argument 1 does not attack argument 2 and the opposite

My exhaustive abstract algorithm:

argnum=number of arguments;  Ai[argnum-1]=relation "attacks" ,where 1<=i<=argnum  P[2^argnum-1]=all possible relations that can be generated from all the arguments  S[2^argnum-1]=empty; where S are all the stable sets  j=0; //counter for while k=1; //counter for counting stable sets while j<2^argnum-1     if P[j] attacks all arguments not in P[j](check using Ai[])         if all arguments in P[j] are conlfict-free             S[k++]=P[j];         end if     end if      j++; end while 

I want to solve the above problem either by transforming the above algorithm to CNF or by using a different algorithm and finally use a SAT Solver(or anything similar if exists) give CNF as input and get stable sets as output.

I wonder if someone can give me any feedback of how i can transform any algorithm like the above to CNF in order to be used into a SAT Solver.

I decided to use precosat.

Asked By : Dchris

Answered By : Kyle Jones

Finding a stable argument set is equivalent to finding an independent set in the directed graph of argument attacks, with the added restriction that some member of the set must be adjacent to each vertex in the graph not in the independent set. The problem is at least as hard as the indepependent set decision problem and is thus NP-hard. The decision version of the stable argument set problem is reducible to Boolean SAT as follows:

Input: Given a set of $n$ arguments $ARG_{1}$ to $ARG_{n}$, let the SAT propositional variable $ATTACK_{i,j}$ be true if $ARG_{i}$ attacks $ARG_{j}$.

Output: Let $INDSET_{1} ... INDSET_{n}$ be a new set of propositional variables. $INDSET_{i}$ will be true in the SAT solution iff $ARG_{i}$ is part of the stable set found.

Generating the clauses:

1. For every pair of variables $INDSET_{i}$, $INDSET_{j}$, add clauses that require

   $\overline{(INDSET_{i} \land INDSET_{j})} \lor (\overline{ATTACK_{i,j}} \land \overline{ATTACK_{j,i}})$.

   These clauses prohibit any stable set argument from attacking another.

2. Let $NEEDATTACK_{1} ... NEEDATTACK_{n}$ be a new set of propositional variables. For each $INDSET_{i}$ variable, add clauses that require

   $INDSET_{i} \oplus NEEDATTACK_{i}$

   These clauses record which arguments must be attacked by the stable set arguments.

3. Let $GOTATTACK_{1} ... GOTATTACK_{n}$ be a new set of propositional variables. For each $GOTATTACK_{j}$ variable, add clauses that require

   $GOTATTACK_{j} = (INDSET_{1} \land ATTACK_{1,j})$ $\lor$ ... $\lor$ $(INDSET_{n} \land ATTACK_{n,j})$

   These clauses record which arguments have been attacked by the stable set arguments.

4. For each $GOTATTACK_{i}$ variable, add clauses that require

   $NEEDATTACK_{i} \oplus \overline{GOTATTACK_{i}}$

   These clauses require that every argument that needed to be attacked by some stable set argument was in fact attacked.

The Boolean expressions can be converted to circuits and from there to CNF using Tseitin transformations.

To obtain all the stable sets, when the SAT solver returns a set of $INDSET$ variables, you must construct a CNF clauses that forbids that solution and append it to the CNF formula. Rerun the solver and it will either find a new solution or report that the formula is now unsatisfiable. If "unsatisfiable" is reported, then you know you've found all the stable sets. If a new solution is found, construct another CNF clause to forbid that solution, append it to the formula and run the solver again.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/12135

 Ask a Question

 Download Related Notes/Documents