Timeline for Modeling the problem of finding all stable sets of an argumentation framework as SAT
Current License: CC BY-SA 3.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 30, 2013 at 18:11 | comment | added | Kyle Jones | Let's move this to chat. | |
| May 30, 2013 at 16:25 | comment | added | Dchris | But how can i transform clauses 3 to CNF if the number of arguments are different every time?I tried to explicitly define the values of all GOTATTACKs and remove clauses 3 but it didn't work.. | |
| May 26, 2013 at 0:37 | comment | added | Kyle Jones | OK, I see where it went off the rails. Section 3 needs to make the GOTATTACK variables the output of an or-gate which is fed by and-ing the relevant INDSET and ATTACK variables. I've corrected the answer to reflect that. | |
| May 26, 2013 at 0:33 | history | edited | Kyle Jones | CC BY-SA 3.0 |
changed section 3 to make GOTATTACK the output of an or-gate full of and's to make the logic work properly
|
| May 25, 2013 at 16:32 | comment | added | Dchris | The above clauses don't work in the following case.Having 4 arguments and the attacks: ATTACK1,2 ATTACK 2,1 and ATTACK3,4 the solver returns as one of the solutions: INDSET1=F,INDSET2=F,INDSET3=T,INDSET4=F, which is a wrong solution.The problem is that the clauses can't check whether the arguments not in the stable set are being attacked by the arguments in the stable set(only argument 3 in this case) or by any other argument.I tried to figure out how i can check that but i couldn't imagine how.Any ideaS? | |
| May 24, 2013 at 17:34 | comment | added | Dchris | I forgot to mention that an argument inside a stable set(INDSET of that argument is TRUE) can be attacked by an argument not in the set if and only if any argument in the stable set(including itself too) is attacking back that argument.So i changed the final set of clauses(4th) and i made it NOT NEEDATTACKi OR GOTATTACKi.This allows an argument to got attack even if it does not need an attack(allows GOTATTACK to be TRUE even if NEEDATTACK is FALSE). That also covers everything else that was covered from the previous version of clauses No4 | |
| May 24, 2013 at 17:14 | comment | added | Kyle Jones | Yes, that's it exactly. | |
| May 24, 2013 at 17:06 | comment | added | Dchris | The input of a sat solver is all the clauses and the output is unsatisfiable or an assignment of values for each variable that makes all clauses true.I am not sure what do you mean by using ATTACKi,j as input.Do you mean that i have to add a new clause for every ATTACKi,j variable(eg if ATTACK1,2 is false and it's number in the cnf file is 3 then the clause will be -3 0 ) or do you mean something else? | |
| May 24, 2013 at 16:49 | comment | added | Kyle Jones | Yes, ATTACKi,j is the input. You must use all the clauses together. | |
| May 24, 2013 at 15:59 | comment | added | Dchris | Also,will i run all clauses at once or run each type of clauses separately(there are 4 types of clauses according to your answer) | |
| May 24, 2013 at 14:43 | comment | added | Dchris | Will the variables ATTACKi,j be the input? | |
| May 24, 2013 at 14:04 | vote | accept | Dchris | ||
| May 21, 2013 at 2:52 | history | answered | Kyle Jones | CC BY-SA 3.0 |