ANTLR - 부울 satisfiabilty

Question

나는 생성 된 방문자를 사용하여 양식 (A & (B | C))의 표현식을 평가할 수있는 ANTLR 표현 파서를 가지고 있습니다. A, B 및 C는 2 개의 값 true 또는 false 중 하나를 취할 수 있습니다. 그러나 나는 표현이 사실 인 A, B 및 C의 모든 조합을 찾는 문제에 직면 해있다. 나는 다음과 같은 방법으로 이것을 풀려고했다.

1. 은 3 개 변수의 식을 복용 평가 진실하고 2^3 내가 000, 001, 010과 같은 값을주고 평가 8
2. 때문에이 8 개 조합에 관해서 각
3. 거짓 ..... .. 111을 변수에 적용하고 방문자를 사용하여 평가하십시오.

이 방법은 변수의 수가 증가함에 따라 집중적으로 계산됩니다. 그러므로 20 개의 변수가있는 표현식의 경우 1048576 번의 계산이 필요합니다. 이 모든 복잡성을 최적화하여 모든 실제 표현을 얻으려면 어떻게해야합니까? 나는 이것이 Boolean satisfiabilty problem

Answer 1

의 밑에 떨어질 것을 희망한다. 20-30 개의 변수가있는 경우 모든 조합을 무작위로 시도 할 수 있습니다. 1 회 시도 당 100ns가 걸리는 경우 (약 500 개의 기계 명령어) 약 100 초 후에 실행됩니다. 그것은 당신보다 빠릅니다.

보다 큰 방정식을 풀려면 실제 제약 조건 해결자를 만들어야합니다. 당신이 당신의 부울 식을 표현하는 방법을

나도 몰라 : 짐승 힘이 대답은 자바 프로그램의 속도를 평행 이동하려고 약으로 인해 영업 이익 발언에

는

편집 할 수 있습니다. brute force의 경우 수식 트리를 해석하거나 느린 다른 작업을 수행하고 싶지 않습니다.

가장 중요한 트릭은 부울 수식 을으로 평가하는 것입니다. 대부분의 프로그래밍 언어의 경우, 예를 들어, 손으로 그 언어의 기본 표현으로 테스트 할 수있는 공식을 코딩 N 중첩 루프를 싸서 전체를 컴파일 할 수 있어야한다

A=false; 
do { 
    B=false; 
    do { 
      C= false; 
      do { 
       if (A & (B | C)) { printf (" %b %b %b\n",A,B,C); 
       C=~C; 
      } until C==false; 
      B=~B; 
     } until B==false; 
    A=~A; 
    } until A==false; 

컴파일 (또는 JITted 자바에 의해), 나는 내부 루프가 부울 연산 당 1 ~ 2 개의 기계 명령어를 취하고, 레지스터 또는 하나의 캐시 라인을 만지며 루프에 2를 더하는 것이 기대된다. 약 42 개의 기계 명령어에 대해 첫 번째 단락의 대략적인 추정치보다 훨씬 낫습니다.

만일 가장 바깥 쪽 루프 (3 또는 4)를 병렬 스레드로 변환 할 수는 있지만 인쇄 명령문을 원한다면 유틸리티의 측면에서 실제로 중요하지는 않습니다.

이러한 수식이 많으면 수식에 대한 표현 (예 : ANTLR 구문 분석 트리)을 사용하여 코드 생성기를 쉽게 작성할 수 있습니다.