prolog - 从 CNF 转换为喇叭形式

Question

如何使用 Prolog 将 CNF 子句转换为 Horn 形式？我正在尝试创建一个以 CNF 作为输入的 SAT Solver，需要将其转换为 Horn 形式。

Answer 1

Horn 子句是 CNF 的一个子集。即 CNF 可以看作是一般从句的结合，其中每个从句具有以下形式，其中 Ai,Bk 是命题变量，n>=0 和 m>=0：

A1 v .. v An v ~B1 v .. v ~Bm

Ai 是正面文字，~Bk 是负面文字。Horn 子句现在是那些最多有一个肯定字面量的一般子句，即 n=<1。即具有以下任一形式：

A1 v ~B1 v .. v ~Bm

~B1 v .. v ~Bm

现在不可能将每个 CNF 转换为 Horn 子句，即使我们允许在表示中更改文字的符号。取这个公式 nae(A,B,C)=(A xor B) v (B xor C) 和相关的符号变化变量作为 CNF：

nae(A,B,C)       = (~A v ~B v ~C) & (A v B v C)
nae(A,B,~C)      = (~A v ~B v C) & (A v B v ~C)
nae(A,~B,C)      = (~A v B v ~C) & (A v ~B v C)
nae(A,~B,~C)     = (~A v B v C) & (A v ~B v ~C)
nae(~A,B,C)      = (~A v B v C) & (A v ~B v ~C)
nae(~A,B,~C)     = (~A v B v ~C) & (A v ~B v C)
nae(~A,~B,C)     = (~A v ~B v C) & (A v B v ~C)
nae(~A,~B,~C)    = (~A v ~B v ~C) & (A v B v C)

它们都是非喇叭子句，因此无法重命名翻译。但也许使用其他约简，可能是非多项式的约简，可用于将 CNF 转换为 Horn 子句。

PS： nae(A,B,C) 示例取自此处。