Python SAT與pycosat

Question

我有一個課堂作業，我需要編寫一個函數，使用pycosat庫來測試SAT。我很難找出一組將從庫中返回「UNSAT」的參數。有人可以幫我找到一組不能「解決」的參數嗎？查看圖書館的單元測試，我能找到的唯一例子是[[1]，[-1]]

**這個任務要複雜得多，我只是想了解SAT求解器這是用來測試我的任務。

Answer 1

回答我自己的問題：您需要創建一個矛盾。創建3個變量（A，B，C）。爲了創建一個無法解決的計算，您需要創建一個布爾操作，使其無法解決。

（A或B）和（非A或未B）和（B或C）和（非B或C）

真值表將表明沒有A，B或C中的值的組合可能導致上述計算結果爲真。爲了表示這個pycosat，它看起來像：

[[1,2]，[-1，-2]，[2,3]，[-2,3]]