SatisfiableQ

SatisfiableQ[bf]

ブール関数 bf がTrueを与える変数値の組合せが存在するときにTrueを返す．

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

ブール式 expr がTrueを与える aiの値の組合せが存在するときにTrueを返す．

詳細とオプション

  • 次は，使用可能なMethod設定である．
  • "BDD"二分決定図法
    "SAT"SATソルバ
    "TREE"分岐評価法

例題

すべて開くすべて閉じる

例  (2)

ブール式が充足可能かどうかテストする：

純ブール関数が充足可能かどうかテストする：

オプション  (1)

Method  (1)

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

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

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

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

特性と関係  (4)

式は，ある種の変数割当てが真となる場合に充足可能である：

変数の式は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 Language. 2008. "SatisfiableQ." Wolfram Language & System Documentation Center. Wolfram Research. https://reference.wolfram.com/language/ref/SatisfiableQ.html.

APA

Wolfram Language. (2008). SatisfiableQ. Wolfram Language & System Documentation Center. Retrieved from 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 ]}