我正在嘗試使用Z3（一種由Microsoft Research開發的SMT求解器）來檢索一些一階理論的所有可能模型。這是一個最小的工作示例：(declare-const f Bool)(assert (or (= f true) (= f false)))在這種命題情況下，有兩個令人滿意的分配：f->true和f->false。由于Z3（通常是SMT求解器）只會嘗試找到一個令人滿意的模型，因此不可能直接找到所有解決方案。在這里，我找到了一個名為的有用命令(next-sat)，但似乎最新版本的Z3不再支持此命令。這對我來說有點不幸，總體而言，我認為該命令非常有用。還有另一種方法嗎？
2 回答
慕標琳琳
TA貢獻1830條經驗 獲得超9個贊
對于我使用此方法的示例，似乎很有意義，因為在初始模型之后找到下幾個模型更快。以下是針對58個模型的特定情況的運行時間（以毫秒為單位）的列表： 8942 801 1663 5 599 320 450 2 2 3 1 5 1377 36 5 738 162 105 1639 3 5 16 2041 27 475 953 562 746 45 151 18 4206 3416 9 850 120 3 4 12 615 593 1219 449 154 987 3 10 1365 16 438 792 1686 743 46 5 8 412 126。請注意，第一個絕對是最長的，但是其他的則隨機得多（可能取決于問題以及求解器獲得的幸運程度）。
添加回答
舉報
0/150
提交
取消