Document Open Access Logo

Resolution with Symmetry Rule Applied to Linear Equations

Authors Pascal Schweitzer, Constantin Seebach

PDF

File

Thumbnail PDF
PDF
LIPIcs.STACS.2021.58.pdf
  • Filesize: 0.75 MB
  • 16 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Logical Resolution
  • Symmetry Rule
  • Linear Equation System

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

This paper considers the length of resolution proofs when using Krishnamurthy’s classic symmetry rules. We show that inconsistent linear equation systems of bounded width over a fixed finite field 𝔽_p with p a prime have, in their standard encoding as CNFs, polynomial length resolutions when using the local symmetry rule (SRC-II).
As a consequence it follows that the multipede instances for the graph isomorphism problem encoded as CNF formula have polynomial length resolution proofs. This contrasts exponential lower bounds for individualization-refinement algorithms on these graphs.
For the Cai-Fürer-Immerman graphs, for which Torán showed exponential lower bounds for resolution proofs (SAT 2013), we also show that already the global symmetry rule (SRC-I) suffices to allow for polynomial length proofs.

Cite As Get BibTex

Pascal Schweitzer and Constantin Seebach. Resolution with Symmetry Rule Applied to Linear Equations. In 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 187, pp. 58:1-58:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.STACS.2021.58

Author Details

Pascal Schweitzer
  • TU Kaiserslautern, Germany
Constantin Seebach
  • TU Kaiserslautern, Germany

Funding

The research leading to these results has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (EngageS: grant agreement No. 820148).

References

  1. Noriko H. Arai and Alasdair Urquhart. Local symmetries in propositional logic. In Roy Dyckhoff, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 3-7, 2000, Proceedings, volume 1847 of Lecture Notes in Computer Science, pages 40-51. Springer, 2000. URL: https://doi.org/10.1007/10722086_3.
  2. Belaid Benhamou and Lakhdar Sais. Tractability through symmetries in propositional calculus. J. Autom. Reasoning, 12(1):89-102, 1994. URL: https://doi.org/10.1007/BF00881844.
  3. Joshua Blinkhorn and Olaf Beyersdorff. Proof complexity of QBF symmetry recomputation. In Mikolás Janota and Inês Lynce, editors, Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, volume 11628 of Lecture Notes in Computer Science, pages 36-52. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_3.
  4. Jin-yi Cai, Martin Fürer, and Neil Immerman. An optimal lower bound on the number of variables for graph identifications. Combinatorica, 12(4):389-410, 1992. URL: https://doi.org/10.1007/BF01305232.
  5. Vasek Chvátal and Endre Szemerédi. Many hard examples for resolution. J. ACM, 35(4):759-768, 1988. URL: https://doi.org/10.1145/48014.48016.
  6. Thierry Boy de la Tour and Stéphane Demri. On the complexity of extending ground resolution with symmetry rules. In Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, IJCAI 95, Montréal Québec, Canada, August 20-25 1995, pages 289-297. Morgan Kaufmann, 1995. URL: http://ijcai.org/Proceedings/95-1/Papers/038.pdf.
  7. Heidi E. Dixon, Matthew L. Ginsberg, David K. Hofer, Eugene M. Luks, and Andrew J. Parkes. Implementing a generalized version of resolution. In Deborah L. McGuinness and George Ferguson, editors, Proceedings of the Nineteenth National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence, July 25-29, 2004, San Jose, California, USA, pages 55-60. AAAI Press / The MIT Press, 2004. URL: http://www.aaai.org/Library/AAAI/2004/aaai04-009.php.
  8. Uwe Egly. A first order resolution calculus with symmetries. In Andrei Voronkov, editor, Logic Programming and Automated Reasoning,4th International Conference, LPAR'93, St. Petersburg, Russia, July 13-20, 1993, Proceedings, volume 698 of Lecture Notes in Computer Science, pages 110-121. Springer, 1993. URL: https://doi.org/10.1007/3-540-56944-8_46.
  9. Michael Frank and Michael Codish. Logic programming with graph automorphism: Integrating nauty with prolog (tool description). TPLP, 16(5-6):688-702, 2016. URL: https://doi.org/10.1017/S1471068416000223.
  10. Yuri Gurevich and Saharon Shelah. On finite rigid structures. J. Symb. Log., 61(2):549-562, 1996. URL: https://doi.org/10.2307/2275675.
  11. Armin Haken. The intractability of resolution. Theor. Comput. Sci., 39:297-308, 1985. URL: https://doi.org/10.1016/0304-3975(85)90144-6.
  12. Balakrishnan Krishnamurthy. Short proofs for tricky formulas. Acta Informatica, 22(3):253-275, August 1985. URL: https://doi.org/10.1007/BF00265682.
  13. Brendan D. McKay and Adolfo Piperno. Practical graph isomorphism, II. J. Symb. Comput., 60:94-112, 2014. URL: https://doi.org/10.1016/j.jsc.2013.09.003.
  14. Daniel Neuen and Pascal Schweitzer. An exponential lower bound for individualization-refinement algorithms for graph isomorphism. In Ilias Diakonikolas, David Kempe, and Monika Henzinger, editors, Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2018, Los Angeles, CA, USA, June 25-29, 2018, pages 138-150. ACM, 2018. URL: https://doi.org/10.1145/3188745.3188900.
  15. Pascal Schweitzer and Constantin Seebach. Resolution with symmetry rule applied to linear equations. CoRR, abs/2101.05142, 2021. (Full version of the paper). URL: http://arxiv.org/abs/2101.05142.
  16. Stefan Szeider. The complexity of resolution with generalized symmetry rules. Theory Comput. Syst., 38(2):171-188, 2005. URL: https://doi.org/10.1007/s00224-004-1192-0.
  17. Jacobo Torán. On the resolution complexity of graph non-isomorphism. In Matti Järvisalo and Allen Van Gelder, editors, Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings, volume 7962 of Lecture Notes in Computer Science, pages 52-66. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39071-5_6.
  18. G. S. Tseitin. On the Complexity of Derivation in Propositional Calculus, pages 466-483. Springer Berlin Heidelberg, Berlin, Heidelberg, 1983. URL: https://doi.org/10.1007/978-3-642-81955-1_28.
  19. Alasdair Urquhart. Hard examples for resolution. J. ACM, 34(1):209-219, January 1987. URL: https://doi.org/10.1145/7531.8928.
  20. Alasdair Urquhart. The symmetry rule in propositional logic. Discrete Applied Mathematics, 96-97:177-193, 1999. URL: https://doi.org/10.1016/S0166-218X(99)00039-6.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact