Parameter Setting in SAT Solver using Machine Learning Techniques

被引:2
作者
Beskyd, Filip [1 ]
Surynek, Pavel [1 ]
机构
[1] Czech Tech Univ, Fac Informat Technol, Thakurova 9, Prague 16000 6, Czech Republic
来源
ICAART: PROCEEDINGS OF THE 14TH INTERNATIONAL CONFERENCE ON AGENTS AND ARTIFICIAL INTELLIGENCE - VOL 2 | 2022年
关键词
SAT Problem; Boolean Satisfiability; Solver; Graph Structure; Machine Learning; Heuristic Parameter Tuning; ALGORITHM;
D O I
10.5220/0010910200003116
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
Boolean satisfiability (SAT) solvers are essential tools for many domains in computer science and engineering. Modern complete search-based SAT solvers represent a universal problem solving tool which often provide higher efficiency than ad-hoc direct solving approaches. Over the course of at least two decades of SAT related research, many variable and value selection heuristics were devised. Heuristics can usually be tuned by single or multiple numerical parameters prior to executing the search process over the concrete SAT instance. In this paper we present a machine learning approach that predicts the parameters of heuristic from the underlying structure of the input SAT instance.
引用
收藏
页码:586 / 597
页数:12
相关论文
共 22 条
[1]  
Ansotegui Carlos, 2012, P 15 INT C THEORY AP, P410, DOI DOI 10.1007/978-3-642-31612-8
[2]   A comparison between SAT and CSP techniques [J].
Bennaceur, H .
CONSTRAINTS, 2004, 9 (02) :123-138
[3]   Bounded model checking [J].
Biere, Armin .
Frontiers in Artificial Intelligence and Applications, 2009, 185 (01) :457-481
[4]  
Cook S. A., 1971, Proceedings of the 3rd annual ACM symposium on theory of computing, P151
[5]  
D'Ippolito N, 2010, LECT NOTES COMPUT SC, V5977, P160, DOI 10.1007/978-3-642-11811-1_13
[6]  
Dennis Greg, 2006, Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006, Portland, Maine, USA, July 17-20, 2006, P109, DOI [DOI 10.1145/1146238.1146251, 10.1145/1146238. 1146251]
[7]   Effective preprocessing in SAT through variable and clause elimination [J].
Eén, N ;
Biere, A .
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, PROCEEDINGS, 2005, 3569 :61-75
[8]   An extensible SAT-solver [J].
Eén, N ;
Sörensson, N .
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, 2004, 2919 :502-518
[9]  
Ganesh V., 2009, AVATARSAT AUTOTUNING
[10]  
Gupta A, 2006, LECT NOTES COMPUT SC, V3965, P108