Document Open Access Logo

On the Satisfiability of Smooth Grid CSPs

Authors Vasily Alferov, Mateus de Oliveira Oliveira

PDF
Thumbnail PDF

File

LIPIcs.SEA.2022.18.pdf
  • Filesize: 0.79 MB
  • 14 pages

Document Identifiers

Author Details

Vasily Alferov
  • National Research University Higher School of Economics, Saint Petersburg, Russia
Mateus de Oliveira Oliveira
  • University of Bergen, Norway

Funding

  • de Oliveira Oliveira, Mateus: Research Council of Norway, Grant Numbers 288761 and 326537.

Cite As Get BibTex

Vasily Alferov and Mateus de Oliveira Oliveira. On the Satisfiability of Smooth Grid CSPs. In 20th International Symposium on Experimental Algorithms (SEA 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 233, pp. 18:1-18:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.SEA.2022.18

Abstract

Many important NP-hard problems, arising in a wide variety of contexts, can be reduced straightforwardly to the satisfiability problem for CSPs whose underlying graph is a grid. In this work, we push forward the study of grid CSPs by analyzing, from an experimental perspective, a symbolic parameter called smoothness.
More specifically, we implement an algorithm that provably works in polynomial time on grids of polynomial smoothness. Subsequently, we compare our algorithm with standard combinatorial optimization techniques, such as SAT-solving and integer linear programming (ILP). For this comparison, we use a class of grid-CSPs encoding the pigeonhole principle. We demonstrate, empirically, that these CSPs have polynomial smoothness and that our algorithm terminates in polynomial time.
On the other hand, as strong evidence that the grid-like encoding is not destroying the essence of the pigeonhole principle, we show that the standard propositional translation of pigeonhole CSPs remains hard for state-of-the-art SAT solvers, such as minisat and glucose, and even to state-of-the-art integer linear-programming solvers, such as Coin-OR CBC.

Subject Classification

ACM Subject Classification
  • Theory of computation → Discrete optimization
Keywords
  • Grid CSPs
  • Smoothness
  • SAT Solving
  • Linear Programming

Metrics

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

Supplementary Materials

References

  1. Gilles Audemard and Laurent Simon. On the glucose SAT solver. Int. J. Artif. Intell. Tools, 27(1):1840001:1-1840001:25, 2018. URL: https://doi.org/10.1142/S0218213018400018.
  2. Paul Beame, Henry Kautz, and Ashish Sabharwal. Towards understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research, pages 319-351, 2004. Google Scholar
  3. Paul Beame and Toniann Pitassi. Simplified and improved resolution lower bounds. In Foundations of Computer Science, 1996. Proceedings., 37th Annual Symposium on, pages 274-282. IEEE, 1996. Google Scholar
  4. Samuel R Buss, Jan Hoffmann, and Jan Johannsen. Resolution trees with lemmas: Resolution refinements that characterize DLL algorithms with clause learning. Logical Methods in Computer Science, 4, 2008. Google Scholar
  5. Alessandra Cherubini, Stefano Crespi Reghizzi, Matteo Pradella, and Pierluigi San Pietro. Picture languages: Tiling systems versus tile rewriting grammars. Theoretical Computer Science, 356(1):90-103, 2006. Google Scholar
  6. Mateus de Oliveira Oliveira. Satisfiability via smooth pictures. In International Conference on Theory and Applications of Satisfiability Testing, pages 13-28. Springer, 2016. Google Scholar
  7. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Theory and applications of satisfiability testing, pages 502-518. Springer, 2003. Google Scholar
  8. John Forrest and Robin Lougee-Heimer. Cbc user guide. In Emerging theory, methods, and applications, pages 257-277. INFORMS, 2005. Google Scholar
  9. Dora Giammarresi and Antonio Restivo. Recognizable picture languages. International Journal of Pattern Recognition and Artificial Intelligence, 6(2&3):241-256, 1992. Google Scholar
  10. Armin Haken. The intractability of resolution. Theoretical Computer Science, 39:297-308, 1985. Google Scholar
  11. Philipp Hertel, Fahiem Bacchus, Toniann Pitassi, and Allen Van Gelder. Clause learning can effectively P-simulate general propositional resolution. In Proc. of the 23rd National Conference on Artificial Intelligence (AAAI 2008), pages 283-290, 2008. Google Scholar
  12. Changwook Kim and Ivan Hal Sudborough. The membership and equivalence problems for picture languages. Theoretical Computer Science, 52(3):177-191, 1987. Google Scholar
  13. Jan Krajíček. Lower bounds to the size of constant-depth propositional proofs. The Journal of Symbolic Logic, 59(01):73-86, 1994. Google Scholar
  14. Jan Krajíček, Pavel Pudlák, and Alan Woods. An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle. Random Structures & Algorithms, 7(1):15-39, 1995. Google Scholar
  15. Michel Latteux and David Simplot. Recognizable picture languages and domino tiling. Theoretical computer science, 178(1):275-283, 1997. Google Scholar
  16. Hermann A Maurer, Grzegorz Rozenberg, and Emo Welzl. Using string languages to describe picture languages. Information and Control, 54(3):155-185, 1982. Google Scholar
  17. Matthew W Moskewicz, Conor F Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th annual Design Automation Conference, pages 530-535. ACM, 2001. Google Scholar
  18. Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence, 175(2):512-525, 2011. Google Scholar
  19. Toniann Pitassi, Paul Beame, and Russell Impagliazzo. Exponential lower bounds for the pigeonhole principle. Computational complexity, 3(2):97-140, 1993. Google Scholar
  20. Azriel Rosenfeld. Picture languages: formal models for picture recognition. Academic Press, 2014. Google Scholar
  21. David Simplot. A characterization of recognizable picture languages by tilings by finite sets. Theoretical Computer Science, 218(2):297-323, 1999. Google Scholar
  22. Gift Stromoney, Rani Siromoney, and Kamala Krithivasan. Abstract families of matrices and picture languages. Computer Graphics and Image Processing, 1(3):284-307, 1972. Google Scholar
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact