5

次のような一連の記号ブール式を解く必要があります。

>>> solve(x | y = False)
(False, False)

>>> solve(x & y = True)
(True, True)

>>> solve (x & y & z = True)
(True, True, True)

>>> solve(x ^ y = False)
((False, False), (True, True))

そのような変数の数が多い (~200) ため、ブルート フォース戦略は不可能です。Web を検索したところ、SympyとSageには記号操作機能があることがわかりました (特にthisとthisが役立つ可能性があります)。どうやってやるの？

編集:私は主にそのようなものを操作しようとしました:

>>> from sympy import *

>>> x=Symbol('x', bool=True)

>>> y=Symbol('y', bool=True)

>>> solve(x & y, x)

になりますNotImplementedError。次に、 solve(x * y, x)どちらが与えられたかを試してみました[0]（それが何を意味するのかわかりません）、solve(x * y = True, x)結果はSyntaxErrorにsolve(x * y, True, x)なりsolve(x & y, True, x)、AttributeError. 他に何を試せばいいのかわからない！

EDIT（2）：私もこれを見つけました、役に立つかもしれません！

4

2 に答える 2

4

まず、質問で露骨に間違っているいくつかのことを修正します。

  • solve代数式を解きます。solve(expr, x)について式 expr = 0 を解きxます。

  • solve(x | y = False)などは無効な構文です。=Python では、平等を意味するために使用することはできません。http://docs.sympy.org/latest/tutorial/gotchas.html#equals-signsを参照してください(このチュートリアルの残りも読むことをお勧めします)。

  • 別の質問への回答で述べたように、Symbol('y', bool=True)何もしません。に仮定をSymbol('x', something=True)設定しますが、SymPy のどの部分からも認識されている仮定ではありません。ブール式には正規を使用してください。is_somethingxboolSymbol('x')

一部のコメンターが指摘したように、必要なのはsatisfiableSAT ソルバーを実装する です。satisfiable(expr)が充足可能かどうかexpr、つまり、それを真にする変数の値があるかどうかを示しexprます。満足できる場合は、そのような値のマッピング (「モデル」と呼ばれます) を返します。そのようなマッピングが存在しない場合、つまりexpr矛盾している場合は、 を返しますFalse。

したがって、satisfiable(expr)は を解くのと同じですexpr = True。を解きたい場合は、 ( SymPy では not を意味します)expr = Falseを使用する必要があります。satisfiable(~expr)~

In [5]: satisfiable(x & y)
Out[5]: {x: True, y: True}

In [6]: satisfiable(~(x | y))
Out[6]: {x: False, y: False}

In [7]: satisfiable(x & y & z)
Out[7]: {x: True, y: True, z: True}

最後に、1 つの解しか返さないことに注意してくださいsatisfiable。これは、一般に必要なのはこれだけです。一般に、すべての解を見つけることは非常にコストがかかります。式の変数の数です2**n。n

ただし、それらすべてを見つけたい場合、通常のトリックは、元の式に を追加することです。~EここEで、 は前の解の結合です。たとえば、

In [8]: satisfiable(x ^ y)
Out[8]: {x: True, y: False}

In [9]: satisfiable((x ^ y) & ~(x & ~y))
Out[9]: {x: False, y: True}

これは、が真で偽& ~(x & ~y)である解が必要ないことを意味します(解に条件を追加すると考えてください)。このように繰り返すことで、すべてのソリューションを生成できます。xy&

于 2013-11-05T01:29:49.020 に答える