计算机科学

首页 > 计算机科学

布尔可满足性问题

2018-08-30 10:06:25     所属分类:计算机逻辑

可满足性(英语:Satisfiability)是用来解决给定的真值方程式,是否存在一组变量赋值,使问题为可满足。布尔可满足性问题(Boolean satisfiability problemSAT))属于决定性问题,也是第一个被证明属于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

相关推荐