양성 DNF의 압축

Question

긍정 명제식을 분리 기준 형식 (DNF)으로 압축하고 싶습니다.

나는 단지 리터럴이없는 단순한 DNF를 가정합니다. 역 과정, 감압은 쉽게 정의 할 수 있습니다. 단지 결합 및 분리에서 내장 공식의 경우, 다음 재 작성 규칙은 DNF를 생성합니다 : 이제 몇 가지 알고리즘이 있는지 궁금

Example: Decompression 
Input: 
    (p & (q v r) & s & (t v u)) v 
    w. 

Output: 
    (p & q & s & t) v 
    (p & r & s & t) v 
    (p & q & s & u) v 
    (p & r & s & u) v 
    w. 

: 여기

A & (B v C) --> (A & B) v (A & C) 
(A v B) & C --> (A & C) v (B & C) 

이 압축 해제의 예입니다 인데 DNF에서 단일 수식을 다시 생성 할 수 있습니다. 이진 결정 다이어그램을 이미 살펴 보았습니다. 내가 가지고있는 문제는 그들이 도중에도 의 결합을 결합 할 수 없다는 것입니다.

는 예를 들어 사용 공유, 여전히 비슷한 지점을 보여줄 것이다 이진 결정 다이어그램 인쇄 및/또는 새로운 전치사 변수를 도입 동안의 알고리즘은 두 가지 요구되지 않습니다

Example: Compression (Bad) 
Input: 
    (p & q & s & t) v 
    (p & r & s & t) v 
    (p & q & s & u) v 
    (p & r & s & u) v 
    w. 

Output: 
    (p & ((q & s & (t v u)) v (r & s & (t v u)))) v 
    w. 

- or - 

Output: 
    (p & ((q & h) v (r & h))) & (h <-> s & (t v u))) v 
    w. 

결과를해야한다 이 아닌 더 이상 DNF, 이진 결정 다이어그램 보다 더 작고 이항 및 연결 만 사용하는 알고리즘 및 전치사 변수는 이미 fo입니다. und 원래 DNF. 다음은 원하는 압축 예입니다.

Example: Compression (Good) 
Input: 
    (p & q & s & t) v 
    (p & r & s & t) v 
    (p & q & s & u) v 
    (p & r & s & u) v 
    w. 

Output: 
    (p & (q v r) & s & (t v u)) v 
    w. 

취할 수있는 조치는 무엇입니까? 프롤로그 구현이 선호됩니다.

안녕

Answer 1

나는 당신이 필요로하는 두 개의 층 (입력 변수의 접속사의 분리, 또는 입력 변수의 disjunctions의 결합 중 하나)에서 부울 식의 최소값을 계산하기위한 체계적인 알고리즘 생각 .

이 작업을 수행하는 데 사용되는 일반적인 알고리즘은 Karnaugh maps 및 Quine-McCluskey 알고리즘입니다.

이러한 알고리즘은 부정 변수로 작동합니다. 어떤 경우 든, 입력이 분리 정상 형태 (DNF)이고 부정 변수가 나타나지 않으면, 입력 변수의 결합의 분리로 표현 된 출력은 부정 변수를 갖지 않을 것입니다.