Guiding High-Performance SAT Solvers with Unsat-Core Predictions
Abstract
NeuroSAT is a method to improve CDCL solvers with predictions of unsat-cores.
can provide e?ective guidance to high-performance SAT solvers on real problems.
代碼：
https://github.com/dselsam/neurocore-public
unsat-core ： In mathematical logic, given an unsatisfiable Boolean propositional formula in conjunctive normal form, a subset of clauses whose conjunction is still unsatisfiable is called an unsatisfiable core of the original formula.
A minimum unsatisfiable core contains the smallest number of the original clauses required to still be unsatisfiable. No practical algorithms for computing the minimum core are known
An unsatisfiable core is called a minimal unsatisfiable core, if every proper subset (allowing removal of any arbitrary clause or clauses) of it is satisfiable. Thus, such a core is a local minimum, though not necessarily a global one. There are several practical methods of computing minimal unsatisfiable cores.[1][2]
Introduction
aim: 1.help inform variable branching decisions within high-performance SAT solvers on real problems
- how to make use of the predictions inside a SAT solver.
Our approach is to generate a supervised dataset mapping unsatis?able problems to the variables in their unsatis?able cores.
for some problems, the smallest core may include every variable, and of course for satis?able problems, there are no cores at all.
每一次variable branching decision都querying NeuroSAT 時間花費(fèi)過大错忱，所以選擇： 對現(xiàn)有heuritics算法進(jìn)行補(bǔ)充而不是試圖替代
branching on the free variable with the highest score.
refer to our integration strategy as periodic refocusing 稱積分策略為定期調(diào)整
pipeline:
1.通過抽取現(xiàn)有問題 Generate many unsatis?able problems
2. generate a DRAT proof, 并且extract the variables that appear in the unsat core
3.Train NeuroSAT （ NeuroCore）夸浅， map unsat problem to vaiables in the core.
4.solver定期詢問 NeuroCore证膨，通過這個網(wǎng)絡(luò)的預(yù)測 reset variable activity scores士葫。
Data Generation
to predict which variables will be involved in unsat cores
現(xiàn)有數(shù)據(jù)集過小，通過unsatis?able subproblems of existing problems來generate數(shù)據(jù)，獲得 problems with labeled cores。
Background on neural networks.
basic building block: MLP/ feed-forward network/ fully-connected network
放射變化+激活函數(shù)（recti?ed linear unit (ReLU：sets all negative numbers to zero.) ）
NeuroCore architecture.
image.png
image.png
The goal is not to learn a perfect core predictor, but rather only to learn a coarse heuristic that broadly assigns higher score to more important variables.
Hybrid Solving: Extending CDCL with NeuroCore (混合求解)
Modern SAT solvers are based on the Con?ict-Driven Clause Learning (CDCL) algorithm
image.png
NeuroCore then returns a vector ? v ∈Rnv, where a higher score for a variable indicates that NeuroCore thinks the corresponding variable is more likely to be in the core.
image.png
decay factor ρ is often rather small
Word & Phrase
此后 hereafter, afterwards, henceforth, afterward, hence
To the extent 在某種程度上
integrate集成芥备，整合
each but the last 除了最后一個的每一個
specify them by hand
A toy problem ： is a problem that doesn't have all the complexity of a real-world engineering problem. It could be a simplified or shallow version of a more difficult and intricate problem or class of problems.
Our results demonstrate that。舌菜。萌壳。
wonderful, fantastic, marvelous, intriguing, fantastical, marvellous
實(shí)用 practical, functional, pragmatic, functionary
tens of thousands of 數(shù)萬的
on-device sharing 設(shè)備共享
settle for less 退而求其次
The gains are even greater 收益更大
