將不可滿足的約束集合轉換爲可滿足的較小約束集合

我在我的腦海中有一個項目，我很好奇之前是否做過類似的事情。假設有一組不同的約束條件，並且這些約束條件不能一起滿足。將不可滿足的約束集合轉換爲可滿足的較小約束集合

C = {C1，C2，C3，...，CN}

（c1和c2和c3 ... CN）：不符合要求

我的目標是分割該組分爲k集合（可能k非常小），使得每一組約束都可單獨滿足。

基本的解決方案是使用貪婪的方法。約束將被選作第一個約束並標記爲第一組。然後，將選擇第二個，並檢查它是否可用第一個約束解決。如果它們是可解的，那麼第二個約束也將在第一個組中，否則，它將被標記爲第二個組。該過程將以這種方式繼續，直到該集合中沒有約束。做這件事的另一種方法可能是將約束分成兩組，並檢查這些組是否可以單獨解決。如果不是，則繼續遞歸分割。這兩種方法的規模都很大，它們將約束條件分成很小的集合。

我正在尋找一種將約束集劃分爲k個集合的有效方法，其中k接近最優值（最小k值）。這裏面臨2個挑戰，1）可伸縮性問題和2）約束結構事先是未知的。

來源

2015-10-20 genclik27

爲什麼你到底要做到這一點呢？如果您正在尋找調試方法，「不可核心」（或OR的Irreducable Inconsistent Subsystem）概念似乎密切相關。它在很多方面是相反的 - 一小部分不受約束的約束，從而消除其中的任何一個使得問題可以滿足。你當然可以使用這些現有的算法來啓發式地計算你想要的。 – tobyodavies

一個可以做你想做的算法可以用很少被研究的不可滿足的子集來表示。這是最新的SAT比賽賽道爲他們儘可能我可以告訴大家：http://www.cril.univ-artois.fr/SAT11/results/results.php?idev=48

利用這一點，下面的僞代碼應該做你想要

def sat_partition(CNF): 
    partitions = {} 
    while CNF is not empty: 
     MUS = compute_mus(CNF) 
     Remove one arbitrary element of MUS 
     partitions += {MUS} 
     CNF -= MUS 
    return partitions

來源

2015-10-27 03:08:50 tobyodavies

Thansk的答案。我也發現了一種類似的方法http://ijcai.org/papers13/Papers/IJCAI13-098.pdf我將實現你的算法並讓你知道結果。 – genclik27

將不可滿足的約束集合轉換爲可滿足的較小約束集合

回答

相關問題