sat-solvers

3熱度

2回答

我正在使用Z3 Python接口爲我的實驗創建公式。然後我將這個公式發送給Z3解算器。如果我是正確的Z3使用它自己的求解器！如何在Z3py中使用不同的SAT/SMT解算器？我在CBMC（C有界模型檢查器）中使用它的方式：運行程序並吐出中間DIMAC表示（在文件中），然後將該文件用作其他SAT求解器的輸入。我可以在Z3做類似的事情嗎？謝謝。

0熱度

1回答

關於sat4j，如何使用sat4j來解決僞布爾問題？

我有僞布爾問題，我需要用sat4j來解決它。有人可以幫助我嗎？這裏是我的問題：我有一個名爲的變量列表：A，B，C，d，E，F 而且我所代表的值的列表：＃ 1，＃2，＃3 ..... H（A，＃1）是指分配＃1到我有一些實施例C onstraints： h(a,#1)=1 h(a,#1)+h(b,#1)+h(c,#1)=1 h(a,#1)+h(a,#5)>=1 h(b,#2)+h(b,

0熱度

1回答

/usr/bin/ld：找不到-lcplex

我試圖從這個git repo設置MaxHS SAT求解器 - https://github.com/fbacchus/MaxHS。我得到一個錯誤，說'/ usr/bin/ld：can not find -lcplex'。任何人都可以指導我什麼是lcplex庫和如何解決這個問題？我的控制檯看起來像這樣.. install -d /mnt/c/Akhil/Abhyas/CQA/maxhs_ins

2熱度

1回答

MiniSat中的非決策變量的語義是什麼？

當使用MiniSat作爲C++庫時，每個新變量都可以創建爲決策變量或非決策變量。我對此的粗略理解是，當解算器決定在分支期間使用下一個變量時，不考慮非決策變量。然而，在我的項目中，當非決策變量位於蘊含的左側時，我遇到了麻煩，而不是等價關係，因爲求解器返回了SAT，即使公式實際上是UNSAT。進一步的實驗表明，只有當非決策變量在一個長於2個變量的公式中時纔會出現這種情況（我認爲2變量公式路徑是解算

1熱度

1回答

從CNF轉換爲喇叭形式

如何使用Prolog將CNF子句轉換爲喇叭形式？我正在嘗試創建一個將CNF作爲輸入的SAT求解器，這將需要轉換爲喇叭形式。

1熱度

1回答

在Z3中將函數作爲屬性的數據類型Python

我正在使用Z3的Python綁定，並嘗試創建屬性爲函數的Z3數據類型。例如，我可以執行以下命令： Foo = Datatype('Foo') Foo.declare('foo', [('my_function', Function('f', IntSort(), BoolSort()))]) Foo.create() 這是試圖建立一個數據類型Foo與屬性my_function，在那裏我將能

4熱度

1回答

增量式SMT解算器具有降低特定約束的能力

是否有增量式SMT解算器或某些增量式SMT解算器的API，我可以在其中增量添加約束，我可以通過某些標籤/名稱唯一標識每個約束？我想唯一標識約束的原因是我可以稍後通過指定該標籤/名稱來放棄它們。需要放棄約束是因爲我早先的約束與時間無關。我看到，與Z3我不能使用基於推/彈出的增量方法，因爲它遵循基於堆棧的想法，而我的要求是放棄特定的早期/舊約束。隨着Z3基於假設的其他增量方法，我將不得不執行格

1熱度

1回答

使用Z3和c＃

獲取不穩定的核心示例我想在C＃實現中使用Z3座標解算器。此代碼非常接近Microsoft本身在「http://z3.codeplex.com/SourceControl/latest#examples/dotnet/Program.cs」中給出的示例。我的代碼是： using (Context ctx = new Context(new Dictionary<string, string>() {

1熱度

2回答

用多種假設求解

假設我有一個變量(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添加單位子句）。但是如果我有多重假設呢？這可能嗎？

1熱度

1回答

使用命題邏輯求解方程

我正在尋找關於如何將數學方程式編碼爲cnf-sat形式的想法，以便他們可以通過像MiniSat這樣的開源SAT求解器來解決。所以，我怎麼轉換是這樣的： 3X + 4Y - Z = 14 -2x - 4Z < = -6 X - 3Y + Z> = 15 成爲可以通過使用SAT求解器求解的命題式。任何建議，因爲我很難過？