布尔可 满足性: 理 论与工程 By Moshe Y. Vardi Communications of the ACM, March 2014, Vol. 57 No. 3, Page 5 一, 译文 布尔可 满足性问题( Boolean Satisfiability Problem , 简称 SAT ) 问的是,一个给定的布尔公式在 AND 和 NOT 等布尔门的作用下,其 输入变量的 ...
SAT 问题是 “ 布尔逻辑可满足性问题( boolean SATisfiability problem ) ” 的简称,指给定一个合取范式公式 f ,判断其是否可满足,即找出布尔变量真值赋值,使得公式 f 为真。 一, SAT 问题 1 ,基本概念 布尔变量( Boolean variables ):取值为真值 {0 , 1} 的变量, x 1 , x 2 , …… x n , ...
众所周知, SAT (可满足性)问题是由斯蒂芬 - 库克( Stephen Cook )在其 1971 年发表的题为 The Complexity of Theorem-Proving Procedures» 的论文中提出的, SAT 问题涉及判定合取范式公式的可满足性,合取范式公式由变量、逻辑运算符和子句组成。这些公式使用布尔代数的原理来表达。 ...