sat

0熱度

1回答

我試圖從這個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變量公式路徑是解算

0熱度

1回答

使用Scala類的SAT求解器

我需要從用Scala編寫的應用程序調用通用SAT求解器。我正在研究SAT4J，因爲它可以很容易地導入爲jar文件，但是實際上很難實際使用它。有沒有一種方法可以從我的Scala代碼中釋放SAT4j jar文件來計算我的SAT問題？如果SAT4J不是正確的方法，是否有任何SAT庫可以直接使用，而不是啓動外部SAT解算器？

-1熱度

1回答

基於SAT運動規劃

SAT BASED MOTION PLANNING ALGORITHM 簡單運動規劃問題可以被改造爲一個SAT解決問題。任何人都可以解釋這是如何可能的？在這個問題中，我們必須找到從開始到結束位置的無碰撞路徑。

0熱度

1回答

找到一條路徑：SAT求解

我們給出了一個n * m網格，它在各個點都有障礙物，bot的起始和結束位置。任務是從頭到尾找到一條無碰撞的路徑。這個問題將被模擬爲SAT問題。請指導我在這種情況下應該做什麼來獲得最佳解決方案。

0熱度

1回答

SAT4J蘊涵使用情況

我是新來sat4j庫。我如何定義蘊含(A1 v A2 v A3) => (A1 ∧ A4)使用sat4j並找到所有變量的布爾值？我已經找到了sat4j單元測試比我在下面列出試過喜歡的東西。問題是hasASolution()返回true，但solution變量爲空。 DependencyHelper<String, String> dependencyHelper = new Dependency

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回答

Choco Sat配方

我想模擬一個使用巧克力4.0.1的SAT公式。我讀了docs，我試圖從javadoc瞭解，但不幸的是我失敗了。這是我第一次研究這些類型的問題，還有choco。所以，我可能會問一些非常明顯的問題。我需要一些限制的增加，如模型（VAR每一個BoolVar）： x <-> (a and -b) 我想在模型中使用ifOnlyIf方法，但我不知道如何否定一個變量，或者使用和。有人可以提供我（理想情況下

0熱度

1回答

SAT求解器：SAT4J - 更多示例？

我之前沒有用過SAT求解器，所以我開始學習如何使用SAT4J。大多數情況下，我正在使用它的API，但我有時會發現有些參數（在類或方法中）意味着什麼或者它們的格式/類型是可接受的，這很難理解。例如： public BinaryClause(IVecInt ps, ILits voc) 我的問題是，如果有一些使用示例，它可以幫助我更多地瞭解SAT4j中實現的功能？預先感謝您！

0熱度

1回答

格式化爲3SAT格式表

遠離python一段時間，因此格式化技能不存在。展望把這個格式的東西： [[8, -6, -4], [-10, 4, 6], [6, -8, -9]] 到的東西，看起來像這樣： (x8 v ~x6 v ~x4)^(~x10 v x4 v x6)^(x6 v ~x8 v ~x9) ，然後能夠引用的每個數字作爲單獨的輸入改爲T或F.任何指導意見會很高興。 import random def