Abstract
Reductions are perhaps the most useful tool in complexity theory and, naturally, it is in general undecidable to determine whether a reduction exists between two given decision problems. However, asking for a reduction on inputs of bounded size is essentially a \(\Sigma^p_2\) problem and can in principle be solved by ASP, QBF, or by iterated calls to SAT solvers. We describe our experiences developing and benchmarking automatic reduction finders. We created a dedicated reduction finder that does counter-example guided abstraction refinement by iteratively calling either a SAT solver or BDD package. We benchmark its performance with different SAT solvers and report the tradeoffs between the SAT and BDD approaches. Further, we compare this reduction finder with the direct approach using a number of QBF and ASP solvers. We describe the tradeoffs between the QBF and ASP approaches and show which solvers perform best on our \(\Sigma^p_2\) instances. It turns out that even state-of-the-art solvers leave a large room for improvement on problems of this kind. We thus provide our instances as a benchmark for future work on \(\Sigma^p_2\) solvers.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Allender, E., Balcázar, J.L., Immerman, N.: A first-order isomorphism theorem. SIAM J. Comput. 26(2), 539–556 (1997)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)
Crouch, M., Immerman, N., Moss, J.E.B.: Finding reductions automatically. In: Blass, A., Dershowitz, N., Reisig, W. (eds.) Fields of Logic and Computation. LNCS, vol. 6300, pp. 181–200. Springer, Heidelberg (2010)
Eiter, T., Gottlob, G.: On the computational cost of disjunctive logic programming: Propositional case. Annals of Mathematics and Artificial Intelligence 15(3-4), 289–323 (1995)
Faber, W., Ricca, F.: Solving hard ASP programs efficiently. In: Baral, C., Greco, G., Leone, N., Terracina, G. (eds.) LPNMR 2005. LNCS (LNAI), vol. 3662, pp. 240–252. Springer, Heidelberg (2005)
Fagin, R.: Generalized first-order spectra and polynomial-time recognizable sets. In: Complexity of Computation, SIAM-AMS Proceedings, vol. 7, pp. 43–73. Amer. Mathematical Soc. (1974)
Gold, E.: Language identification in the limit. Inform. Control 10(5), 447–474 (1967)
Grädel, E., Kolaitis, P.G., Libkin, L., Marx, M., Spencer, J., Vardi, M.Y., Venema, Y., Weinstein, S.: Finite Model Theory and Its Applications. Texts in Theoretical Computer Science. Springer (2007)
Grohe, M.: Fixed-point logics on planar graphs. In: Proc. of LICS 1998, pp. 6–15. IEEE Computer Society (1998)
Grohe, M.: Fixed-point definability and polynomial time on graphs with excluded minors. J. ACM 59(5), 27:1–27:64 (2012)
Immerman, N.: Relational queries computable in polynomial time. Inform. Control 68, 86–104 (1986)
Immerman, N.: Languages that capture complexity classes. SIAM J. Comput. 16(4), 760–778 (1987)
Immerman, N.: Descriptive Complexity. Springer (1999)
Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 114–128. Springer, Heidelberg (2012)
Janota, M., Marques-Silva, J.: Abstraction-based algorithm for 2QBF. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 230–244. Springer, Heidelberg (2011)
Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., Scarcello, F.: The DLV system for knowledge representation and reasoning. ACM Transactions on Computational Logic 7(3), 499–562 (2006)
Peschiera, C., Pulina, L., Tacchella, A., Bubeck, U., Kullmann, O., Lynce, I.: The seventh QBF solvers evaluation (QBFEVAL’10). In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 237–250. Springer, Heidelberg (2010)
Vardi, M.Y.: The complexity of relational query languages. In: Proc. of STOC 1982, pp. 137–146. ACM (1982)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jordan, C., Kaiser, Ł. (2013). Experiments with Reduction Finding. In: Järvisalo, M., Van Gelder, A. (eds) Theory and Applications of Satisfiability Testing – SAT 2013. SAT 2013. Lecture Notes in Computer Science, vol 7962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39071-5_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-39071-5_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39070-8
Online ISBN: 978-3-642-39071-5
eBook Packages: Computer ScienceComputer Science (R0)