SatisfiableQ

SatisfiableQ[bf]

如果存在变量组合，使得布尔函数 bf 产生 True，给出 True.

SatisfiableQ[expr,{a1,a2,…}]

如果存在 ai 值的组合，使得布尔表达式 expr 产生 True，给出 True.

更多信息和选项

  • 可使用下列 Method 设置：
  • "BDD"二分决策图 (BDD) 方法
    "SAT"SAT 求解器
    "TREE"分支和计算方法

范例

打开所有单元关闭所有单元

基本范例  (2)

测试布尔表达式是否满足：

测试纯函数是否满足：

选项  (1)

Method  (1)

默认情况下，SatisfiableQ 自动选择要使用的方法：

设置 Method"SAT"，输入转换为析取式的合取，并使用 SAT 求解器：

设置 Method"BDD"，则会计算输入的 BDD 表示：

设置 Method"TREE"，则会使用简单的分支和计算搜索方法：

属性和关系  (4)

如果对于某些变量分配是 true，满足表达式：

如果 SatisfiabilityCount 大于 0，满足 元变量的表达式：

用 SatisfiabilityInstances 得到明确的例子：

SatisfiableQ[f] 等价于 ¬TautologyQ[¬f]：

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 年

BibTeX

@misc{reference.wolfram_2024_satisfiableq, author="Wolfram Research", title="{SatisfiableQ}", year="2008", howpublished="\url{https://reference.wolfram.com/language/ref/SatisfiableQ.html}", note=[Accessed: 15-November-2024 ]}

BibLaTeX

@online{reference.wolfram_2024_satisfiableq, organization={Wolfram Research}, title={SatisfiableQ}, year={2008}, url={https://reference.wolfram.com/language/ref/SatisfiableQ.html}, note=[Accessed: 15-November-2024 ]}