布尔可满足性问题
![本页使用了标题或全文手工转换](http://images.weserv.nl/?url=//upload.wikimedia.org/wikipedia/commons/thumb/c/cd/Zh_conversion_icon_m.svg/35px-Zh_conversion_icon_m.svg.png)
(重定向自布爾可滿足性問題)
可滿足性(英語:Satisfiability)是用來解決給定的真值方程式,是否存在一组变量赋值,使問題为可满足。布尔可滿足性問題(Boolean satisfiability problem;SAT )屬於決定性問題,也是第一个被证明屬於NP完全的问题。此問題在電腦科學上許多的領域皆相當重要,包括電腦科學基礎理論、演算法、人工智慧、硬體設計等等。
直观描述
- 对于一个确定的逻辑电路,是否存在一种输入使得输出为真。
参见
外部連結
SAT Solvers:
- Chaff (页面存档备份,存于互联网档案馆)
- HyperSAT (页面存档备份,存于互联网档案馆)
- Spear (页面存档备份,存于互联网档案馆)
- The MiniSAT Solver (页面存档备份,存于互联网档案馆)
- UBCSAT
Conferences/Publications:
- SAT 2007: Tenth International Conference on Theory and Applications of Satisfiability Testing (页面存档备份,存于互联网档案馆)
- Journal on Satisfiability, Boolean Modeling and Computation
- Survey Propagation
Benchmarks:
- Forced Satisfiable SAT Benchmarks (页面存档备份,存于互联网档案馆)
- IBM Formal Verification SAT Benchmarks
- SATLIB (页面存档备份,存于互联网档案馆)
- Software Verification Benchmarks (页面存档备份,存于互联网档案馆)
SAT solving in general:
- http://www.satlive.org (页面存档备份,存于互联网档案馆)
- http://www.satisfiability.org (页面存档备份,存于互联网档案馆)
- Sat4j (页面存档备份,存于互联网档案馆)
|