satisfiability

1熱度

1回答

我想解決一個SAT問題，它只包含一個熱點約束。現在我使用Claessen在第二部分提出的單一編碼。 4.2 [1]和MiniSAT。我想知道是否有更好的方法來解決這個問題，與基於CNF的SAT求解器相比，這種類型的求解器更適合這類問題。我已經查了一下，但根本找不到關於SAT和單熱約束的很多信息。 [1] Successful SAT Encoding Techniques. Magnus Bji

0熱度

2回答

SMT-Lib標準是否支持理論的組合？

我知道有幾件作品正在試圖處理SMT理論的結合。但是，SMT-Lib 2.0語言（http://smtlib.cs.uiowa.edu/docs.html）在這一點上並沒有提到任何問題。我的問題是它是否支持這一點，以及Solvers提供瞭如何同時使用多種理論的能力？感謝，

0熱度

2回答

布爾式編碼

我想知道如何需要許多比特來編碼的布爾公式像 @(x1,x2,x3,x4) = (x1 OR x2 OR NOT(x3) OR x4) AND ((NOT)x2 OR x3) AND (x1 OR (NOT)x4) @是SAT的一個實例。我認爲它是4位，因爲可能的組合總數是2（power4）。那是對的嗎？我應該計算OR，NOT，還是計算編碼所需的位數？我搜查了很多，但無法找到任何東西。

3熱度

1回答

錯誤的結果從z3

我試圖用Z3 SMT求解器證明以下內容：((x*x) + x) = ((~x * ~x) + ~x)。這是正確的，因爲c語言中的溢出語義。現在，我寫了下面的SMT-LIB代碼： (declare-fun a() Int) (define-fun myadd ((x Int) (y Int)) Int (mod (+ x y) 4294967296)) (define-fun mynot

4熱度

1回答

最小獨立集合

給定一組公式s，我想找到s的最小子集s'，暗示s中的每個公式。我將s稱爲最小的獨立集合，因爲中的每一對a,b,a並不意味着b，反之亦然。在我看來，天真的方法將需要O(2^|s|)複雜性。有沒有更有效的方法？這個問題可以編碼一些如何利用當前的smt/sat求解器（例如不可核心）？

2熱度

2回答

Max-SMT解算器如何工作？

SMT解算器是針對與SAT類似的可滿足性開發的。正如我們所知道的，SAT也是可以滿足的，並且提出了SAT的變體。其中之一是max-SAT。所以我想問問是否存在最大SMT解算器，如果存在，它是如何工作的？

6熱度

1回答

布爾可滿足性 - 算法

我有一個布爾公式：（x_ {1}或x_ {2}）和（x_ {3}或x_ {4}）以及.....和（x_ {2r-1 }或x_ {2r}），其中x_ {i}屬於集合：{p_ {1}，p_ {2}，... p_ {99}，〜p_ {1}，〜p_ { 2}，...〜p_ {99}}我必須確定是否對於某些值x_ {i}給出的公式可以是真實的。我知道它在計算上一般很困難。但是有沒有比較快的方法可以解決這個

-3熱度

1回答

Dpll，SAT（可滿足性）問題，需要DPLL函數或程序？

這裏是我的問題，我stucked在Matlab與SAT問題（Satisfability）其實我需要一個叫做DPLL功能，我是在這裏看到的地方，但它在Java中，任何人都可以幫我請？感謝

12熱度

2回答

是否可以使用SAT求解器查找所有解決方案？

我寫了一個我認爲是quite interesting question的答案，但不幸的是，這個問題在我發佈之前被作者刪除了。我在這裏重新發布這個問題的總結和我的答案，以防其他人使用它。假設我有一個SAT求解器，給定一個布爾公式以聯合範式，返回解決方案（滿足公式的變量賦值）或問題不可滿足的信息。我可以用這個求解器找到全部是的解決方案嗎？

1熱度

1回答

用於SAT預處理的哈希函數

在預處理包含子句數據庫的SAT實例期間，每個變量都需要分配一個單詞。散列函數爲每個變量返回一個僅由0組成的32位字，除了16個最高有效位（MSB）中的一個位和16個最低有效位（LSB）中的一個位，它們被設置爲1，具體取決於變量。子句的簽名是其所有變量的哈希函數值的按位或。如何實現這個散列函數？