布尔可满足性问题
维基百科,自由的 encyclopedia
可满足性(英语:Satisfiability)是用来解决给定的真值方程式,是否存在一组变量赋值,使问题为可满足。布尔可满足性问题(Boolean satisfiability problem;SAT )属于决定性问题,也是第一个被证明属于NP完全的问题。此问题在电脑科学上许多的领域皆相当重要,包括电脑科学基础理论、算法、人工智慧、硬件设计等等。
直观描述
- 对于一个确定的逻辑电路,是否存在一种输入使得输出为真。
参见
- NP-complete问题列表
- 几乎完备(Almost complete(英语:Almost complete))问题与弱完备(weakly complete(英语:weakly complete))问题
- ASR-complete
- Ladner理论
- NP困难
- P/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: