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: 22-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: 22-November-2024 ]}