Document Open Access Logo

Engineering an Efficient PB-XOR Solver

Authors Jiong Yang, Kuldeep S. Meel

PDF
Thumbnail PDF

File

LIPIcs.CP.2021.58.pdf
  • Filesize: 0.98 MB
  • 20 pages

Document Identifiers

Author Details

Jiong Yang
  • School of Computing, National University of Singapore, Singapore
Kuldeep S. Meel
  • School of Computing, National University of Singapore, Singapore

Funding

This work was supported in part by National Research Foundation Singapore under its NRF Fellowship Programme [NRF-NRFFAI1-2019-0004] and AI Singapore Programme [AISG-RP-2018-005], and NUS ODPRT Grant [R-252-000-685-13]. The computational work for this article was fully performed on resources of the National Supercomputing Centre, Singapore (https://www.nscc.sg).

Acknowledgements

We are grateful to the anonymous reviewer for pointing out a subtle bug in the presentation of Algorithm 1. We are thankful to Priyanka Golia and Yang Suwei for their detailed feedback on the early drafts of the paper.

Cite AsGet BibTex

Jiong Yang and Kuldeep S. Meel. Engineering an Efficient PB-XOR Solver. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 58:1-58:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CP.2021.58

Abstract

Despite the NP-completeness of Boolean satisfiability, modern SAT solvers are routinely able to handle large practical instances, and consequently have found wide ranging applications. The primary workhorse behind the success of SAT solvers is the widely acclaimed Conflict Driven Clause Learning (CDCL) paradigm, which was originally proposed in the context of Boolean formulas in CNF. The wide ranging applications of SAT solvers have highlighted that for several domains, CNF is not a natural representation and the reliance of modern SAT solvers on resolution proof system limit their ability to efficiently solve several families of constraints. Consequently, the past decade has witnessed the design of solvers with native support for constraints such as Pseudo-Boolean (PB) and CNF-XOR. The primary contribution of our work is an efficient solver engineered for PB-XOR formulas, i.e., formulas consisting of a conjunction of PB and XOR constraints. We first observe that a simple adaption of CNF-XOR architecture does not provide an improvement over baseline; our analysis highlights the need for careful engineering of the order of propagations. To this end, we propose three different tactics, all of which achieve significant performance improvements over the baseline. Our work is motivated by applications arising from binarized neural network verification where the verification of properties such as robustness, fairness, trojan attacks can be reduced to model counting queries; the state of the art model counters reduce counting to polynomially many SAT queries over the original formula conjuncted with randomly generated XOR constraints. To this end, we augment ApproxMC with LinPB and we call the resulting counter as ApproxMCPB. In an extensive empirical comparison over 1076 benchmarks, we observe that ApproxMCPB can solve 912 instances while the baseline version of ApproxMC4 (augmented with CryptoMiniSat) can solve only 802 instances.

Subject Classification

ACM Subject Classification
  • Theory of computation
  • Computing methodologies → Artificial intelligence
Keywords
  • PB-XOR Solving
  • Pseudo-Boolean
  • XOR
  • Gauss Jordan Elimination
  • SAT-Solving
  • Model Counting

Metrics

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

Supplementary Materials

References

  1. Dimitris Achlioptas, Zayd S. Hammoudeh, and Panos Theodoropoulos. Fast sampling of perfectly uniform satisfying assignments. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018, pages 135-147, Cham, 2018. Springer International Publishing. Google Scholar
  2. Teodora Baluta, Shiqi Shen, Shweta Shine, Kuldeep S. Meel, and Prateek Saxena. Quantitative verification of neural networks and its security applications. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (CCS), November 2019. Google Scholar
  3. D. Chai and A. Kuehlmann. A fast pseudo-boolean constraint solver. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24(3):305-317, 2005. URL: https://doi.org/10.1109/TCAD.2004.842808.
  4. Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. A scalable approximate model counter. In Proceedings of International Conference on Constraint Programming (CP), pages 200-216, September 2013. Google Scholar
  5. Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. Improving approximate counting for probabilistic inference: From linear to logarithmic sat solver calls. In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), July 2016. Google Scholar
  6. Stephen A. Cook. The complexity of theorem-proving procedures. In Proceedings of the Third Annual ACM Symposium on Theory of Computing, STOC '71, page 151–158, New York, NY, USA, 1971. Association for Computing Machinery. URL: https://doi.org/10.1145/800157.805047.
  7. W. Cook, C.R. Coullard, and Gy. Turán. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18(1):25-38, 1987. URL: https://doi.org/10.1016/0166-218X(87)90039-4.
  8. Jo Devriendt. Watched propagation of - integer linear constraints. In Proceedings of International Conference on Constraint Programming (CP), pages 160-176, September 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_10.
  9. Heidi Dixon, Matt Ginsberg, and Andrew Parkes. Generalizing boolean satisfiability i: Background and survey of existing work. J. Artif. Intell. Res. (JAIR), 21:193-243, February 2004. URL: https://doi.org/10.1613/jair.1353.
  10. Heidi E. Dixon and Matthew L. Ginsberg. Inference methods for a pseudo-boolean satisfiability solver. In Eighteenth National Conference on Artificial Intelligence, page 635–640, USA, 2002. American Association for Artificial Intelligence. Google Scholar
  11. N. Eén and Niklas Sörensson. Translating pseudo-boolean constraints into sat. J. Satisf. Boolean Model. Comput., 2:1-26, 2006. Google Scholar
  12. Jan Elffers and Jakob Nordström. Divide and conquer: Towards faster pseudo-boolean solving. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI-18, pages 1291-1299. International Joint Conferences on Artificial Intelligence Organization, July 2018. URL: https://doi.org/10.24963/ijcai.2018/180.
  13. Stefano Ermon, Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Taming the curse of dimensionality: Discrete integration by hashing and optimization. In Proceedings of the 30th International Conference on International Conference on Machine Learning - Volume 28, ICML'13, page II–334–II–342. JMLR.org, 2013. Google Scholar
  14. Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Model counting: A new strategy for obtaining good bounds. In Proceedings of the 21st National Conference on Artificial Intelligence - Volume 1, AAAI'06, page 54–61. AAAI Press, 2006. Google Scholar
  15. Armin Haken. The intractability of resolution. Theoretical Computer Science, 39:297-308, 1985. Third Conference on Foundations of Software Technology and Theoretical Computer Science. URL: https://doi.org/10.1016/0304-3975(85)90144-6.
  16. Cheng-Shen Han and Jie-Hong Roland Jiang. When boolean satisfiability meets gaussian elimination in a simplex way. In P. Madhusudan and Sanjit A. Seshia, editors, Computer Aided Verification, pages 410-426, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Google Scholar
  17. John Hooker. Generalized resolution for 0–1 linear inequalities. Annals of Mathematics and Artificial Intelligence, 6:271-286, March 1992. URL: https://doi.org/10.1007/BF01531033.
  18. Saurabh Joshi, Ruben Martins, and Vasco M. Manquinho. Generalized totalizer encoding for pseudo-boolean constraints. In Gilles Pesant, editor, Principles and Practice of Constraint Programming - 21st International Conference, CP 2015, Cork, Ireland, August 31 - September 4, 2015, Proceedings, volume 9255 of Lecture Notes in Computer Science, pages 200-209. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23219-5_15.
  19. Jean-Marie Lagniez and Pierre Marquis. A recursive algorithm for projected model counting. Proceedings of the AAAI Conference on Artificial Intelligence, 33(01):1536-1543, July 2019. URL: https://doi.org/10.1609/aaai.v33i01.33011536.
  20. Daniel Le Berre and Anne Parrain. The sat4j library, release 2.2. JSAT, 7:59-6, January 2010. Google Scholar
  21. Leonid A. Levin. Universal sequential search problems. Problems of Information Transmission, 9(3), 1973. Google Scholar
  22. J.P. Marques-Silva and K.A. Sakallah. Grasp: a search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506-521, 1999. URL: https://doi.org/10.1109/12.769433.
  23. Ruben Martins, Vasco Manquinho, and Inês Lynce. Open-wbo: A modular maxsat solver,. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014, pages 438-445, Cham, 2014. Springer International Publishing. Google Scholar
  24. Kuldeep S. Meel. Constrained Counting and Sampling: Bridging the Gap between Theory and Practice. PhD thesis, Rice University, 2017. Google Scholar
  25. Kuldeep S. Meel, Moshe Y. Vardi, Supratik Chakraborty, Daniel J. Fremont, Sanjit A. Seshia, Dror Fried, Alexander Ivrii, and Sharad Malik. Constrained sampling and counting: Universal hashing meets sat solving. In Proceedings of Workshop on Beyond NP(BNP), 2016. Google Scholar
  26. Alexander Nadel and Vadim Ryvchin. Chronological backtracking. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018, pages 111-121, Cham, 2018. Springer International Publishing. Google Scholar
  27. Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, and Toby Walsh. Verifying Properties of Binarized Deep Neural Networks. arXiv e-prints, page arXiv:1709.06662, 2017. URL: http://arxiv.org/abs/1709.06662.
  28. Olivier Roussel and Vasco Manquinho. Pseudo-boolean and cardinality constraints. In Handbook of satisfiability, pages 695-733. IOS Press, 2009. Google Scholar
  29. Kenji Hashimoto Ryosuke Suzuki and Masahiko Sakai. Improvement of projected model-counting solver with component decomposition using sat solving in components. JSAI Technical Report, SIG-FPAI-103-B506:31-36, March 2017. in Japanese. Google Scholar
  30. Masahiko SAKAI and Hidetomo NABESHIMA. Construction of an robdd for a pb-constraint in band form and related techniques for pb-solvers. IEICE Transactions on Information and Systems, E98.D(6):1121-1127, 2015. URL: https://doi.org/10.1587/transinf.2014FOP0007.
  31. Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. Ganak: A scalable probabilistic exact model counter. In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), 2019. Google Scholar
  32. H.M. Sheini and K.A. Sakallah. Pueblo: a modern pseudo-boolean sat solver. In Design, Automation and Test in Europe, pages 684-685 Vol. 2, 2005. URL: https://doi.org/10.1109/DATE.2005.246.
  33. Hossein Sheini and Karem Sakallah. Pueblo: A hybrid pseudo-boolean sat solver. JSAT, 2:165-189, March 2006. URL: https://doi.org/10.3233/SAT190020.
  34. Mate Soos, Stephan Gocht, and Kuldeep S. Meel. Tinted, detached, and lazy cnf-xor solving and its applications to counting and sampling. In Proceedings of International Conference on Computer-Aided Verification (CAV), July 2020. Google Scholar
  35. Mate Soos and Kuldeep S. Meel. Bird: Engineering an efficient cnf-xor sat solver and its applications to approximate model counting. In Proceedings of AAAI Conference on Artificial Intelligence (AAAI), January 2019. Google Scholar
  36. Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending sat solvers to cryptographic problems. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, pages 244-257, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  37. G. S. Tseitin. On the complexity of derivation in propositional calculus. Automation of Reasoning, pages 466-483, 1983. URL: https://doi.org/10.1007/978-3-642-81955-1_28.
  38. Alasdair Urquhart. Hard examples for resolution. J. ACM, 34(1):209–219, 1987. URL: https://doi.org/10.1145/7531.8928.
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