SatisfiabilityInstances

SatisfiabilityInstances[bf]

ブール関数 bf がTrueを返す変数を見付けようとする．

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

ブール式 expr がTrueを返すような aiを見付けようとする．

SatisfiabilityInstances[…,…,m]

Trueを返す変数を m 通り見付けようとする．

詳細とオプション

  • 変数をどのように選んでもTrueが返されない場合，SatisfiabilityInstances[…]は{}を返す．
  • SatisfiabilityInstances[…,…,All]は，Trueを与える変数の全選択肢を与える．
  • 次は，使用可能なMethod設定である．
  • "BDD"二分決定図法
    "SAT"SATソルバ
    "TREE"分岐評価法

例題

すべて開くすべて閉じる

例  (3)

ブール式が真となる例を1つ生成する：

複数の例を生成する．この場合は2通りしか存在しない：

純ブール関数の例を3つ求める：

入力が充足可能ではない場合，空のリストが返される：

スコープ  (1)

ブール式が真となる場合をすべて求める：

オプション  (1)

Method  (1)

デフォルトで，SatisfiabilityInstancesは使用するメソッドを自動的に選ぶ：

Method"SAT"とすると，入力は論理和の論理積に変換されてSATソルバが使われる：

Method"BDD"とすると，入力のBDD表現が計算される：

Method"TREE"とすると，単純な分岐評価検索法が使われる：

特性と関係  (4)

n 変数のブール式には最高で2nの真となる場合があり得る：

SatisfiabilityCountを使って真となる場合の厳密な数を得る：

SatisfiabilityInstancesはBooleanTableのTrue項目に対応する：

FindInstanceを使って方程式と不等式の解を求める：

おもしろい例題  (1)

さまざまな例：

完全なリストはより長くなる：

Wolfram Research (2008), SatisfiabilityInstances, Wolfram言語関数， https://reference.wolfram.com/language/ref/SatisfiabilityInstances.html.

テキスト

Wolfram Research (2008), SatisfiabilityInstances, Wolfram言語関数， https://reference.wolfram.com/language/ref/SatisfiabilityInstances.html.

CMS

Wolfram Language. 2008. "SatisfiabilityInstances." Wolfram Language & System Documentation Center. Wolfram Research. https://reference.wolfram.com/language/ref/SatisfiabilityInstances.html.

APA

Wolfram Language. (2008). SatisfiabilityInstances. Wolfram Language & System Documentation Center. Retrieved from https://reference.wolfram.com/language/ref/SatisfiabilityInstances.html

BibTeX

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

BibLaTeX

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