BDD를 CNF로 변환

Question

JavaBDD을 사용하여 BDD 표현을 사용했는데 다른 도구와 함께 사용할 수 있도록 연결 표준 형식으로 변환해야합니다. 전환을 구현하는 가장 좋은 방법은 무엇이 될지 궁금합니다. DNF를 추출하는 것은 충분히 간단합니다 (단지 "1"로 모든 경로를 추출하십시오). 그러나 나는 CNF를 보러 갈 수있는 가장 좋은 방법이 무엇인지 확신하지 못합니다. 어떤 아이디어라도 대단히 감사하겠습니다.

Answer 1

모든 경로를 0으로 추출하십시오. 각 경로는 절으로 변환되어야합니다.

¬A, B, C를 0 경로 중 하나라고합시다. 상대 절은 (A ∨ B ∨ C)입니다.

일단 모든 절이 있으면 간단히 ∧를 붙이십시오!

알고리듬은 calculate a CNF from a truth table과 동일합니다.

Answer 2

등가의 CNF는 BDD의 크기가 지수적일 수있다. 애플리케이션에 따라 보조 변수를 추가하는 것이 좋습니다. Tseitin 변환을 사용하여. BDD가 만족스러운 경우에만 결과 CNF가 만족 될 수 있지만 추가 변수로 인해 논리적으로 동등하지는 않습니다.