Enable JavaScript to interact with content and submit forms on Wolfram websites. Learn how

SatisfiabilityInstances

SatisfiabilityInstances[bf]

尝试求出变量，使得布尔函数 bf 产生 True.

SatisfiabilityInstances[expr,{a₁,a₂,…}]

尝试求出一个 a_i，使得布尔表达式 expr 为 True.

SatisfiabilityInstances[…,…,m]

尝试求出 m 个使得产生 True 的变量.

更多信息和选项

如果没有找到产生 True 的变量，SatisfiabilityInstances[…] 给出 {}.
SatisfiabilityInstances[…,…,All] 给出变量产生 True 的所有选择.
可使用下列 Method 设置：
"BDD" 二分决策图 (BDD) 方法

"SAT" SAT 求解器

"TREE" 分支和计算方法

范例

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

基本范例 (3)

产生一个单个例子，其中布尔表达式为 true：

产生多个例子；在这里，仅存在两个例子：

求出一个布尔函数的 3 个例子：

当输入不被满足时，返回一个空表：

范围 (1)

找出所有布尔表达式为真的实例：

选项 (1)

Method (1)

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

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

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

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

属性和关系 (4)

n 元变量的布尔表达式最多有 2ⁿ 个例子：

用 SatisfiabilityCount 统计：

在 BooleanTable 中，SatisfiabilityInstances 对应于 True 项：

用 FindInstance 求出方程和不等式的解：

巧妙范例 (1)

一个实例采样：

整个列表很长：

顶部