Name
Abstract | ||
|---|---|---|
This paper presents a reduction from the problem of solving parity games to the satisfiability problem in propositional logic (SAT). The reduction is done in two stages, first into difference logic, i.e. SAT combined with the theory of integer differences, an instance of the SAT modulo theories (SMT) framework. In the second stage the integer variables and constraints of the difference logic encoding are replaced with a set of Boolean variables and constraints on them, giving rise to a pure SAT encoding of the problem. The reduction uses Jurdzinski@?s characterisation of winning strategies via progress measures. The reduction is motivated by the success of SAT solvers in symbolic verification, bounded model checking in particular. The paper reports on prototype implementations of the reductions and presents some experimental results. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1016/j.jcss.2011.05.004 | J. Comput. Syst. Sci. |
Keywords | Field | DocType |
difference logic,satisfiability problem,propositional logic,propositional satisfiability,parity games,paper report,parity game,sat solvers,integer difference,integer variable,pure sat encoding,difference logic encoding,sat modulo theory | #SAT,Discrete mathematics,Combinatorics,Model checking,Boolean satisfiability problem,Propositional calculus,Zeroth-order logic,DPLL algorithm,Boolean data type,Propositional variable,Mathematics | Journal |
Volume | Issue | ISSN |
78 | 2 | Journal of Computer and System Sciences |
Citations | PageRank | References |
11 | 0.59 | 27 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Keijo Heljanko | 1 | 751 | 47.90 |
| Misa Keinänen | 2 | 38 | 3.59 |
| Martin Lange | 3 | 111 | 9.54 |
| Ilkka Niemelä | 4 | 2939 | 148.38 |