Modeling the problem of finding all stable sets of an argumentation framework as SAT

Question

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.

Answer 1

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.

Answer 2

The SAT solvers I have used are designed to find one solution. There are also SAT solvers that exhaustively eliminate all possible solutions, intended for random SAT benchmark instances. These solvers are optimized to discard information during search, instead focusing on finding one (or the presence of one) solution. Optimizing for enumerating all solutions requires a different approach, maintaining a memory-efficient data structure containing all the information found during search. If your approach requires finding all different solutions or optimizing over them, then more general tools may be needed. (Although sometimes it is perfectly reasonable to re-run the solver from scratch for a large number of different instances where each forbids the solutions found previously; if the runtime is low enough then it does not matter that the runs do not share data.) For a good list of state-of-the-art SAT solvers, many freely available, see the results of the SAT Challenge 2012.

I cannot prescribe a particular solver since I do not have a good handle on your problem domain. Personally, I would try to express a small but nontrivial instance of your problem as a constraint satisfaction problem using the MiniZinc language or using the Minion input format, as a sequence of SAT instances, as a Z3 SMT instance, and as as an input to clasp. By doing so, you will likely find aspects of some of these tools have limitations that make them more or less suitable for your task. I would initially do this quickly, to quickly explore the space of tools, then focus more time on the one or two most promising tools.

(The ordering above reflects my personal familiarity with the toolsets, not any particular recommendation. Note that clasp tends to perform well at the SAT Challenge.)

However, expressing real problems in these generic modelling paradigms is often challenging. There is even an annual workshop that deals with the general problem of modelling and model reformulation. Application papers describing how to use SAT/CP/SMT/ASP approaches to solve specific new problems are definitely welcome at the main conferences in these areas.