Document Open Access Logo

Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT

Authors Anshujit Sharma , Matthew Burns , Michael C. Huang

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.25.pdf
  • Filesize: 4.23 MB
  • 21 pages

Document Identifiers

Author Details

Anshujit Sharma
  • Department of Electrical and Computer Engineering, University of Rochester, NY, USA
Matthew Burns
  • Department of Electrical and Computer Engineering, University of Rochester, NY, USA
Michael C. Huang
  • Department of Electrical and Computer Engineering, University of Rochester, NY, USA

Cite As Get BibTex

Anshujit Sharma, Matthew Burns, and Michael C. Huang. Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 25:1-25:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.SAT.2023.25

Abstract

Dynamical solvers for combinatorial optimization are usually based on 2superscript{nd} degree polynomial interactions, such as the Ising model. These exhibit high success for problems that map naturally to their formulation. However, SAT requires higher degree of interactions. As such, these quadratic dynamical solvers (QDS) have shown poor solution quality due to excessive auxiliary variables and the resulting increase in search-space complexity. Thus recently, a series of cubic dynamical solver (CDS) models have been proposed for SAT and other problems. We show that such problem-agnostic CDS models still perform poorly on moderate to large problems, thus motivating the need to utilize SAT-specific heuristics. With this insight, our contributions can be summarized into three points. First, we demonstrate that existing make-only heuristics perform poorly on scale-free, industrial-like problems when integrated into CDS. This motivates us to utilize break counts as well. Second, we derive a relationship between make/break and the CDS formulation to efficiently recover break counts. Finally, we utilize this relationship to propose a new make/break heuristic and combine it with a state-of-the-art CDS which is projected to solve SAT problems several orders of magnitude faster than existing software solvers.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Probabilistic algorithms
  • Computer systems organization → Analog computers
Keywords
  • Satisfiability
  • Ising machines
  • Stochastic Heuristics
  • Natural Computation

Metrics

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

Supplementary Materials

References

  1. Richard Afoakwa, Yiqiao Zhang, Uday Kumar Reddy Vengalam, Zeljko Ignjatovic, and Michael Huang. Brim: Bistable resistively-coupled Ising machine. 2021 IEEE International Symposium on High-Performance Computer Architecture (HPCA), pages 749-760, 2021. URL: https://doi.org/10.1109/HPCA51647.2021.00068.
  2. Tameem Albash and Daniel A. Lidar. Adiabatic quantum computation. Rev. Mod. Phys., 90:015002, January 2018. URL: https://doi.org/10.1103/RevModPhys.90.015002.
  3. Tasniem Nasser Alyahya, Mohamed El Bachir Menai, and Hassan Mathkour. On the structure of the boolean satisfiability problem: A survey. ACM Computing Surveys (CSUR), 55(3):1-34, 2022. Google Scholar
  4. Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. On the structure of industrial SAT instances. In Principles and Practice of Constraint Programming-CP 2009: 15th International Conference, CP 2009 Lisbon, Portugal, September 20-24, 2009 Proceedings 15, pages 127-141. Springer, 2009. Google Scholar
  5. Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. Towards industrial-like random SAT instances. In Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI'09, pages 387-392, San Francisco, CA, USA, 2009. Morgan Kaufmann Publishers Inc. Google Scholar
  6. Masashi Aono, Makoto Naruse, Song-Ju Kim, Masamitsu Wakabayashi, Hirokazu Hori, Motoichi Ohtsu, and Masahiko Hara. Amoeba-inspired nanoarchitectonic computing: Solving intractable computational problems using nanoscale photoexcitation transfer dynamics. Langmuir : the ACS journal of surfaces and colloids, 29, April 2013. URL: https://doi.org/10.1021/la400301p.
  7. Daniel Azses, Maxime Dupont, Bram Evert, Matthew J. Reagor, and Emanuele G. Dalla Torre. Navigating the noise-depth tradeoff in adiabatic quantum circuits, 2022. URL: https://doi.org/10.48550/arXiv.2209.11245.
  8. Adrian Balint and Uwe Schöning. Choosing probability distributions for stochastic local search and the role of make versus break. In SAT, 2012. Google Scholar
  9. Mohammad Khairul Bashar, Antik Mallick, Avik W. Ghosh, and Nikhil Shukla. Dynamical system-based computational models for solving combinatorial optimization on hypergraphs. IEEE Journal on Exploratory Solid-State Computational Devices and Circuits, pages 1-1, 2023. URL: https://doi.org/10.1109/JXCDC.2023.3235113.
  10. Tomas Baylo, Marijn J.H. Heule, Markus Iser, Matti Järvisalo, and Martin Suda. Proceedings of SAT competition 2022: Solver and benchmark descriptions. In Proceedings of SAT Competition 2022 : Solver and Benchmark Descriptions, volume B-2022-1 of Department of Computer Science Series of Publications B, Helsinki, 2022. Department of Computer Science, University of Helsinki. URL: http://hdl.handle.net/10138/347211.
  11. Kishor Bharti, Alba Cervera-Lierta, Thi Ha Kyaw, Tobias Haug, Sumner Alperin-Lea, Abhinav Anand, Matthias Degroote, Hermanni Heimonen, Jakob S. Kottmann, Tim Menke, Wai-Keong Mok, Sukin Sim, Leong-Chuan Kwek, and Alán Aspuru-Guzik. Noisy intermediate-scale quantum algorithms. Rev. Mod. Phys., 94:015004, February 2022. URL: https://doi.org/10.1103/RevModPhys.94.015004.
  12. Zhengbing Bian, Fabian Chudak, William Macready, Aidan Roy, Roberto Sebastiani, and Stefano Varotti. Solving sat (and maxsat) with a quantum annealer: Foundations, encodings, and preliminary results. Information and Computation, 275:104609, 2020. URL: https://doi.org/10.1016/j.ic.2020.104609.
  13. 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
  14. Armin Biere and Mathias Fleury. Gimsatul, IsaSAT, Kissat entering the SAT competition 2022. In Proceedings of SAT Competition 2022 : Solver and Benchmark Descriptions, 2022. Google Scholar
  15. Sami Boulebnane and Ashley Montanaro. Solving boolean satisfiability problems with the quantum approximate optimization algorithm, 2022. URL: https://doi.org/10.48550/arXiv.2208.06909.
  16. Connor Bybee, Denis Kleyko, Dmitri E Nikonov, Amir Khosrowshahi, Bruno A Olshausen, and Friedrich T Sommer. Efficient optimization with higher-order Ising machines. arXiv preprint, 2022. URL: https://arxiv.org/abs/2212.03426.
  17. Muya Chang, Xunzhao Yin, Zoltan Toroczkai, Xiaobo Hu, and Arijit Raychowdhury. An analog clock-free compute fabric base on continuous-time dynamical system for solving combinatorial optimization problems. In 2022 IEEE Custom Integrated Circuits Conference (CICC), pages 1-2, 2022. URL: https://doi.org/10.1109/CICC53496.2022.9772850.
  18. Mohamed Sami Cherif, Djamal Habet, and Cyril Terrioux. Combining vsids and chb using restarts in SAT. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021. Google Scholar
  19. Tzuu-Shuh Chiang, Chii-Ruey Hwang, and Shuenn Jyi Sheu. Diffusion for global optimization in ℝⁿ. SIAM Journal on Control and Optimization, 25(3):737-753, 1987. URL: https://doi.org/10.1137/0325042.
  20. D-WAVE. minorminer, 2014. URL: https://github.com/dwavesystems/minorminer.
  21. D-WAVE. Operation and timing, 2022. URL: https://docs.dwavesys.com/docs/latest/c_qpu_timing.html.
  22. John D. Davis, Zhangxi Tan, Fang Yu, and Lintao Zhang. A practical reconfigurable hardware accelerator for boolean satisfiability solvers. In Proceedings of the 45th Annual Design Automation Conference, DAC '08, pages 780-785, New York, NY, USA, 2008. Association for Computing Machinery. URL: https://doi.org/10.1145/1391469.1391669.
  23. Mária Ercsey-Ravasz and Zoltán Toroczkai. Optimization hardness as transient chaos in an analog approach to constraint satisfaction. Nature Physics, 7(12):966-970, 2011. Google Scholar
  24. Edward Farhi, Jeffrey Goldstone, and Sam Gutmann. A quantum approximate optimization algorithm, 2014. URL: https://doi.org/10.48550/arXiv.1411.4028.
  25. D. Freedman and P. Drineas. Energy minimization via graph cuts: settling what is possible. In 2005 IEEE Computer Society Conference on Computer Vision and Pattern Recognition (CVPR'05), volume 2, pages 939-946 vol. 2, 2005. URL: https://doi.org/10.1109/CVPR.2005.143.
  26. Thomas Gabor, Sebastian Zielinski, Sebastian Feld, Christoph Roch, Christian Seidel, Florian Neukart, Isabella Galter, Wolfgang Mauerer, and Claudia Linnhoff-Popien. Assessing solution quality of 3SAT on a quantum annealing platform, 2019. URL: https://doi.org/10.48550/arXiv.1902.04703.
  27. Hayato Goto, Kosuke Tatsumura, and Alexander R Dixon. Combinatorial optimization by simulating adiabatic bifurcations in nonlinear hamiltonian systems. Science advances, 5(4):eaav2372, 2019. Google Scholar
  28. Kanupriya Gulati, Suganth Paul, Sunil P. Khatri, Srinivas Patil, and Abhijit Jas. Fpga-based hardware acceleration for boolean satisfiability. ACM Trans. Des. Autom. Electron. Syst., 14(2), April 2009. URL: https://doi.org/10.1145/1497561.1497576.
  29. Ryan Hamerly, Takahiro Inagaki, Peter L. McMahon, Davide Venturelli, Alireza Marandi, Tatsuhiro Onodera, Edwin Ng, Carsten Langrock, Kensuke Inaba, Toshimori Honjo, Koji Enbutsu, Takeshi Umeki, Ryoichi Kasahara, Shoko Utsunomiya, Satoshi Kako, Ken ichi Kawarabayashi, Robert L. Byer, Martin M. Fejer, Hideo Mabuchi, Dirk Englund, Eleanor Rieffel, Hiroki Takesue, and Yoshihisa Yamamoto. Experimental investigation of performance differences between coherent Ising machines and a quantum annealer. Science Advances, 5(5):eaau0823, 2019. URL: https://doi.org/10.1126/sciadv.aau0823.
  30. Kazuaki Hara, Naoki Takeuchi, Masashi Aono, and Yuko Hara-Azumi. Amoeba-inspired stochastic hardware sat solver. In 20th International Symposium on Quality Electronic Design (ISQED), pages 151-156, 2019. URL: https://doi.org/10.1109/ISQED.2019.8697729.
  31. Takahiro Inagaki, Yoshitaka Haribara, Koji Igarashi, Tomohiro Sonobe, Shuhei Tamate, Toshimori Honjo, Alireza Marandi, Peter L McMahon, Takeshi Umeki, Koji Enbutsu, et al. A coherent Ising machine for 2000-node optimization problems. Science, 354(6312):603-606, 2016. Google Scholar
  32. Tadashi Kadowaki and Hidetoshi Nishimori. Quantum annealing in the transverse Ising model. Physical Review E, 58(5):5355-5363, November 1998. URL: https://doi.org/10.1103/physreve.58.5355.
  33. Taro Kanao and Hayato Goto. Simulated bifurcation for higher-order cost functions. Applied Physics Express, 16(1):014501, 2022. Google Scholar
  34. Henry Kautz. Walksat, 2018. URL: https://gitlab.com/HenryKautz/Walksat.
  35. Scott Kirkpatrick, C Daniel Gelatt Jr, and Mario P Vecchi. Optimization by simulated annealing. science, 220(4598):671-680, 1983. Google Scholar
  36. V. Kolmogorov and R. Zabin. What energy functions can be minimized via graph cuts? IEEE Transactions on Pattern Analysis and Machine Intelligence, 26(2):147-159, 2004. URL: https://doi.org/10.1109/TPAMI.2004.1262177.
  37. Jia Hui Liang, Vijay Ganesh, Ed Zulkoski, Atulan Zaman, and Krzysztof Czarnecki. Understanding vsids branching heuristics in conflict-driven clause-learning SAT solvers. In Hardware and Software: Verification and Testing: 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings 11, pages 225-241. Springer, 2015. Google Scholar
  38. Andrew Lucas. Ising formulations of many NP problems. Frontiers in Physics, 2:5, 2014. Google Scholar
  39. Debasis Mitra, Fabio Romeo, and Alberto Sangiovanni-Vincentelli. Convergence and finite-time behavior of simulated annealing. In 1985 24th IEEE Conference on Decision and Control, pages 761-767, 1985. URL: https://doi.org/10.1109/CDC.1985.268600.
  40. Ferenc Molnár, Shubha R Kharel, Xiaobo Sharon Hu, and Zoltán Toroczkai. Accelerating a continuous-time analog SAT solver using gpus. Computer Physics Communications, 256:107469, 2020. Google Scholar
  41. Anh Hoang Ngoc Nguyen, Masashi Aono, and Yuko Hara-Azumi. Amoeba-inspired hardware sat solver with effective feedback control. In 2019 International Conference on Field-Programmable Technology (ICFPT), pages 243-246, 2019. URL: https://doi.org/10.1109/ICFPT47387.2019.00038.
  42. Tiemo Pedergnana and Nicolas Noiray. Exact potentials in multivariate langevin equations. Chaos: An Interdisciplinary Journal of Nonlinear Science, 32(12):123146, 2022. URL: https://doi.org/10.1063/5.0124031.
  43. Irina Rish and Rina Dechter. Resolution versus search: Two strategies for SAT. Journal of Automated Reasoning, 24(1-2):225-275, 2000. Google Scholar
  44. I. G. Rosenberg. Reduction of bivalent maximization to the quadratic case. Cahiers du Centre d'Etudes de Recherche Operationnelle, 17:71-74, 1975. Google Scholar
  45. Bart Selman, Henry A Kautz, Bram Cohen, et al. Local search strategies for satisfiability testing. Cliques, coloring, and satisfiability, 26:521-532, 1993. Google Scholar
  46. Anshujit Sharma, Richard Afoakwa, Zeljko Ignjatovic, and Michael Huang. Increasing Ising machine capacity with multi-chip architectures. In Proceedings of the 49th Annual International Symposium on Computer Architecture, ISCA '22, pages 508-521, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3470496.3527414.
  47. Anshujit Sharma, Matthew Burns, Andrew Hahn, and Michael Huang. Augmented electronic ising machine as an effective sat solver, 2023. URL: https://arxiv.org/abs/2305.01623.
  48. Yong Shim, Abhronil Sengupta, and Kaushik Roy. Biased random walk using stochastic switching of nanomagnets: Application to SAT solver. IEEE Transactions on Electron Devices, 65(4):1617-1624, 2018. URL: https://doi.org/10.1109/TED.2018.2808232.
  49. Ali Asgar Sohanghpurwala and Peter Athanas. An effective probability distribution SAT solver on reconfigurable hardware. In 2016 International Conference on ReConFigurable Computing and FPGAs (ReConFig), pages 1-6. IEEE, 2016. Google Scholar
  50. Ali Asgar Sohanghpurwala, Mohamed W. Hassan, and Peter M. Athanas. Hardware accelerated SAT solvers - a survey. J. Parallel Distributed Comput., 106:170-184, 2017. Google Scholar
  51. Juexiao Su, Tianheng Tu, and Lei He. A quantum annealing approach for boolean satisfiability problem. In Proceedings of the 53rd Annual Design Automation Conference, pages 1-6, 2016. Google Scholar
  52. Tianshi Wang, Leon Wu, and Jaijeet Roychowdhury. New computational results and hardware prototypes for oscillator-based Ising machines. In Proceedings of the 56th Annual Design Automation Conference 2019, DAC '19, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3316781.3322473.
  53. Yulun Wang and Predrag S. Krstic. Prospect of using groverquotesingles search in the noisy-intermediate-scale quantum-computer era. Physical Review A, 102(4), October 2020. URL: https://doi.org/10.1103/physreva.102.042609.
  54. Ryan Williams. Maximum Two-Satisfiability, pages 507-510. Springer US, Boston, MA, 2008. URL: https://doi.org/10.1007/978-0-387-30162-4_227.
  55. Pan Xu, Jinghui Chen, Difan Zou, and Quanquan Gu. Global convergence of langevin dynamics based algorithms for nonconvex optimization. Advances in Neural Information Processing Systems, 31, 2018. Google Scholar
  56. Xunzhao Yin, Behnam Sedighi, Melinda Varga, Maria Ercsey-Ravasz, Zoltan Toroczkai, and Xiaobo Sharon Hu. Efficient analog circuits for boolean satisfiability. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 26(1):155-167, 2017. Google Scholar
  57. Yiqiao Zhang, Uday Kumar Reddy Vengalam, Anshujit Sharma, Michael Huang, and Zeljko Ignjatovic. Qubrim: A cmos compatible resistively-coupled Ising machine with quantized nodal interactions. In Proceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design, ICCAD '22, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3508352.3549443.
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