布林可滿足性問題
外觀
![本頁使用了標題或全文手工轉換](http://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 (頁面存檔備份,存於網際網路檔案館)
|