satisfiability

5熱度

1回答

SAT是NP完全的證明是一種建設性證明，所以應該可以將其作爲程序來實現。有沒有人做過這個？我正在尋找一個程序（一個編譯器），它將一個程序（它返回true或false）作爲輸入並輸出一個SAT公式。例如，編譯器可以將以下程序（以pythonic語法顯示，但任何語言都適合我）作爲輸入，並輸出SAT公式。將SAT公式提供給SAT求解器將給出參數「證書」的解決方案。在這種情況下，解決方案會是[假，真，真

1熱度

1回答

命題邏輯

我有以下問題：我有兩個命題公式必須在邏輯上等價。只有其中一個包含一個'變量'，因爲變量可以被任何命題公式所取代。現在的問題是，我需要找到變量的實際替代，以使邏輯等價變爲真。例如：（一個^〜b）或X = A 在此，x表示該變量。這個邏輯等價可由真實的，通過用^ B更換的x，所以它成爲：（一個^〜B）或（a^B）=一個因此，這就是問題所在。我需要一種算法，得到作爲輸入的「與一個變量x方程」，並

1熱度

1回答

獨立EXISTS子句的動作如何工作？

如果我有這樣一個公式： FAx FAy (Ez(!A(x,z) v !A(y,z)) v B(x,y)) （FA =對於全部/ E =存在） skolemisation的規則說：如果E是FA以外替換常數或如果E在FA內部，則由新函數替換包含來自FA外部的所有變量作爲參數。那麼在這種情況下我該怎麼辦？我可以放下Exists量詞嗎？還是用常量替換它？謝謝！