MiniSat의 비 결정 변수의 의미는 무엇입니까?

Question

C++ 라이브러리로 MiniSat을 사용할 때, 모든 새로운 변수는 결정 변수 또는 비 결정 변수로 생성 될 수 있습니다.

솔직히 분기 할 때 어떤 변수를 사용할 지 결정할 때 비 결정 변수는 고려되지 않습니다. 그러나 솔라가 SAT를 반환 할 때 공식이 실제로 UNSAT 임에도 불구하고 내 프로젝트에서 솔리드가 동등한 관계에있는 대신 결정되지 않은 변수가 왼쪽에있을 때 문제가 발생했습니다.

비 결정 변수가 2 변수보다 긴 수식에있는 경우에만 발생합니다 (2 변수 수식 경로는 해석자의 특수 사례이므로 다른 방식으로 동작 함). .

Answer 1

비 결정 변수는 추론을 통해서만 값을 설정할 수 있습니다. Minisat이 사용하는 유일한 추론 방법은 단위 규칙입니다. 따라서 모든 결정 변수를 설정해도 단위 규칙이 호출되어 모든 비 결정 변수를 설정하지 않으면 후자의 변수는 절대로 설정되지 않습니다.

비 결정 변수를 갖는 일반적인 이유는 CNF 인스턴스가 고정 된 결정 변수 세트를 설정하면 다른 모든 변수에 대한 값을 내포하는 구조임을 알 수 있기 때문입니다.

예를 들어, n 비트 정수의 소수 요소를 찾는 CNF 인스턴스입니다. 인스턴스는 반드시 승산을 구현하는 시프트 - 가산기 체인을 구현해야하지만 승산 회로에 대한 입력 인 2 (n-1) 비트 만 설정하면됩니다. 이러한 비트를 나타내는 변수는 결정 변수가되며 모든 다른 변수는 비 결정 변수로 안전하게 선언 될 수 있습니다.