Ich habe 60 Gleichungen mit 70 Variablen. alle von ihnen sind in einer Liste:sympy lösen lineare Gleichungen XOR, nicht
(x0, x1, ..., x239) sind sympy Symbole
list_a = [Xor(Not(x40), Not(x86)), Xor(x41, Not(x87)), ...]
und meine Frage ist, ob es möglich ist, irgendwie zu verwandeln diese Gleichungen Matrix oder löste sie. Ich denke, dass es mehr als eine Lösung haben kann.
Eine Lösung für ein System von logischen Ausdrücken ist die gleiche wie die Überprüfung von SAT für die Konjunktion (And) der Ausdrücke.
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}
Wenn Sie alle Lösungen wollen Sie all_models=True, obwohl beachten Sie passieren kann, dass es im allgemeinen Fall sind exponentiell viele Lösungen.
Danke für die Lösung, aber wenn ich 60 Gleichungen mit 120 Variablen habe, dauert es lange. Gibt es die Möglichkeit, es schneller zu machen? –
Es hängt davon ab, welcher Teil langsam ist. Im Allgemeinen ist die Umwandlung in cnf oder die SAT-Lösung entweder langsam. Sie können dies überprüfen, indem Sie 'to_cnf (And (* list_a))' für Ihr System separat ausführen. – asmeurer
Sieht aus wie Systeme linearer Gleichungen auf booleschem Raum genau wie Systeme linearer Gleichungen auf reellen Zahlen gelöst werden. Könnten Sie bitte in Ihrer Frage klären, suchen Sie nach einem Algorithmus oder wie implementieren Sie einen Algorithmus, den Sie bereits haben, oder beides? – Vovanrock2002
Klingt wie ein SAT-Problem. –
Ich suche sowohl.Algorithmus als auch für die Transformation von Liste zu Matrix. –