布尔可满足性问题
可满足性
变量(数学)
逻辑回归
蒙特卡罗方法
计算机科学
解算器
预处理器
命题公式
算法
数学
人工智能
统计
命题变量
数学优化
数学分析
描述逻辑
中间逻辑
标识
DOI:10.1145/3017680.3022464
摘要
In this project, we aimed to improve the runtime of Minisat, a Conflict-Driven Clause Learning (CDCL) solver that solves the Propositional Boolean Satisfiability (SAT) problem. We first used a logistic regression model to predict the satisfiability of propositional boolean formulae after fixing the values of a certain fraction of the variables in each formula. We then applied the logistic model and added a preprocessing period to Minisat to determine the preferable initial value (either true or false) of each boolean variable using a Monte-Carlo approach. Concretely, for each Monte-Carlo trial, we fixed the values of a certain ratio of randomly selected variables, and calculated the confidence that the resulting sub-formula is satisfiable with our logistic regression model. The initial value of each variable was set based on the mean confidence scores of the trials that started from the literals of that variable. We were particularly interested in setting the initial values of the backbone variables correctly, which are variables that have the same value in all solutions of a SAT formula. Our Monte-Carlo method was able to set 78% of the backbones correctly. Excluding the preprocessing time, compared with the default setting of Minisat, the runtime of Minisat for satisfiable formulae decreased by 23%. However, our method did not outperform vanilla Minisat in runtime, as the decrease in the conflicts was outweighed by the long runtime of the preprocessing period.
科研通智能强力驱动
Strongly Powered by AbleSci AI