用多種假設求解

Question

假設我有一個變量(a,b,c,d,e,f,g)的CNF表達式。考慮到{a,b,c,g} = {1,0,0,1}和{a,b,c,g} = {1,1,1,1}，如何使用SAT解算器找到(d,e,f)的作業？如果這是一個假設，那麼調用座標求解器來尋找{d,e,f}的分配將是直接的（例如，通過向CNF添加單位子句）。但是如果我有多重假設呢？這可能嗎？

Answer 1

下面是哈羅德試圖向你描述什麼（我想）的步驟。你在變量a，b，c，d，e，f和g上有一些CNF公式F.

1. 重複該式中，主叫重複G.
2. 在G，與AA BB與替換變量a，B，C與cc，並且與GG克。
3. 將單位從句添加到F中，使（a，b，c，g）=（1,0,0,1）。
4. 將單位從句添加到G中，使（aa，bb，cc，gg）=（1,1,1,1）。
5. 連接公式F和G並將結果輸入到SAT解算器中。

求解器將找到與（a，b，c，g）和（aa，bb，cc，gg）的預設值一致的令人滿意的賦值。

Answer 2

這是不是很清楚，如果你想要一個實際的答案或有趣的理論上的答案。我會去實際的。

對於每組假設，調用一個座標解算器，該座標解算器支持在假設條件下（example）的假設。在同一個求解器實例上按順序執行此操作。

優點：

• 你不要混用互相排斥的集合假設滿足性。如果一組假設A對公式F滿足，而另一組A'對於F不滿足，那麼對求解器的每次調用都會告訴你這些假設是否爲飽和/不滿。
• 來自第一個電話的已知條款可能會停留在第二個電話。中級學習語句談論相同的變量。 （注意：如果你有一個不相交的公式F & G其中F超過了變量X，G超過了變量Y和X而Y沒有共享變量，分辨率 - CDCL中使用的推理規則 - 不能得出混合F和G的子句。是兩個混合在一起，而不是分開分裂他們，除非一個實例是很容易證明不飽和度，並停止早期沒有明顯的增益）

缺點：

• 如果實例的難以解決練習但A'是微不足道的，你可能會卡在A.
• 它不是平行的，所以如果你有更多的實例比兩個你想盡快解決，你需要更多的機制。

我知道這是一個明顯的答案，但值得一試。如果失敗了，你可以嘗試做更有趣的事情，比如解決w.r.t.假設A union A'，並且只有這樣才能解決這個A和A'的策略。這對你的例子沒有幫助，因爲(a,b,c,g) = (1,0,0,1)和(a,b,c,g) = (1,1,1,1)是互斥的。