布林可滿足性問題

可滿足性（英語：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 （頁面存檔備份，存於網際網路檔案館）