Document Open Access Logo

Effective Auxiliary Variables via Structured Reencoding

Authors Andrew Haberlandt , Harrison Green , Marijn J. H. Heule

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.11.pdf
  • Filesize: 3.81 MB
  • 19 pages

Document Identifiers

Author Details

Andrew Haberlandt
  • Carnegie Mellon University, Pittsburgh, PA, USA
Harrison Green
  • Carnegie Mellon University, Pittsburgh, PA, USA
Marijn J. H. Heule
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

The authors are supported by National Science Foundation grant CCF-2015445.
  • Haberlandt, Andrew: NSF Graduate Research Fellowship Grant No. DGE-2140739.

Acknowledgements

The authors thank Bernardo Subercaseaux for his assistance revising this paper, and the Pittsburgh Supercomputing Center for allowing us to use the Bridges2 [Brown et al., 2021] cluster for our experiments.

Cite AsGet BibTex

Andrew Haberlandt, Harrison Green, and Marijn J. H. Heule. Effective Auxiliary Variables via Structured Reencoding. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.11

Abstract

Extended resolution shows that auxiliary variables are very powerful in theory. However, attempts to exploit this potential in practice have had limited success. One reasonably effective method in this regard is bounded variable addition (BVA), which automatically reencodes formulas by introducing new variables and eliminating clauses, often significantly reducing formula size. We find motivating examples suggesting that the performance improvement caused by BVA stems not only from this size reduction but also from the introduction of effective auxiliary variables. Analyzing specific packing-coloring instances, we discover that BVA is fragile with respect to formula randomization, relying on variable order to break ties. With this understanding, we augment BVA with a heuristic for breaking ties in a structured way. We evaluate our new preprocessing technique, Structured BVA (SBVA), on more than 29 000 formulas from previous SAT competitions and show that it is robust to randomization. In a simulated competition setting, our implementation outperforms BVA on both randomized and original formulas, and appears to be well-suited for certain families of formulas.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Reencoding
  • Auxiliary Variables
  • Extended Resolution

Metrics

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

Supplementary Materials

References

  1. Tomas Balyo, Marijn J.H. Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2022: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B. Department of Computer Science, University of Helsinki, Finland, 2022. Google Scholar
  2. A. Biere, A. Biere, M. Heule, H. van Maaren, and T. Walsh. Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, NLD, 2009. Google Scholar
  3. Armin Biere and Marijn Heule. The effect of scrambling CNFs. In Proceedings of Pragmatics of SAT, volume 59, pages 111-126, 2019. Google Scholar
  4. Armin Biere, Matti Järvisalo, and Benjamin Kiesl. Preprocessing in SAT solving. Handbook of Satisfiability, 336:391-435, 2021. Google Scholar
  5. Maria Luisa Bonet and Katherine St John. Efficiently calculating evolutionary tree measures using SAT. In Theory and Applications of Satisfiability Testing-SAT 2009: 12th International Conference, SAT 2009, Swansea, UK, June 30-July 3, 2009. Proceedings 12, pages 4-17. Springer, 2009. Google Scholar
  6. Pierre Bouvier and Hubert Garavel. Efficient algorithms for three reachability problems in safe petri nets. In Didier Buchs and Josep Carmona, editors, Application and Theory of Petri Nets and Concurrency, pages 339-359, Cham, 2021. Springer International Publishing. Google Scholar
  7. Shawn T. Brown, Paola Buitrago, Edward Hanna, Sergiu Sanielevici, Robin Scibek, and Nicholas A. Nystrom. Bridges-2: A platform for rapidly-evolving and data intensive research. In Practice and Experience in Advanced Research Computing, PEARC '21, New York, NY, USA, 2021. Association for Computing Machinery. Google Scholar
  8. Stephen A Cook. A short proof of the pigeon hole principle using extended resolution. Acm Sigact News, 8(4):28-32, 1976. Google Scholar
  9. Niklas Eén and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. SAT, 3569:61-75, 2005. Google Scholar
  10. Katalin Fazekas, Markus Sinnl, Armin Biere, and Sophie Parragh. Duplex encoding of staircase at-most-one constraints for the antibandwidth problem. In Integration of Constraint Programming, Artificial Intelligence, and Operations Research: 17th International Conference, CPAIOR 2020, Vienna, Austria, September 21-24, 2020, Proceedings 17, pages 186-204. Springer, 2020. Google Scholar
  11. Armin Haken. The intractability of resolution. Theoretical Computer Science, 39:297-308, 1985. Third Conference on Foundations of Software Technology and Theoretical Computer Science. Google Scholar
  12. Markus Iser and Carsten Sinz. A problem meta-data library for research in SAT. In Daniel Le Berre and Matti Järvisalo, editors, Proceedings of Pragmatics of SAT 2015 and 2018, volume 59 of EPiC Series in Computing, pages 144-152. EasyChair, 2019. Google Scholar
  13. W. Klieber and G. Kwon. Efficient CNF encoding for selecting 1 from n objects. In Fourth Workshop on Constraints in Formal Verification (CFV), 2007. Google Scholar
  14. Petr Kučera, Petr Savickỳ, and Vojtěch Vorel. A lower bound on CNF encodings of the at-most-one constraint. Theoretical Computer Science, 762:51-73, 2019. Google Scholar
  15. Norbert Manthey, Marijn JH Heule, and Armin Biere. Automated reencoding of boolean formulas. In Haifa Verification Conference, pages 102-117. Springer, 2012. Google Scholar
  16. Norbert Manthey and Peter Steinke. Too many rooks. Proceedings of SAT competition, pages 97-98, 2014. Google Scholar
  17. Gi-Joon Nam, Fadi Aloul, Karem Sakallah, and Rob Rutenbar. A comparative study of two boolean formulations of FPGA detailed routing constraints. In Proceedings of the 2001 International Symposium on Physical Design, pages 222-227, 2001. Google Scholar
  18. Neil Newman, Alexandre Fréchette, and Kevin Leyton-Brown. Deep optimization for spectrum repacking. Communications of the ACM, 61(1):97-104, 2017. Google Scholar
  19. O. Roussel. Another SAT to CSP conversion. In 16th IEEE International Conference on Tools with Artificial Intelligence, pages 558-565, 2004. Google Scholar
  20. Carsten Sinz. Towards an optimal CNF encoding of boolean cardinality constraints. In Peter van Beek, editor, Principles and Practice of Constraint Programming - CP 2005, pages 827-831, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  21. Bernardo Subercaseaux and Marijn JH Heule. The packing chromatic number of the infinite square grid is at least 14. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  22. Bernardo Subercaseaux and Marijn JH Heule. The packing chromatic number of the infinite square grid is 15. arXiv preprint, 2023. URL: https://arxiv.org/abs/2301.09757.
  23. Grigori S Tseitin. On the complexity of derivation in propositional calculus. In Studies in Mathematics and Mathematical Logic 2, pages 115-125, 1968. 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 Imprint Privacy Contact