如何將布爾表達式轉換爲cnf文件？

我需要使用解算器坐了檢查布爾表達式的可滿足..如何將布爾表達式轉換爲cnf文件？

我有複雜的布爾表達式這樣

alt text

有任何自動CNF文件轉換器，這樣我可以直接給它坐解決者？

我讀取cnf格式文件..但如何在.cnf文件中表達這個表達式？當palenthesis中存在連詞時，我會感到困惑，並且如何表達 - >和< - >？請幫我

來源

2010-10-16 karthi

有幾個解決方案。

Limboole是一個開放源代碼的工具，我相信它包括一個單獨的'CNF'轉換器的命題邏輯。

更一般地說，你也可以使用一種本機支持命題邏輯的工具;一些示例包括Z3,CVC3和Yices。

來源

2011-01-17 19:58:14 phooji

您所命名的SMT解算器真的可以解決SAT解決問題的難題.... – EfForEffort 2012-11-06 03:06:52

@DenisBueno：我很同意（SMT求解器比SAT解決方案做得更多）。在這種情況下，我並沒有真正看到成本 - 現代基於DPLL（T）的SMT解算器具有與最好的僅SAT解算器相媲美的SAT性能，而且使用起來也不那麼困難。如果你願意使用SMT-lib語法，你可以編寫相當高層次的命題，並且仍然可以互換使用解算器。我會補充一點，Z3，cvc3和yices正在積極維護並且有相當活躍的郵件列表來支持用戶。 – phooji 2012-11-06 04:13:02

SBSAT是一種基於狀態的SAT求解器，能夠接受各種輸入格式。你可以採取一個簡單的表達式，並將其提供給SBSAT以轉換爲CNF。 manual，第4.10節描述瞭如何做到這一點。

來源

2012-11-06 03:09:29 EfForEffort

我無法在'SBSAT'中找到這樣的功能。可以將「跟蹤格式」指定爲輸入格式。但是，這不允許嵌套的布爾表達式，但只允許門語句的網表。 – 2014-01-16 13:17:15

如何將布爾表達式轉換爲cnf文件？

回答

相關問題