2016-10-11 18 views
1

私は70の変数で60の方程式を持っています。sympy解く線形方程式XOR、NOT

(X0、X1、...、x239)があるsympyシンボル

list_a = [Xor(Not(x40), Not(x86)), Xor(x41, Not(x87)), ...] 

は、私の質問は、それが可能であれば何とかこの方程式は行列に変換または、次のとおりです。 それらのすべてが1つのリストにありますそれらを解決しました。 私はそれが複数の解決策を持つことができると思います。

+0

ブール空間上の線形方程式のシステムのように見えるのは、実数上の線形方程式のシステムとまったく同じです。あなたの質問で明確にしてください、あなたはアルゴリズムを探していますか、すでに持っているアルゴリズムを実装する方法、あるいはその両方ですか? – Vovanrock2002

+0

SATのような音がします。 –

+0

私はboth.Algorithmを探していて、リストから行列への変換もしています。 –

答えて

1

論理式のシステムに対する解決策は、SATで式の論理積(And)をチェックすることと同じです。

In [3]: list_a = [Xor(Not(x40), Not(x86)), Xor(x41, Not(x87))] 

In [4]: list_a 
Out[4]: [¬x₄₀ ⊻ ¬x₈₆, x₄₁ ⊻ ¬x₈₇] 

In [5]: satisfiable(And(*list_a)) 
Out[5]: {x87: False, x40: True, x86: False, x41: False} 

あなたはすべてのソリューションをしたい場合は、一般的なケースでは指数関数的に多くのソリューションがあることに注意してくださいが、all_models=Trueを渡すことができます。

+0

ありがとうございます。しかし、120の変数を持つ60の方程式があれば、時間がかかります。それを速くする可能性はありますか? –

+0

どの部分が遅いかによって異なります。一般的には、cnfへの変換やSATの解決が遅いです。システムの 'to_cnf(And(* list_a))'を別々に実行することで確認できます。 – asmeurer

関連する問題