%SAT及其能解决的问题
The CDCL SAT solver is an important tool for solving large real-world problems, and has been widely used in software debugging, design verification, cryptography, artificial intelligence and other fields. The powerful capabilities of modern CDCL solver comes from the fact that the framework contains many key components that work together under the guidance of various heuristic strategies.
%CDCL求解框架各种策略的组合产生强大的求解问题能力

Despite the hardness, modern CDCL SAT solvers can solve large real-world problems from important domains, such as hardware design verification [8], software debugging [4], planning [21], and encryption [18, 23], sometimes with surprising efficiency. This is the result of a careful combination of its key components, such as preprocessing [6, 10] and inprocessing [11, 17], robust branching heuristics [13, 14, 19], efficient restart policies [2, 20], intelligent conflict analysis [22], and effective clause learning [19].

Min Li, Zhengyuan Shi, Qiuxia Lai, Sadaf Khan, Shaowei Cai, Qiang Xu:
On EDA-Driven Learning for SAT Solving. DAC 2023: 1-6

The Boolean satisfiability (SAT) problem, which determines whether a combination of binary input variables exists to satisfy a given Boolean formula, has a broad range of applications, such as planning [1], scheduling [2], and verification [3].

electronic design automation (EDA) 

@inproceedings{DBLP:conf/dac/LiSLKCX23,
  author       = {Min Li and
                  Zhengyuan Shi and
                  Qiuxia Lai and
                  Sadaf Khan and
                  Shaowei Cai and
                  Qiang Xu},
  title        = {On EDA-Driven Learning for {SAT} Solving},
  booktitle    = {60th {ACM/IEEE} Design Automation Conference, {DAC} 2023, San Francisco,
                  CA, USA, July 9-13, 2023},
  pages        = {1--6},
  publisher    = {{IEEE}},
  year         = {2023},
  url          = {https://doi.org/10.1109/DAC56929.2023.10248001},
  doi          = {10.1109/DAC56929.2023.10248001},
  timestamp    = {Mon, 05 Feb 2024 20:28:08 +0100},
  biburl       = {https://dblp.org/rec/conf/dac/LiSLKCX23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

planning  dblp中搜索Planning as satisfiability可得较多的文献，其中最早及近期的文献如下：

@inproceedings{DBLP:conf/ecai/KautzS92,
  author       = {Henry A. Kautz and
                  Bart Selman},
  editor       = {Bernd Neumann},
  title        = {Planning as Satisfiability},
  booktitle    = {10th European Conference on Artificial Intelligence, {ECAI} 92, Vienna,
                  Austria, August 3-7, 1992. Proceedings},
  pages        = {359--363},
  publisher    = {John Wiley and Sons},
  year         = {1992},
  timestamp    = {Wed, 31 Jul 2019 08:45:08 +0200},
  biburl       = {https://dblp.org/rec/conf/ecai/KautzS92.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/aips/ButtnerR05,
  author       = {Markus B{\"{u}}ttner and
                  Jussi Rintanen},
  editor       = {Susanne Biundo and
                  Karen L. Myers and
                  Kanna Rajan},
  title        = {Satisfiability Planning with Constraints on the Number of Actions},
  booktitle    = {Proceedings of the Fifteenth International Conference on Automated
                  Planning and Scheduling {(ICAPS} 2005), June 5-10 2005, Monterey,
                  California, {USA}},
  pages        = {292--299},
  publisher    = {{AAAI}},
  year         = {2005},
  url          = {http://www.aaai.org/Library/ICAPS/2005/icaps05-030.php},
  timestamp    = {Fri, 05 Feb 2021 17:14:47 +0100},
  biburl       = {https://dblp.org/rec/conf/aips/ButtnerR05.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/etfa/ErosDFB21,
  author       = {Endre Er{\'{o}}s and
                  Martin Dahl and
                  Petter Falkman and
                  Kristofer Bengtsson},
  title        = {Evaluation of high level methods for efficient planning as satisfiability},
  booktitle    = {26th {IEEE} International Conference on Emerging Technologies and
                  Factory Automation, {ETFA} 2021, Vasteras, Sweden, September 7-10,
                  2021},
  pages        = {1--8},
  publisher    = {{IEEE}},
  year         = {2021},
  url          = {https://doi.org/10.1109/ETFA45728.2021.9613254},
  doi          = {10.1109/ETFA45728.2021.9613254},
  timestamp    = {Thu, 05 Oct 2023 17:14:10 +0200},
  biburl       = {https://dblp.org/rec/conf/etfa/ErosDFB21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

scheduling

@article{DBLP:journals/anor/Horbach10,
  author       = {Andrei Horbach},
  title        = {A Boolean satisfiability approach to the resource-constrained project
                  scheduling problem},
  journal      = {Ann. Oper. Res.},
  volume       = {181},
  number       = {1},
  pages        = {89--107},
  year         = {2010},
  url          = {https://doi.org/10.1007/s10479-010-0693-2},
  doi          = {10.1007/S10479-010-0693-2},
  timestamp    = {Thu, 13 Aug 2020 12:40:20 +0200},
  biburl       = {https://dblp.org/rec/journals/anor/Horbach10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

verification

@article{DBLP:journals/pieee/VizelWM15,
  author       = {Yakir Vizel and
                  Georg Weissenbacher and
                  Sharad Malik},
  title        = {Boolean Satisfiability Solvers and Their Applications in Model Checking},
  journal      = {Proc. {IEEE}},
  volume       = {103},
  number       = {11},
  pages        = {2021--2035},
  year         = {2015},
  url          = {https://doi.org/10.1109/JPROC.2015.2455034},
  doi          = {10.1109/JPROC.2015.2455034},
  timestamp    = {Sat, 30 Sep 2023 10:23:39 +0200},
  biburl       = {https://dblp.org/rec/journals/pieee/VizelWM15.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

hardware and software verification 

@inproceedings{DBLP:conf/date/Velev02,
  author       = {Miroslav N. Velev},
  title        = {Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue
                  Out-of-Order Microprocessors with a Reorder Buffer},
  booktitle    = {2002 Design, Automation and Test in Europe Conference and Exposition
                  {(DATE} 2002), 4-8 March 2002, Paris, France},
  pages        = {28--35},
  publisher    = {{IEEE} Computer Society},
  year         = {2002},
  url          = {https://doi.org/10.1109/DATE.2002.998246},
  doi          = {10.1109/DATE.2002.998246},
  timestamp    = {Fri, 24 Mar 2023 00:02:46 +0100},
  biburl       = {https://dblp.org/rec/conf/date/Velev02.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

Satisfiability checking (SAT) is one of the well known NP-hard problems [15]
in both theoretical and practical computer science. There are several real-world
applications that are actually tackled by modelling parts of these problems as
SAT instances like hardware and software verification [34], planning [23], and
bioinformatics [28].

hardware and software verification

@inproceedings{DBLP:conf/date/Velev02,
  author       = {Miroslav N. Velev},
  title        = {Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue
                  Out-of-Order Microprocessors with a Reorder Buffer},
  booktitle    = {2002 Design, Automation and Test in Europe Conference and Exposition
                  {(DATE} 2002), 4-8 March 2002, Paris, France},
  pages        = {28--35},
  publisher    = {{IEEE} Computer Society},
  year         = {2002},
  url          = {https://doi.org/10.1109/DATE.2002.998246},
  doi          = {10.1109/DATE.2002.998246},
  timestamp    = {Fri, 24 Mar 2023 00:02:46 +0100},
  biburl       = {https://dblp.org/rec/conf/date/Velev02.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

bioinformatics  生物信息学 

在dblp中搜索作者João P. Marques Silva  –  João Paulo Marques Silva得到很多模型检验、sat形式化及应用方面的文献

@inproceedings{DBLP:conf/sat/LynceM06,
  author       = {In{\^{e}}s Lynce and
                  Jo{\~{a}}o Marques{-}Silva},
  editor       = {Armin Biere and
                  Carla P. Gomes},
  title        = {{SAT} in Bioinformatics: Making the Case with Haplotype Inference},
  booktitle    = {Theory and Applications of Satisfiability Testing - {SAT} 2006, 9th
                  International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {4121},
  pages        = {136--141},
  publisher    = {Springer},
  year         = {2006},
  url          = {https://doi.org/10.1007/11814948\_16},
  doi          = {10.1007/11814948\_16},
  timestamp    = {Mon, 24 Feb 2020 19:23:28 +0100},
  biburl       = {https://dblp.org/rec/conf/sat/LynceM06.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

 circuit design

@article{DBLP:journals/tcad/StephanBS96,
  author       = {Paul R. Stephan and
                  Robert K. Brayton and
                  Alberto L. Sangiovanni{-}Vincentelli},
  title        = {Combinational test generation using satisfiability},
  journal      = {{IEEE} Trans. Comput. Aided Des. Integr. Circuits Syst.},
  volume       = {15},
  number       = {9},
  pages        = {1167--1176},
  year         = {1996},
  url          = {https://doi.org/10.1109/43.536723},
  doi          = {10.1109/43.536723},
  timestamp    = {Thu, 24 Sep 2020 11:26:56 +0200},
  biburl       = {https://dblp.org/rec/journals/tcad/StephanBS96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

neural network verification

@inproceedings{DBLP:conf/aaai/NarodytskaKRSW18,
  author       = {Nina Narodytska and
                  Shiva Prasad Kasiviswanathan and
                  Leonid Ryzhyk and
                  Mooly Sagiv and
                  Toby Walsh},
  editor       = {Sheila A. McIlraith and
                  Kilian Q. Weinberger},
  title        = {Verifying Properties of Binarized Deep Neural Networks},
  booktitle    = {Proceedings of the Thirty-Second {AAAI} Conference on Artificial Intelligence,
                  (AAAI-18), the 30th innovative Applications of Artificial Intelligence
                  (IAAI-18), and the 8th {AAAI} Symposium on Educational Advances in
                  Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February
                  2-7, 2018},
  pages        = {6615--6624},
  publisher    = {{AAAI} Press},
  year         = {2018},
  url          = {https://doi.org/10.1609/aaai.v32i1.12206},
  doi          = {10.1609/AAAI.V32I1.12206},
  timestamp    = {Mon, 04 Sep 2023 16:50:26 +0200},
  biburl       = {https://dblp.org/rec/conf/aaai/NarodytskaKRSW18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}