布尔可满足性问题
维基百科，自由的百科全书
可滿足性（英語：Satisfiability）是用來解決給定的布林方程式，是否存在一组变量赋值，使問題为可满足。布林可滿足性問題（Boolean satisfiability problem；SAT)）屬於決定性問題，是第一个被证明NP完全问题。為電腦科學上許多領域的重要問題，包括電腦科學基礎理論、演算法、人工智慧、硬體設計等等。
直观描述 [编辑]
- 对于一个确定的逻辑电路，是否存在一种输入使得输出为true，是第一个被证明的NPC问题。
外部連結 [编辑]
SAT Solvers:
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:
|
|||||||||||||||||||
