可滿足性（英語：Satisfiability）是用來解決給定的真值方程式，是否存在一组变量赋值，使問題为可满足。布尔可滿足性問題（Boolean satisfiability problem；SAT ）屬於決定性問題，也是第一个被证明屬於NP完全的问题。此問題在電腦科學上許多的領域皆相當重要，包括電腦科學基礎理論、演算法、人工智慧、硬體設計等等。
直观描述
- 对于一个确定的逻辑电路，是否存在一种输入使得输出为真。
参见
- NP-complete問題列表
- 幾乎完備（）問題與弱完備（）問題
- ASR-complete
- Ladner理論
- NP困难
- P/NP问题
外部連結
SAT Solvers:
*[http://www.princeton.edu/~chaff/ Chaff]
*[http://www.cs.ubc.ca/~babic/index_hypersat.htm HyperSAT]
*[http://www.cs.ubc.ca/~babic/index_spear.htm Spear]
*[http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/MiniSat.html The MiniSAT Solver]
*[https://web.archive.org/web/20070804183143/http://www.satlib.org/ubcsat/ UBCSAT]
Conferences/Publications:
*[http://sat07.ecs.soton.ac.uk/ SAT 2007: Tenth International Conference on Theory and Applications of Satisfiability Testing ]
*[https://web.archive.org/web/20060219180520/http://jsat.ewi.tudelft.nl/ Journal on Satisfiability, Boolean Modeling and Computation]
*[https://web.archive.org/web/20060210192113/http://www.ictp.trieste.it/~zecchina/SP/ Survey Propagation]
Benchmarks:
*[http://www.nlsde.buaa.edu.cn/~kexu/benchmarks/benchmarks.htm Forced Satisfiable SAT Benchmarks]
*[https://web.archive.org/web/20070717105815/http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/bmcbenchmarks.html IBM Formal Verification SAT Benchmarks]
*[http://www.satlib.org SATLIB]
*[http://www.cs.ubc.ca/~babic/index_benchmarks.htm Software Verification Benchmarks]
SAT solving in general:
*http://www.satlive.org
*http://www.satisfiability.org
*[http://www.sat4j.org/ Sat4j]
评论 (0)