Machine Learning Methods in Solving the Boolean Satisfiability Problem

Wenxuan Guo; Hui-Ling Zhen; Xijun Li; Wanqian Luo; Mingxuan Yuan; Yaohui Jin; Junchi Yan

doi:10.1007/s11633-022-1396-2

Volume 20 Issue 5

October 2023

Turn off MathJax

Article Contents

Relative Articles

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

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

Citation:

PDF( 1558 KB)

Machine Learning Methods in Solving the Boolean Satisfiability Problem

doi: 10.1007/s11633-022-1396-2

Wenxuan Guo^{1

,},
Hui-Ling Zhen^{2

,},
Xijun Li^{2

,},
Wanqian Luo^{2

,},
Mingxuan Yuan^{2

,},
Yaohui Jin^{1

,},
Junchi Yan^{1

,}

1.
MoE Key Laboratory of Artificial Intelligence, Shanghai Jiao Tong University, Shanghai 200240, China
2.
Noah′s Ark Laboratory, Huawei Ltd., Shenzhen 518129, China

More Information

Author Bio:
Wenxuan Guo received the B. Sc. degree in computer science and technology from Shanghai Jiao Tong University, China in 2021. Currently, she is a Ph. D. degree candidate in computer science and technology at Department of Computer Science and Engineering, Shanghai Jiao Tong University, China. Her research interests include machine learning and combinatorial optimization. E-mail: arya_g@sjtu.edu.cn ORCID iD: 0000-0001-6336-3819

Hui-Ling Zhen received the B. Sc. degree in numerical mathematics and the Ph. D. degree in applied mathematics from Beijing University of Posts and Telecommunications, China in 2011and 2016, respectively. She was a post-doctoral research fellow in City University of Hong Kong, China from 2016 to 2019. Currently, she is a research scientist in Noah′s Ark Laboratory, Huawei, China since 2019. She has published over 60 peer-reviewed papers in mainstream conferences and journals. Her research interests include large-scale optimization, constraint programming, as well as their applications in supply chain management and chip design. E-mail: zhenhuiling2@huawei.com

Xijun Li received M. Sc. degree in computer science from Shanghai Jiao Tong University, China in 2018. Currently, he is a senior researcher of Huawei Noah′s Ark Laboratory, China, and also is a Ph. D. degree candidate in Electronic Engineering and information science at University of Science and Technology of China (HUAWEI-USTC Joint Ph. D. Program). He has published several papers on top peer-reviewed conferences and journals (SIGMOD, KDD, ICDE, DAC, CIKM, ICDCS, TCYB, etc.). His research interests include learning to optimize combinatorial optimization problem and machine learning for computer systems. E-mail: xijun.li@huawei.com (Corresponding author) ORCID iD: 0000-0002-9013-1180

Wanqian Luo received the B. Sc. degree in numerical mathematics and the M. Eng. degree in software engineer from South China University of Technology, China in 2016 and 2019respectively. After that, he is a research engineer of Huawei Noah′s Ark Laboratory, China. His research interests include applied formal methods, Boolean satisfiability problem, as well as the applications in chip design. E-mail: luowanqian1@huawei.com

Mingxuan Yuan received the Ph. D. degree in computer science from Hong Kong University of Science and Technology, China in 2011. He is currently a principal researcher of Huawei Noah′s Ark Laboratory, China. His research interests include data-driven optimization algorithms, data-driven SAT/MIP solving algorithms and data-driven EDA algorithm. E-mail: Yuan.Mingxuan@huawei.com

Yaohui Jin received the Ph. D. degree in electronic engineering from Shanghai Jiao Tong University, China in 2000. He is a tenured professor in School of Electronic Information and Electrical Engineering and Artificial Intelligence Institute, Shanghai Jiao Tong University, China. He was a member of technical staff at Bell Labs Research, China from 2000 to 2002. His research interests include software defined infrastructure, spatial and temporal data mining as well as natural language understanding. E-mail: jinyh@sjtu.edu.cn (Corresponding author) ORCID iD: 0000-0001-6158-6277

Junchi Yan received the B. Eng. degree in automation from University of Science and Technology Beijing, China in 2008, and the M. Sc. degree in pattern recognition and intelligent systems, and the Ph.D. degree in information and communication engineering, both from Shanghai Jiao Tong University, China in 2011 and 2015, respectively. He is an associate professor with Department of Computer Science and Engineering, and AI Institute of Shanghai Jiao Tong University, China. Before that, he was a senior research staff member with IBM Research where he started his career since April 2011. He served as Area Chair for NeurIPS/ICML/CVPR/AAAI/ACM-MM and Senior PC for IJCAI/CIKM, and Associate Editor for Pattern Recognition. His research interests include machine learning (especially for combinatorial optimization) and computer vision. E-mail: yanjunchi@sjtu.edu.cn (Corresponding author) ORCID iD: 0000-0001-9639-7679
Received Date: 2022-07-01
Accepted Date: 2022-11-23
Publish Online: 2023-06-01
Publish Date: 2023-10-01

Abstract

Abstract

This paper reviews the recent literature on solving the Boolean satisfiability problem (SAT), an archetypal $ {\cal{NP}}$-complete problem, with the aid of machine learning (ML) techniques. Over the last decade, the machine learning society advances rapidly and surpasses human performance on several tasks. This trend also inspires a number of works that apply machine learning methods for SAT solving. In this survey, we examine the evolving ML SAT solvers from naive classifiers with handcrafted features to emerging end-to-end SAT solvers, as well as recent progress on combinations of existing conflict-driven clause learning (CDCL) and local search solvers with machine learning methods. Overall, solving SAT with machine learning is a promising yet challenging research topic. We conclude the limitations of current works and suggest possible future directions. The collected paper list is available at https://github.com/Thinklab-SJTU/awesome-ml4co.
- Machine learning (ML),
- Boolean satisfiability (SAT),
- deep learning,
- graph neural networks (GNNs),
- combinatorial optimization

¹ https://satcompetition.github.io/² https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html

³The satisfiability of a formula is not affected by permuting the variables, the clauses or the literals within a clause. It is also not affected by negating every literal corresponding to a given variable^[14].

FullText(HTML)

References(89)

References

[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.

Relative Articles

Supplements(0)

Cited By

Proportional views

Proportional views

通讯作者: 陈斌, bchen63@163.com

1.
沈阳化工大学材料科学与工程学院沈阳 110142

Figures(3) / Tables(2)

Get Citation

PDF

XML

Entire Issue PDF

用微信扫码二维码

分享至好友和朋友圈

Article Metrics

Article views (444) PDF downloads(24)

Machine Learning Methods in Solving the Boolean Satisfiability Problem

doi: 10.1007/s11633-022-1396-2

Abstract

References

Proportional views

Catalog

通讯作者: 陈斌, bchen63@163.com

Article Metrics

Proportional views

Related

Machine Learning Methods in Solving the Boolean Satisfiability Problem

doi: 10.1007/s11633-022-1396-2

Abstract

References

Proportional views

Catalog

通讯作者: 陈斌, bchen63@163.com

Article Metrics

Proportional views

Related

Export File

Citation

Format

Content