從CNF轉換爲喇叭形式

如何使用Prolog將CNF子句轉換爲喇叭形式？我正在嘗試創建一個將CNF作爲輸入的SAT求解器，這將需要轉換爲喇叭形式。從CNF轉換爲喇叭形式

2017-08-26 piyo_kuro

如果您定義了什麼Horn窗體以及它與您使用的CNF格式有什麼不同，可能會有所幫助，因爲CNF可用於編碼Horn公式。 –

這沒有多大意義。非常非正式：解決CNF是NP難題，解決HornSat在P中。這意味着（通過矛盾使用基本論點）：複雜性方面，這種轉換與解決原始CNF-SAT（NP-hard）和輸出可能是指數大小的（對於你的HornSAT解算器你可以做的不多）！ – sascha

Kyle Jones，CNF如何被用來編碼喇叭公式？ –

Horn子句是CNF的一個子集。即CNF可被視爲一般條款的結合，其中每子句具有以下形式和其中，Ai，BK是命題變量且n> = 0且m> = 0：

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

的艾是正文字而〜Bk是否定文字。 Horn子句現在其具有n個這些通則在最大一個正文字，即= < 1。即它們的任一形式的如下：

A1 v ~B1 v .. v ~Bm 

~B1 v .. v ~Bm

現在它不可能每CNF轉換成Horn子句，即使我們允許更改表示中文字的符號。藉此式亞科（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子句。（A，B，C）示例取自here。

來源

2018-02-26 23:06:50

從CNF轉換爲喇叭形式

回答

相關問題