sat4j

0熱度

1回答

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

0熱度

1回答

SAT4J蘊涵使用情況

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

2熱度

1回答

解析和簡化CNF文件的時間

我剛開始使用Sat4j庫。你能指導我如何計算解析和簡化給定的CNF輸入所花費的時間。我已經使用 ISolver solver = SolverFactory.newDefault(); Reader reader = new DimacsReader(solver); IProblem problem = reader.parseInstance(filename.cnf); boolea

0熱度

1回答

Sat4j遠程控制窗口未打開

0熱度

1回答

SAT4J embibeding求解器例外

我正在嘗試爲我的學校項目建立N * N Queen求解器。我制定了一個計劃，即生成CNF聲明。我試圖給它的地址作爲「SAT4J embbeding求解器」7th page, 3.1的參數，但它一直拋出ParseFormatException。我也嘗試使用這個文本文件我發現在計算器上： c you can put comment here. c Formatted by StackOverFlo

0熱度

1回答

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

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

4熱度

3回答

輸入CNF爲SAT4J求解

我一個全新的，以求解sat4j .. 它說，有些CNF文件應作爲輸入是否有任何可能的方式給規則作爲輸入，並取得其是否是否可以滿足？我的規則將是那種： Problem = ( (staff_1 <=> staff_2) AND (doctor_1 <=> physician_2) ) AND ( (staff_1 AND doctor_1

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,