爲緩存原因規範化布爾表達式。有沒有比真值表更有效的方法？

Question

我目前的項目是一個帶布爾檢索功能的高級標籤數據庫。記錄被查詢與（在音樂數據庫例如）布爾表達式像這樣：

funky-music and not (live or cover) 

應該得到所有時髦的音樂在音樂數據庫，但不居住或歌曲的翻唱版本。

當涉及到緩存時，問題是存在相同但查詢結構不同的查詢。例如，將德，摩根的規則，上面的查詢可以這樣寫：

funky-music and not live and not cover 

緩存將通過散列查詢字符串，例如執行時會產生完全相同的記錄，但事業突破的緩存。

因此，我的第一個意圖是創建一個查詢的真值表，然後可以用作緩存鍵作爲等價表達式形成相同的真值表。不幸的是，這是不可行的，因爲真值表隨着輸入數量（標籤）呈指數增長，我不想限制一個查詢中使用的標籤數量。

另一種方法是遍歷應用由布爾代數定義的規則的語法樹，以形成（最小）規範化表示，這似乎也很棘手。

因此，總體問題是：是否有一種可行的方法來實現等效查詢的識別，而不需要circuit minimization或真值表（編輯：或任何其他算法是NP-hard）？

ne plus ultra會識別已經緩存的子查詢，但這不是主要目標。

Answer 1

確定查詢是否等價於「False」的通用高效算法可用於有效解決NP完全問題，因此您不可能找到一個。

您可以嘗試將您的查詢轉換爲規範形式。由於上述原因，總會有一些查詢花費很大的代價來轉換成任何給定的形式，但是您可能會發現，在實踐中，某種形式在大多數情況下運行得相當好 - 而且您總是可以放棄一半如果變得太難了，就要轉型。

你可以看看http://en.wikipedia.org/wiki/Conjunctive_normal_form,http://en.wikipedia.org/wiki/Disjunctive_normal_form,http://en.wikipedia.org/wiki/Binary_decision_diagram。

Answer 2

您可以將查詢轉換爲連接標準形式（CNF）。它是布爾公式的典型簡單表示，通常是SAT求解器的基礎。

最有可能的「大」查詢會有很多連詞（而不是很多的disjunctions），所以CNF應該很好地工作。

Answer 3

Quine-McCluskey算法應該能夠實現你正在尋找的東西。與卡諾的地圖類似，但更容易到implement in software。