|
%SAT及其能解决的问题
|
|
|
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]
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}
}
|
|