布尔可满足性问题

可满足性(英语:Satisfiability)是用来解决给定的真值方程式,是否存在一组变量赋值,使问题为可满足。布尔可满足性问题(Boolean satisfiability problemSAT )属于决定性问题,也是第一个被证明属于NP完全的问题。此问题在计算机科学上许多的领域皆相当重要,包括计算机科学基础理论算法人工智能硬件设计等等。

直观描述

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

参见

外部链接

SAT Solvers:

Conferences/Publications:

Benchmarks:

SAT solving in general: