早期文献给出的SAT术语

SAT问题的通俗表述

Given a propositional formula, determining whether there exists a truth assignment for its propositional variables such that the formula evaluates to true is called the propositional Satisfiability problem, commonly abbreviated as SAT.

完备算法与不完备算法的表述

A solution method is said to be complete if it guarantees (given enough time) to find a solution if it exists, or prove lack of solution otherwise.

Incomplete, or stochastic, methods, on the contrary, cannot guarantee finding the solution, although they may scale better than complete methods on some large satisfiable problems.

sat已被证明是NP完全问题

Moreover, SAT carries considerable theoretical interest as the original NP-complete problem [A5, A8].

A5.  S.A. Cook. The Complexity of Theorem-Proving Procedures. In Proceedings of Third Annual ACM Symposium on Theory of Computing, 1971.

A8. M.R. Garey and D.S. Johnson. Computers and Intractability: A Guide to the Theory of NPCompleteness. W.H. Freeman and co., San Francisco, 1979.

主要组件及其对应来源文献 

Modern implementations of CDCL SAT solvers employ a lot of heuristics. Some of them can be considered baseline, such as：

the Variable State Independent Decaying Sum (VSIDS) [6],
restarts [7],
Literal Block Distance (LBD) [8].

Learnt Clause Minimization (LCM) [9],
Distance (Dist) heuristic [10],
Chronological Backtracking (ChronoBT) [11],
duplicate learnts heuristic [12],
Conflict History-Based (CHB) heuristic [13],
Learning Rate-based Branching (LRB) heuristic [14],
and the SLS component [15].

[B6] Moskewicz, M.W.; Madigan, C.F.; Zhao, Y.; Zhang, L.; Malik, S. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference (IEEE Cat. No.01CH37232), Las Vegas, NV, USA, 22 June 2001; pp. 530–535.

[B7] Luby, M.; Sinclair, A.; Zuckerman, D. Optimal speedup of Las Vegas algorithms. Inf. Process. Lett. 1993, 47, 173–180.

[B8] Audemard, G.; Simon, L. Predicting Learnt Clauses Quality in Modern SAT Solvers. In Proceedings of the 21st International Jont Conference on Artifical Intelligence, Pasadena, CA, USA, 11–17 July 2009; IJCAI’09. pp. 399–404.

[B9] Luo, M.; Li, C.M.; Xiao, F.; Manyà, F.; Lü, Z. An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17, Melbourne, Australia 19–25 August 2017; pp. 703–711.

[B13] Liang, J.H.; Ganesh, V.; Poupart, P.; Czarnecki, K. Exponential Recency Weighted Average Branching Heuristic for SAT Solvers. In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, Phoenix, AZ, USA, 12–17 February 2016; AAAI’16. pp. 3434–3440.

[B14] Liang, J.H.; Ganesh, V.; Poupart, P.; Czarnecki, K. Learning Rate Based Branching Heuristic for SAT Solvers. In Proceedings of the Theory and Applications of Satisfiability Testing—SAT 2016—19th International Conference, Bordeaux, France, 5–8 July 2016; Creignou, N., Berre, D.L., Eds.; Springer: Berlin/Heidelberg, Germany, 2016; Volume 9710, pp. 123–140.

[B15] Zhang, X.; Cai, S. Relaxed Backtracking with Rephasing. In Proceedings of the SAT Competition 2020, Alghero, Italy, 3–10 July 2020; Solver and Benchmark Descriptions. University of Helsinki, Department of Computer Science: Helsinki, Finland, 2020; Volume B-2020-1, pp. 15–16.