我正试图用一个解决一个大的CNF公式SAT solver.公式(DIMACS格式)有4,697,898,048 = 2^32 + 402,930,752条款,我找到的所有SAT求解器都有问题:
- (P)lingeling报告"有太多条款"(即比标题行指定的条款更多,但事实并非如此)
- CryptoMiniSat4和picosat宣称读取标题行为402,930,752条款,其中2 ^ 32太少
- 葡萄糖似乎解析了98,916,961条款,然后报告使用简化解决了UNSAT公式,但这不太可能是正确的(公式的初始部分很短很可能是SAT).
是否有人知道可以处理这么大的文件的SAT求解器？或者是否有类似编译器开关的东西可以回避这种行为？我相信所有求解器都是为64位linux编译的.(当谈到处理这么大的数字时,我有点像菜鸟.抱歉.)
我正在使用Z3来提取不可满足的配方的不饱和核心.我正在使用Z3 @Rise界面(基于Web)编写以下代码,
(set-logic QF_LIA)
(set-option :produce-unsat-cores true)
(declare-fun ph1 () Int)
(declare-fun ph1p () Int)
(declare-fun ph3 () Int)
(declare-fun ph3p () Int)
(declare-fun ph4 () Int)
(declare-fun ph4p () Int)
(define-fun one () Bool (= ph3p (+ ph1 1)))
(define-fun two () Bool (= ph3 (+ ph1 1)))
(define-fun three () Bool (= ph1p (+ ph1 1)))
(define-fun four () Bool (= ph4p (+ ph1p 1)))
(define-fun five () Bool (>= ph1 0))
(define-fun six () Bool (>= ph4 …我从Z3的运行中获得了几个统计数据.我需要了解这些意味着什么.对于sat和SMT解决方案的最新发展,我相当生疏,并且没有及时更新,因此我试图自己找到解释并且我可能会出错.所以我的问题主要是:
1)这些措施的名称是什么意思？
2)如果错了,你能指点我更好地理解他们所指的内容吗？
其他观察结果如下,概念上属于上述两个问题.提前致谢!
我的解释如下.
DPLL.下面的所有指标都参考了DPLL算法的行话,这是大多数求解器的基础.
决议.粗略地说,操作使解释条款成为集合; 从分辨率中获取的技术是解决SAT的另一种范例.
其他技术
其他方面
我有兴趣和寻找SMT Z3使用的实际例子(如DbC)以及该工具的代码和开源替代品.所以,事实上,我对类似的Z3正式求解工具很感兴趣,但是:
根据SMT-LIB主页(详见bit.ly软件包),2010年SMT解决方案列表为:"Alt-Ergo,Barcelogic,Beaver,Boolector,CVC3,DPT,MathSAT,OpenSMT,SatEEn,Spear,STP,SWORD, UCLID,veriT,Yices,Z3."
请提供有关在实践中使用其中任何一个的任何反馈(代码示例是最好的)？
最后,任何有关它与GHC可能性进行比较的信息都是有用的,但仅限于存在实施示例(不是语言"特征")的情况.
有关Z3的更快速信息,请访问http://bit.ly/bundles/ewiger/1
给定任意命题公式PHI（某些变量具有线性约束），确定每个变量的（近似）上限和下限的最佳方法是什么？
一些变量可能是无界的。在这种情况下，算法应得出结论，这些变量没有上限/下限。
例如，PHI =（x = 3 AND y> = 1）。x的上限和下限均为3。y的下限为1，并且y没有上限。
这是一个非常简单的示例，但是是否有一般的解决方案（也许使用SMT求解器）？
链接：具有Pyhton绑定的
Z3定理证明者
picosat
我已经使用Z3作为SAT求解器。对于较大的公式，似乎存在性能问题，这就是为什么我想查看picosat来查看它是否是更快的替代方案。我现有的python代码使用z3语法生成一个命题公式：
from z3 import *
import pycosat
from pycosat import solve, itersolve
#
#1 2 3 4 5 6 7 8 (variable names in picosat are numbers!)
#
C, G, M, P, R, S, SN, B = Bools('C G M P R S SN B')
C = (And(*(S,Or(Not(S),P),Or(Not(P),S),Or(Not(P),B),Or(Not(C),P),Or(Not(G),P),Or(Not(M),P),Or(Not(R),P),Or(Not(SN),P),Or(Not(B),P),True,Not(False),Or(R,SN,B,G,M,C,True))))
# formula in Z3:
f = simplify(C)
print f
输出/结果
And(S,
Or(Not(S), P),
Or(Not(P), S),
Or(Not(P), B),
Or(Not(C), P),
Or(Not(G), P),
Or(Not(M), P),
Or(Not(R), P),
Or(Not(SN), P),
Or(Not(B), …是否有增量 SMT 求解器或某些增量 SMT 求解器的 API，我可以在其中增量添加约束，在其中我可以通过某些标签/名称唯一标识每个约束？
我想唯一地标识约束的原因是，我可以稍后通过指定该标签/名称来删除它们。需要删除约束是因为我之前的约束随着时间变得无关紧要。我看到使用 Z3 我不能使用基于推送/弹出的增量方法，因为它遵循基于堆栈的想法，而我的要求是删除特定的早期/旧约束。使用基于假设的 Z3 的其他增量方法，我将不得不执行格式“(check-sat p1 p2 p3)”的 check-sat，即如果我有三个断言要检查，那么我将需要三个布尔常量 p1,p2 ,p3，但在我的实现中，我一次要检查数千个断言，间接需要数千个布尔常量。我还检查了 JavaSMT，一个用于 SMT 求解器的 Java API，
我想知道是否有任何增量求解器可以添加或删除由名称唯一标识的约束，或者有其他方法来处理它的 API。我将不胜感激任何建议或意见。
我是一个全新的sat4j求解器..
它说一些cnf文件应该作为输入
是否有任何可能的方法将规则作为输入并获得它是否可满足？
我的规则将是那种:
Problem = (
( staff_1 <=> staff_2 ) AND
( doctor_1 <=> physician_2 )
) AND (
( staff_1 AND doctor_1 )
) AND (
NOT( ward_2 AND physician_2 ) AND
NOT( clinic_2 AND physician_2 ) AND
NOT( admission_record_2 AND physician_2 )
) AND (
NOT( hospital_2 AND physician_2 ) AND
NOT( department_2 AND physician_2 ) AND
NOT( staff_2 AND physician_2 )
)
有人可以帮我解决这个问题,使用sat4j求解器吗？
我找到了一个坐着的求解器
http://code.google.com/p/aima-java/
我尝试使用以下代码来使用dpllsolver解决表达式
输入是
(A <=> B) AND (C => D) AND (A AND C) AND (NOT (B AND D)) AND (NOT (B AND D AND E))
CNF变压器将其转换为
( ( ( NOT A ) OR B ) AND ( ( NOT B ) OR A ) )
它不考虑逻辑的其他部分,它只考虑第一个术语,如何使其正常工作？
请建议我,如果其他一些坐着的解决方案可以做到这一点
PEParser parser = new PEParser();
CNFTransformer transformer=new CNFTransformer();
Sentence and;
Sentence transformedAnd;
DPLL dpll = new DPLL();
Sentence sentence = (Sentence) parser.parse("(A <=> B) AND (C => D) AND (A AND …java logic artificial-intelligence sat-solvers first-order-logic
现在我正在写一篇关于 SAT 解答的文章，但我陷入了困境。我希望你能帮助我。
\n\n我想描述一些解决 SAT 问题的方法。现在我有三种不同的方式：
\n\n我的问题是唯一有效的算法是 DPLL（以及其他一些与 DPLL 略有不同的算法）。因此我没有什么可以与 DPLL 进行比较。
\n\n我的问题：如果您能告诉我一些不基于 DPLL (DP) 的算法，我可以将其进行比较，那就太好了。
\n\n以下是我发现的一些，但无法确定它们是否是一个不错的选择，或者是否有更好的选择：
\n\n感谢您的帮助。
\n