다중 가정으로 해결

Question

변수가 (a,b,c,d,e,f,g) 인 CNF 표현식이 있다고 가정합니다. SAT 해결사를 사용하여 (d,e,f)에 대한 할당을 찾으려면 어떻게해야합니까? {a,b,c,g} = {1,0,0,1}과 {a,b,c,g} = {1,1,1,1}이 주어 졌습니까? 하나의 가정이라면, {d,e,f}에 대한 과제를 찾기 위해 일일 해결사를 호출하는 것은 간단합니다 (예 : CNF에 단원 절 추가). 하지만 여러 가지 가정이 있다면 어떨까요? 이것이 가능한가?

Answer 1

여기 harold가 당신에게 설명하려고했던 것이 무엇인지에 대한 단계가 있습니다. 변수 a, b, c, d, e, f 및 g 위에 CNF 수식 F가 있습니다.

1. 는 G에서 중복 G.
2. 호출 수식 중복 CC와 C를 BB와 B, AA와 변수 A를 대체하고, GG와 g.
3. (a, b, c, g) = (1,0,0,1)이되도록 F에 단위 절을 추가하십시오.
4. (aa, bb, cc, gg) = (1,1,1,1)이되도록 G에 단위 절을 추가하십시오.
5. 수식 F와 G를 연결하고 그 결과를 SAT 해결사에 제공합니다.

솔버는 (a, b, c, g)와 (aa, bb, cc, gg)의 사전 설정 값과 일치하는 만족스러운 할당을 찾습니다.

Answer 2

실용적인 답을 원하거나 흥미로운 이론적 대답을 원한다면 명확하지 않습니다. 나는 실용적으로 갈 것이다.

가정의 각 집합에 대해 해당 가정 집합 (example)에 대한 가정으로 풀이를 지원하는 만족 된 솔버를 호출하십시오. 동일한 솔버 인스턴스에서 순차적으로 수행하십시오.

장점 :

• 당신은 가정의 상호 배타적 인 세트의 satisfiability를 함께 사용하지 마십시오. 가정의 세트 A가 수식 F에 대해 설정되고 다른 세트 A '가 F에 대해 unsat 인 경우, 각각의 호출은 이러한 가정이 만족스럽지 않은지 여부를 알려줍니다.
• 두 번째 호출에 대해 첫 번째 호출의 학습 된 절이 계속있을 수 있습니다. 중간 학습 된 절은 동일한 변수에 대해 말합니다. (참고 : 분리형 수식이 F & G 인 경우 F는 변수 X 이상이고 G는 변수 Y 및 X이며 Y는 변수를 공유하지 않습니다. resolution - CDCL에서 사용되는 추론 규칙 - F와 G를 섞는 절을 파생시킬 수 없습니다. 함께 두 가지를 혼합 대신에 하나 개의 인스턴스가 초기 unsat 증명 정지 훨씬 쉽게하지 않는 한 그들을 떨어져 분할의 명백한 이득이 없음)

단점 :.

• 인스턴스 A가에서 해결하기 어려운 경우 연습하지만 A '는 사소한 것입니다. A.에 붙어있을 수 있습니다.
• 두 개 이상의 인스턴스가있는 경우 병행하지 않습니다. 당신은 가능한 한 추가 메커니즘이 필요하다는 것을 즉시 풀고 싶습니다.

나는 이것이 명백한 대답이라는 것을 알고 있지만 시도해 볼 가치가있다. 이것이 실패하면 w.r.t를 해결하는 것과 같은 멋진 일을 시도 할 수 있습니다. 가정은 A union A'이고, A의이 전략에 뒤 떨어지면 해결되지 않는 경우에만 'A'가됩니다. 예를 들어 (a,b,c,g) = (1,0,0,1)과 (a,b,c,g) = (1,1,1,1)은 상호 배타적이므로 도움이되지 않습니다.