나는 70 개의 변수가있는 60 개의 방정식을가집니다.sympy 선형 방정식 XOR, NOT
(X0, X1, ..., x239)이 있습니다 sympy 문자
list_a = [Xor(Not(x40), Not(x86)), Xor(x41, Not(x87)), ...]
는 내 질문은 가능하면 어떻게 든이 방정식은 행렬을 변환 또는이다 : 그들 모두는 하나 개의 목록에 그들을 풀었다. 나는 하나 이상의 솔루션을 가질 수 있다고 생각한다.
논리 표현식 시스템에 대한 해결책은 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 통과 할 수있는 모든 솔루션을 원하는 경우
솔루션 주셔서 감사합니다,하지만 만약 내가 120 변수와 60 방정식을 가지고 오랜 시간이 걸립니다. 그것을 더 빨리 만들 가능성이 있습니까? –
어떤 부분이 느린 지에 따라 다릅니다. 일반적으로 cnf 로의 전환이나 SAT 해결 속도가 느립니다. 시스템에 대해'to_cnf (And (* list_a))'를 별도로 실행하여 확인할 수 있습니다. – asmeurer
부울 공간에서 선형 방정식 시스템은 실제 숫자에 대한 선형 방정식 시스템과 똑같은 것처럼 보입니다. 귀하의 질문에 명확히 설명해 주시겠습니까, 당신은 알고리즘을 찾고 있습니까, 아니면 이미 가지고있는 알고리즘을 구현하는 방법, 또는 둘 다? – Vovanrock2002
SAT 문제와 비슷합니다. –
둘 다 찾고 있습니다. 알고리즘 및 또한 목록에서 매트릭스로 변환. –