SatisfiableQ
SatisfiableQ
SatisfiableQ[bf]
SatisfiableQ[expr,{a1,a2,…}]
更多信息和选项
- 可使用下列 Method 设置：
-
"BDD" 二分决策图 (BDD) 方法 "SAT" SAT 求解器 "TREE" 分支和计算方法
范例
打开所有单元 关闭所有单元基本范例 (2)
选项 (1)
Method (1)
默认情况下，SatisfiableQ 自动选择要使用的方法：
SeedRandom[1234];
vars = x /@ Range[25];
form = And@@Or@@@RandomChoice[Join[vars, Not /@ vars], {200, 5}];SatisfiableQ[form, vars]//AbsoluteTiming设置 Method"SAT"，输入转换为析取式的合取，并使用 SAT 求解器：
SatisfiableQ[form, vars, Method -> "SAT"]//AbsoluteTiming设置 Method"BDD"，则会计算输入的 BDD 表示：
SatisfiableQ[form, vars, Method -> "BDD"]//AbsoluteTiming设置 Method"TREE"，则会使用简单的分支和计算搜索方法：
SatisfiableQ[form, vars, Method -> "TREE"]//AbsoluteTiming属性和关系 (4)
BooleanTable[Xor[a, b], {a, b}]SatisfiableQ[Xor[a, b], {a, b}]如果 SatisfiabilityCount 大于 0，满足 
元变量的表达式：
SatisfiabilityCount[¬Implies[Implies[a, b]∧¬b, ¬a]]SatisfiableQ[¬Implies[Implies[a, b]∧¬b, ¬a]]用 SatisfiabilityInstances 得到明确的例子：
SatisfiabilityInstances[Xor[a, b], {a, b}]SatisfiableQ[f] 等价于 ¬TautologyQ[¬f]：
¬TautologyQ[¬Xor[a, b], {a, b}]SatisfiableQ[Xor[a, b], {a, b}]
Wolfram Research (2008)，SatisfiableQ，Wolfram 语言函数，https://reference.wolfram.com/language/ref/SatisfiableQ.html.
文本
Wolfram Research (2008)，SatisfiableQ，Wolfram 语言函数，https://reference.wolfram.com/language/ref/SatisfiableQ.html.
CMS
Wolfram 语言. 2008. "SatisfiableQ." Wolfram 语言与系统参考资料中心. Wolfram Research. https://reference.wolfram.com/language/ref/SatisfiableQ.html.
APA
Wolfram 语言. (2008). SatisfiableQ. Wolfram 语言与系统参考资料中心. 追溯自 https://reference.wolfram.com/language/ref/SatisfiableQ.html 年