무차별 대입을 사용하여 2Sat CNF 형태를 푸십시오.

Question

현재 시험에 대한 2SAT 문제를 연구하고 있으며, 무차별 대입을 사용하여 솔루션이 있는지 확인하는 방법을 실제로 이해하지 못합니다. 이게 이상하게 보일지 모르지만 암시 그래프를 조금 더 구현하는 방법을 이해하지만 무차별 전략을 구현하는 방법을 너무 확신하지 못합니다.

누군가 통찰력을 공유 할 수 있습니까? 어쩌면 의사 코드 또는 java에있을 수 있습니다.

감사

Answer 1

수식의 변수는 정수 값의 비트로 인코딩 할 수 있습니다. 그런 다음 무차별 대입 방법은 통합 "컨테이너"가 취할 수있는 모든 가능한 값에 대한 범위로 내려갑니다.

즉, 모든 수식의 변수를 나타내는 정수 배열이 있고 정수로 증가하고 각 단계에서 수식에 대해 나타내는 솔루션을 확인합니다. 솔루션이 일치하면 멈 춥니 다.

는 다음과 같은 변수 컨테이너 죽은 간단한 구현의 :

class OverflowException extends RuntimeException {} 

public class Variables { 
    int[] data; 
    int size; 

    public Variables(int size_){ 
     size = size_; 
     data = new int[1 + size/32]; 
    } 
    public boolean get(int i){ 
     return (data[i/32] & (1 << i%32)) != 0; 
    } 
    public void set(int i, boolean v){ 
     if (v) 
      data[i/32] |= (1 << i%32); 
     else 
      data[i/32] &= ~(1 << i%32); 
    } 
    public void increment(){ 
     int i; 
     for (i=0; i < size/32; i++){ 
      data[i]++; 
      if (data[i] != 0) return; 
     } 
     if (size%32 != 0){ 
      data[i]++; 
      if ((data[i] & ~((1 << (size%32)) - 1)) != 0) 
       throw new OverflowException(); 
     } 
    } 
} 

(매주의 위험의 위험 부담 : 코드 검증되지 않은).

변수 배열은 더 간단 boolean 컨테이너로 표현 될 수 있지만,이 아마도 대신에 일반 이진 인코딩의 gray code을 사용하여 완화 할 수 있지만 당신은 (때문에 증분 단계의 성능에 약간의 손실 될 수 있습니다 증분 작업이지만이 implementation의 복잡성은 그 반대를 나타내는 것으로 보이며 복잡한 솔루션을 찾으면 좋은 sat2 솔버가 될 수 있습니다.

Answer 2

이것은 우리가 무력 솔루션 : 사용하지 않는 이유는, 그들은 많은 자원을 소모합니다. 내 알고리즘은 모든 가능성을 가진 매트릭스를 생성하지 않을 것입니다. 하지만 하나의 과제를 만든 다음 즉시 과제를 테스트하십시오. 그런 다음 다음 것을 만드십시오. 첫 번째 해결책을 찾았 으면 중단 할 수 있습니다.