Citation: | Wenxuan Guo, Hui-Ling Zhen, Xijun Li, Wanqian Luo, Mingxuan Yuan, Yaohui Jin, Junchi Yan. Machine Learning Methods in Solving the Boolean Satisfiability Problem. Machine Intelligence Research, vol. 20, no. 5, pp.640-655, 2023. https://doi.org/10.1007/s11633-022-1396-2 |
[1] |
S. A. Cook. The complexity of theorem-proving procedures. In Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, Shaker Heights, USA, pp. 151–158, 1971. DOI: 10.1145/800157.805047.
|
[2] |
K. Iwama, S. Miyazaki. SAT-variable complexity of hard combinatorial problems. In Proceedings of IFIP Transactions A: Computer Science and Technology, vol. 51, pp. 253–258, 1994.
|
[3] |
M. N. Velev. Exploiting hierarchy and structure to efficiently solve graph coloring as SAT. In Proceedings of IEEE/ACM International Conference on Computer-aided Design, IEEE, San Jose, USA, pp. 135–142, 2007. DOI: 10.1109/ICCAD.2007.4397256.
|
[4] |
R. Plachetta, A. Van Der Grinten. SAT-and-Reduce for vertex cover: Accelerating branch-and-reduce by SAT solving. In Proceedings of Symposium on Algorithm Engineering and Experiments, Philadelphia, USA, pp. 169–180, 2021. DOI: 10.1137/1.9781611976472.13.
|
[5] |
S. Skansi, K. Šekrst, M. Kardum. A different approach for clique and household analysis in synthetic telecom data using propositional logic. In Proceedings of the 43rd International Convention on Information, Communication and Electronic Technology, IEEE, Opatija, Croatia, pp. 1286–1289, 2020. DOI: 10.23919/MIPRO48935.2020.9245421.
|
[6] |
J. Brakensiek, M. Heule, J. Mackey, D. Narváez. The resolution of Keller′s conjecture. In Proceedings of the 10th International Joint Conference on Automated Reasoning, Springer, Paris, France, pp. 48–65, 2020. DOI: 10.1007/978-3-030-51074-9_4.
|
[7] |
H. T. Zhang, J. H. R. Jiang, A. Mishchenko. A circuit-based sat solver for logic synthesis. In Proceedings of IEEE/ACM International Conference on Computer Aided Design, IEEE, Munich, Germany, 2021. DOI: 10.1109/ICCAD51958.2021.9643505.
|
[8] |
Y. Bengio, A. Lodi, A. Prouvost. Machine learning for combinatorial optimization: A methodological tour d′horizon. European Journal of Operational Research, vol. 290, no. 2, pp. 405–421, 2021. DOI: 10.1016/j.ejor.2020.07.063.
|
[9] |
J. C. Yan, S. Yang, E. Hancock. Learning for graph matching and related combinatorial optimization problems. In Proceedings of the 29th International Joint Conference on Artificial Intelligence, ACM, Yokohama, Japan, Article number 694, 2021. DOI: 10.5555/3491440.3492134.
|
[10] |
J. Y. Zhang, C. Liu, X. J. Li, H. L. Zhen, M. X. Yuan, Y. W. Li, J. C. Yan. A survey for solving mixed integer programming via machine learning. Neurocomputing, vol. 519, pp. 205–217, 2023. DOI: 10.1016/j.neucom.2022.11.024.
|
[11] |
M. S. Cherif, D. Habet, C. Terrioux. Combining VSIDS and CHB using restarts in SAT. In Proceedings of the 27th International Conference on Principles and Practice of Constraint Programming, Dagstuhl, Germany, vol. 210, Article number 20, 2021. DOI: 10.4230/LIPIcs.CP.2021.20.
|
[12] |
M. S. Cherif, D. Habet, C. Terrioux. Kissat MAB: Combining VSIDS and CHB through multi-armed bandit. In Proceedings of SAT Competition: Solver and Benchmark Descriptions, University of Helsinki, Helsinki, Finland, pp. 15–16, 2021.
|
[13] |
J. H. Liang, C. Oh, V. Ganesh, K. Czarnecki, P. Poupart. MapleCOMSPS, MapleCOMSPS LRB, MapleCOMSPS CHB. In Proceedings of SAT Competition: Solver and Benchmark Descriptions, University of Helsinki, Helsinki, Finland, pp. 52–53, 2016.
|
[14] |
D. Selsam, M. Lamm, B. Bünz, P. Liang, L. De Moura, D. L. Dill. Learning a SAT solver from single-bit supervision. In Proceedings of the 7th International Conference on Learning Representations, New Orleans, USA, 2019.
|
[15] |
A. Popescu, S. Polat-Erdeniz, A. Felfernig, M. Uta, M. Atas, V. M. Le, K. Pilsl, M. Enzelsberger, T. N. T. Tran. An overview of machine learning techniques in constraint solving. Journal of Intelligent Information Systems, vol. 58, no. 1, pp. 91–118, 2022. DOI: 10.1007/s10844-021-00666-5.
|
[16] |
S. B. Holden. Machine learning for automated theorem proving: Learning to solve SAT and QSAT. Foundations and Trends® in Machine Learning, vol. 14, no. 6, pp. 807–989, 2021. DOI: 10.1561/2200000081.
|
[17] |
F. Hutter, L. Xu, H. H. Hoos, K. Leyton-Brown. Algorithm runtime prediction: Methods & evaluation. Artificial Intelligence, vol. 206, pp. 79–111, 2014. DOI: 10.1016/j.artint.2013.10.003.
|
[18] |
M. J. H. Heule, A. Biere. Proofs for satisfiability problems. All About Proofs,Proofs for All, vol. 55, no. 1, pp. 1–22, 2015.
|
[19] |
A. Biere, M. Heule, H. Van Maaren, T. Walsh. Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications, Amsterdam, The Netherlands: IOS Press, 2009.
|
[20] |
J. P. Marques-Silva, K. A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, vol. 48, no. 5, pp. 506–521, 1999. DOI: 10.1109/12.769433.
|
[21] |
M. Davis, G. Logemann, D. Loveland. A machine program for theorem-proving. Communications of the ACM, vol. 5, no. 7, pp. 394–397, 1962. DOI: 10.1145/368273.368557.
|
[22] |
M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, S. Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference, IEEE, Las Vegas, USA, pp. 530–535, 2001. DOI: 10.1145/378239.379017.
|
[23] |
A. Biere, A. Fröhlich. Evaluating CDCL variable scoring schemes. In Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing, Springer, Austin, USA, pp. 405–422, 2015. DOI: 10.1007/978-3-319-24318-4_29.
|
[24] |
A. Biere. Adaptive restart strategies for conflict driven SAT solvers. In Proceedings of the 11th International Conference on Theory and Applications of Satisfiability Testing, Springer, Guangzhou, China, pp. 28–33, 2008. DOI: 10.1007/978-3-540-79719-7_4.
|
[25] |
J. H. Liang, V. Ganesh, P. Poupart, K. Czarnecki. Learning rate based branching heuristic for SAT solvers. In Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing, Springer, Bordeaux, France, pp. 123–140, 2016. DOI: 10.1007/978-3-319-40970-2_9.
|
[26] |
F. Xiao, C. M. Li, M. Luo, F. Manyà, Z. Lü, Y. Li. A branching heuristic for SAT solvers based on complete implication graphs. Science China Information Sciences, vol. 62, no. 7, Article number 72103, 2019. DOI: 10.1007/s11432-017-9467-7.
|
[27] |
B. Selman, H. A. Kautz, B. Cohen. Local search strategies for satisfiability testing. In Proceedings of a DIMACS Workshop on Cliques, Coloring, and Satisfiability, New Brunswick, USA, pp. 521–532, 1993.
|
[28] |
G. Audemard, L. Simon. Predicting learnt clauses quality in modern SAT solvers. In Proceedings of the 21st International Joint Conference on Artificial Intelligence, ACM, Pasadena, USA, pp. 399–404, 2009. DOI: 10.5555/1661445.1661509.
|
[29] |
B. Selman, H. Levesque, D. Mitchell. A new method for solving hard satisfiability problems. In Proceedings of the 10th National Conference on Artificial Intelligence, San Jose, USA, pp. 440–446, 1992. DOI: 10.5555/1867135.1867203.
|
[30] |
A. Balint, A. Fröhlich. Improving stochastic local search for SAT with a new probability distribution. In Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing, Springer, Edinburgh, UK, pp. 10–15, 2010. DOI: 10.1007/978-3-642-14186-7_3.
|
[31] |
A. Balint, U. Schöning. Choosing probability distributions for stochastic local search and the role of make versus break. In Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing, Springer, Trento, Italy, pp. 16–29, 2012. DOI: 10.1007/978-3-642-31612-8_3.
|
[32] |
S. W. Cai, C. Luo, K. L. Su. CCAnr: A configuration checking based local search solver for non-random satisfiability. In Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing, Springer, Austin, USA, pp. 1–8, 2015. DOI: 10.1007/978-3-319-24318-4_1.
|
[33] |
A. Biere. Splatz, lingeling, plingeling, treengeling, YalSAT entering the SAT competition. In Proceedings of SAT Competition: Solver and Benchmark Descriptions, Helsinki, Finland, pp. 44–45, 2016.
|
[34] |
S. W. Cai, X. D. Zhang. Deep cooperation of CDCL and local search for SAT. In Proceedings of the 24th International Conference on Theory and Applications of Satisfiability Testing, Springer, Barcelona, Spain, pp. 64–81, 2021. DOI: 10.1007/978-3-030-80223-3_6.
|
[35] |
H. H. Hoos, T. Stützle. SATLIB: An online resource for research on SAT. In Proceedings of the Highlights of Satisfiability Research in the Year 2000, Amsterdam, The Netherlands, pp. 283–292, 2000.
|
[36] |
T. N. Alyahya, M. El Bachir Menai, H. Mathkour. On the structure of the boolean satisfiability problem: A survey. ACM Computing Surveys, vol. 55, no. 3, Article number 46, 2023.
|
[37] |
M. I. Jordan, T. M. Mitchell. Machine learning: Trends, perspectives, and prospects. Science, vol. 349, no. 6245, pp. 255–260, 2015. DOI: 10.1126/science.aaa8415.
|
[38] |
B. Xi, R. Wang, Y. H. Cai, T. Lu, S. Wang. A novel heterogeneous actor-critic algorithm with recent emphasizing replay memory. International Journal of Automation and Computing, vol. 18, no. 4, pp. 619–631, 2021. DOI: 10.1007/s11633-021-1296-x.
|
[39] |
C. J. C. H. Watkins, P. Dayan. Q-learning. Machine Learning, vol. 8, no. 3–4, pp. 279–292, 1992. DOI: 10.1007/BF00992698.
|
[40] |
Y. LeCun, Y. Bengio, G. Hinton. Deep learning. Nature, vol. 521, no. 7553, pp. 436–444, 2015. DOI: 10.1038/nature14539.
|
[41] |
J. Zhou, G. Q. Cui, S. D. Hu, Z. Y. Zhang, C. Yang, Z. Y. Liu, L. F. Wang, C. C. Li, M. S. Sun. Graph neural networks: A review of methods and applications. AI Open, vol. 1, pp. 57–81, 2020. DOI: 10.1016/j.aiopen.2021.01.001.
|
[42] |
T. N. Kipf, M. Welling. Semi-supervised classification with graph convolutional networks. In Proceedings of the 5th International Conference on Learning Representations, Toulon, France, [Online], Available: https://openreview.net/forum?id=HkwoSDPgg, 2017.
|
[43] |
M. H. Zhang, Y. X. Chen. Link prediction based on graph neural networks. In Proceedings of the 32nd International Conference on Neural Information Processing Systems, ACM, Montreal, Canada, pp. 5171–5181, 2018. DOI: 10.5555/3327345.3327423.
|
[44] |
H. J. Dai, E. B. Khalil, Y. Y. Zhang, B. Dilkina, L. Song. Learning combinatorial optimization algorithms over graphs. In Proceedings of the 31st International Conference on Neural Information Processing Systems, ACM, Long Beach, USA, pp. 6351–6361, 2017. DOI: 10.5555/3295222.3295382.
|
[45] |
D. S. Lopera, L. Servadei, G. N. Kiprit, R. Wille, W. Ecker. A comprehensive survey on electronic design automation and graph neural networks: Theory and applications. ACM Transactions on Design Automation of Electronic Systems, vol. 28, no. 2, Article number 15, 2022.
|
[46] |
R. Y. Cheng, J. C. Yan. On joint learning for solving placement and routing in chip design. In Proceedings of the 34th Conference on Neural Information Processing Systems, pp. 16508–16519, 2021.
|
[47] |
R. Y. Cheng, X. L. Lv, Y. Li, J. J. Ye, J. Y. Hao, J. C. Yan. The policy-gradient placement and generative routing neural networks for chip design. In Proceedings of the 36th Conference on Neural Information Processing Systems, 2022.
|
[48] |
Z. C. Lipton, J. Berkowitz, C. Elkan. A critical review of recurrent neural networks for sequence learning, [Online], Available: https://arxiv.org/abs/1506.00019, 2015.
|
[49] |
O. Vinyals, M. Fortunato, N. Jaitly. Pointer networks. In Proceedings of Advances in Neural Information Processing Systems 28, Montreal, Canada, pp. 2692–2700, 2015.
|
[50] |
I. J. Goodfellow, J. Pouget-Abadie, M. Mirza, B. Xu, D. Warde-Farley, S. Ozair, A. Courville, Y. Bengio. Generative adversarial nets. In Proceedings of the 27th International Conference on Neural Information Processing Systems, ACM, Montreal, Canada, vol. 2, pp. 2672–2680, 2014. DOI: 10.5555/2969033.2969125.
|
[51] |
L. Xu, F. Hutter, H. H. Hoos, K. Leyton-Brown. SATzilla: Portfolio-based algorithm selection for SAT. Journal of Artificial Intelligence Research, vol. 32, pp. 565–606, 2008. DOI: 10.1613/jair.2490.
|
[52] |
D. Devlin, B. O′Sullivan. Satisfiability as a classification problem. In Proceedings of Irish Conference on Artificial Intelligence and Cognitive Science, 2008.
|
[53] |
L. Xu, H. Hoos, K. Leyton-Brown. Predicting satisfiability at the phase transition. In Proceedings of AAAI Conference on Artificial Intelligence, Toronto, Canada vol. 26, pp. 584–590, 2021. DOI: 10.1609/aaai.v26i1.8142.
|
[54] |
M. Danisovszky, Z. G. Yang, G. Kusper. Classification of SAT problem instances by machine learning methods. In Proceedings of the 11th International Conference on Applied Informatics, Eger, Hungary, pp. 94–104, 2020.
|
[55] |
A. Atkari, N. Dhargalkar, H. Angne. Employing machine learning models to solve uniform random 3-SAT. In Proceedings of GUCON 2019 Data Communication and Networks, Springer, pp. 255–264, 2020. DOI: 10.1007/978-981-15-0132-6_17.
|
[56] |
M. N. Velev. Exploiting signal unobservability for efficient translation to CNF in formal verification of microprocessors. In Proceedings of Conference on Design, Automation and Test in Europe, IEEE, Paris, France, pp. 266–271, 2004. DOI: 10.1109/DATE.2004.1268859.
|
[57] |
L. Xu, F. Hutter, H. H. Hoos, K. Leyton-Brown. Satzilla2009: An automatic algorithm portfolio for sat. SAT, vol. 4, pp. 53–55, 2009.
|
[58] |
L. Simon. 2002. [Online], Available: http://www.satcompetition.org/2003/TOOLBOX/genAlea.c.
|
[59] |
B. Bünz, M. Lamm. Graph neural networks and Boolean satisfiability. [Online], Available: https://arxiv.org/abs/1702.03592, 2017.
|
[60] |
D. P. Kingma, J. Ba. Adam: A method for stochastic optimization. [Online], Available: https://arxiv.org/abs/1412.6980, 2015.
|
[61] |
C. Cameron, R. Chen, J. Hartford, K. Leyton-Brown. Predicting propositional satisfiability via end-to-end learning. In Proceedings of Conference on Artificial Intelligence, New York, USA, vol. 34, pp. 3324–3331, 2020. DOI: 10.1609/aaai.v34i04.5733.
|
[62] |
J. Hartford, D. Graham, K. Leyton-Brown, S. Ravanbakhsh. Deep models of interactions across sets. In Proceedings of the 35th International Conference on Machine Learning, Stockholm, Sweden, pp. 1909–1918, 2018.
|
[63] |
E. Ozolins, K. Freivalds, A. Draguns, E. Gaile, R. Zakovskis, S. Kozlovics. Goal-aware neural SAT solver. In Proceedings of International Joint Conference on Neural Networks, IEEE, Padua, Italy, 2022. DOI: 10.1109/IJCNN55064.2022.9892733.
|
[64] |
S. Amizadeh, S. Matusevych, M. Weimer. Learning to solve circuit-SAT: An unsupervised differentiable approach. In Proceedings of the 7th International Conference on Learning Representations, New Orleans, USA, 2019.
|
[65] |
D. Selsam, N. Bjorner. Guiding high-performance SAT solvers with unsat-core predictions. In Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing, Springer, Lisbon, Portugal, pp. 336–353, 2019. DOI: 10.1007/978-3-030-24258-9_24.
|
[66] |
S. Jaszczur, M. Łuszczyk, H. Michalewski. Neural heuristics for SAT solving, [Online], Available: https://arxiv.org/abs/2005.13406, 2020.
|
[67] |
V. Kurin, S. Godil, S. Whiteson, B. Catanzaro. Can Q-learning with graph networks learn a generalizable branching heuristic for a SAT solver? In Proceedings of the 34th International Conference on Neural Information Processing Systems, ACM, Vancouver, Canada, Article number 806, 2020. DOI: 10.5555/3495724.3496530.
|
[68] |
J. M. Han. Enhancing SAT solvers with glue variable predictions, [Online], Available: https://arxiv.org/abs/2007.02559, 2020.
|
[69] |
Z. Zhang, Y. Zhang. Elimination mechanism of glue variables for solving SAT problems in linguistics. In Proceedings of the Asian Conference on Language, ACL, pp. 147–167, 2021. DOI: 10.22492/issn.2435-7030.2021.11.
|
[70] |
J. Han. Learning cubing heuristics for SAT from DRAT proofs. In Proceedings of the 5th Conference on Artificial Intelligence and Theorem Proving, Aussois, France, 2020.
|
[71] |
W. X. Wang, Y. Hu, M. Tiwari, S. Khurshid, K. McMillan, R. Miikkulainen. NeuroComb: Improving SAT solving with graph neural networks, [Online], Available: https://arxiv.org/abs/2110.14053, 2021.
|
[72] |
H. Z. Wu. Improving SAT-solving with machine learning. In Proceedings of ACM SIGCSE Technical Symposium on Computer Science Education, Seattle, USA, pp. 787–788, 2017. DOI: 10.1145/3017680.3022464.
|
[73] |
J. H. Liang, C. Oh, M. Mathew, C. Thomas, C. X. Li, V. Ganesh. Machine learning-based restart policy for CDCL SAT solvers. In Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing, Springer, Oxford, UK, pp. 94–110, 2018. DOI: 10.1007/978-3-319-94144-8_6.
|
[74] |
P. Vaezipoor, G. Lederman, Y. H. Wu, R. Grosse, F. Bacchus. Learning clause deletion heuristics with reinforcement learning. In Proceedings of the 5th Conference on Artificial Intelligence and Theorem Proving, Aussois, France, 2020.
|
[75] |
J. H. Liang, V. Ganesh, P. Poupart, K. Czarnecki. Exponential recency weighted average branching heuristic for SAT solvers. In Proceedings of the 30th AAAI Conference on Artificial Intelligence, Phoenix, USA, pp. 3434–3440, 2016. DOI: 10.5555/3016100.3016385.
|
[76] |
A. Biere. CaDiCaL, lingeling, plingeling, treengeling and YalSAT entering the SAT competition 2018. In Proceedings of SAT Competition: Solver and Benchmark Descriptions, SAT, University of Helsinki, Helsinki, Finland, pp. 13–14, 2018.
|
[77] |
M. J. H. Heule, O. Kullmann, V. W. Marek. Solving very hard problems: Cube-and-conquer, a hybrid SAT solving method. In Proceedings of the 26th International Joint Conference on Artificial Intelligence, pp. 4864–4868, 2017. DOI: 10.24963/ijcai.2017/683.
|
[78] |
E. Yolcu, B. Póczos. Learning local search heuristics for Boolean satisfiability. In Proceedings of the 33rd International Conference on Neural Information Processing Systems, ACM, Red Hook, USA, Article number 718, 2019. DOI: 10.5555/3454287.3455005.
|
[79] |
R. J. Williams. Simple statistical gradient-following algorithms for connectionist reinforcement learning. Machine Learning, vol. 8, no. 3–4, pp. 229–256, 1992. DOI: 10.1007/BF00992696.
|
[80] |
Y. Bengio, J. Louradour, R. Collobert, J. Weston. Curriculum learning. In Proceedings of the 26th Annual International Conference on Machine Learning, ACM, Montreal, Canada, pp. 41–48, 2009. DOI: 10.1145/1553374.1553380.
|
[81] |
W. J. Zhang, Z. Y. Sun, Q. H. Zhu, G. Li, S. W. Cai, Y. F. Xiong, L. Zhang. NLocalSAT: Boosting local search with solution prediction. In Proceedings of the 29th International Joint Conference on Artificial Intelligence, pp. 1177–1183, 2020. DOI: 10.24963/ijcai.2020/164.
|
[82] |
B. Selman, H. Kautz, D. McAllester. Ten challenges in propositional reasoning and search. In Proceedings of the 15th International Joint Conference on Artificial Intelligence, ACM, Nagoya, Japan, pp. 50–54, 1997. DOI: 10.5555/1624162.1624170.
|
[83] |
J. Giráldez-Cru, J. Levy. Generating SAT instances with community structure. Artificial Intelligence, vol. 238, pp. 119–134, 2016. DOI: 10.1016/j.artint.2016.06.001.
|
[84] |
J. Giráldez-Cru, J. Levy. Popularity-similarity random SAT formulas. Artificial Intelligence, vol. 299, Article number 103537, 2021. DOI: 10.1016/j.artint.2021.103537.
|
[85] |
H. Z. Wu, R. Ramanujan. Learning to generate industrial SAT instances. In Proceedings of the 20th International Symposium on Combinatorial Search, Napa, USA, 2019. DOI: 10.1609/socs.v10i1.18493.
|
[86] |
J. X. You, H. Z. Wu, C. Barrett, R. Ramanujan, J. Leskovec. G2SAT: Learning to generate SAT formulas. In Proceedings of the 33rd Conference on Neural Information Processing Systems, Vancouver, Canada, 2019.
|
[87] |
I. Garzón, P. Mesejo, J. Giráldez-Cru. On the performance of deep generative models of realistic SAT instances. In Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing, Dagstuhl, Germany, Article number 3, 2022. DOI: 10.4230/LIPIcs.SAT.2022.3.
|
[88] |
W. L. Hamilton, R. Ying, J. Leskovec. Inductive representation learning on large graphs. In Proceedings of the 31st International Conference on Neural Information Processing Systems, ACM, Long Beach, USA, pp. 1025–1035, 2017. DOI: 10.5555/3294771.3294869.
|
[89] |
J. M. Crawford, L. D. Auton. Experimental results on the crossover point in random 3-SAT. Artificial Intelligence, vol. 81, no. 1–2, pp. 31–57, 1996. DOI: 10.1016/0004-3702(95)00046-1.
|