布尔可满足性问题

可滿足性（英語：Satisfiability）是用來解決給定的真值方程式，是否存在一组变量赋值，使問題为可满足。布尔可滿足性問題（Boolean satisfiability problem；SAT ）屬於決定性問題，也是第一个被证明屬於NP完全的问题。此問題在電腦科學上許多的領域皆相當重要，包括電腦科學基礎理論、演算法、人工智慧、硬體設計等等。

直观描述

• 对于一个确定的逻辑电路，是否存在一种输入使得输出为真。

参见

• NP-complete問題列表
• 幾乎完備（Almost 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:

• http://www.satlive.org （页面存档备份，存于互联网档案馆）
• http://www.satisfiability.org （页面存档备份，存于互联网档案馆）
• Sat4j （页面存档备份，存于互联网档案馆）