sat-solvers

4热度

3回答

输入CNF为SAT4J求解

我一个全新的，以求解sat4j .. 它说，有些CNF文件应作为输入 是否有任何可能的方式给规则作为输入，并取得其是否是否可以满足？ 我的规则将是那种： Problem = ( (staff_1 <=> staff_2) AND (doctor_1 <=> physician_2) ) AND ( (staff_1 AND doctor_1

java nlp ontology sat-solvers sat4j 2010-10-15

---

4热度

2回答

如何将布尔表达式转换为cnf文件？

我需要使用解算器坐了检查布尔表达式的可满足.. 我有复杂的布尔表达式这样 有任何自动CNF文件转换器，这样我可以直接给它坐解决者？ 我读取cnf格式文件..但如何在.cnf文件中表达这个表达式？当palenthesis中存在连词时，我会感到困惑，并且如何表达 - >和< - >？请帮我

java boolean-expression conjunctive-normal-form sat-solvers 2010-10-16

---

4热度

1回答

解决在使用DPLL饱和解算器

我发现了一个坐在求解器在 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 (

java artificial-intelligence logic first-order-logic sat-solvers 2010-10-22

---

4热度

2回答

确定任意命题公式中变量的上下限

给定任意命题公式PHI（对某些变量的线性约束），确定每个变量的（近似）上下限的最佳方法是什么？ 某些变量可能是无界的。在这种情况下，算法应该得出结论：这些变量没有上/下限。例如，PHI =（x = 3 AND y> = 1）。 x的上下界都是3. y的下界是1，y没有上界。 这是一个非常简单的例子，但总体上有没有解决方案（可能使用SMT解算器）？

z3 sat-solvers 2012-01-24

---

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

optimization solver z3 satisfiability sat-solvers 2012-01-25

---

5热度

2回答

寻找SMT Z3用例（如DbC）和Z3开源替代品的实际例子？

我对这个工具的代码和开源替代品感兴趣并寻找SMT Z3用法的实际例子（如DbC）。所以，实际上，我感兴趣的相似Z3正式的解决工具，但： 它必须是开源 提供低级别（API）和高级（文字脚本）的相互作用 支持SMT-LIB 合适的（可用）在写/学习语言如Java，Python和Ruby，瓦拉和不哈斯克尔工具/ 具有基于其稳定的（在实践中使用）的工具，如按合同设计（DbC），静态类型验证等。 根据SMT

.net constraint-programming sat-solvers z3 2011-01-06

---

1热度

1回答

控制流枚举的Java解析器

是否有一个开源的Java解析工具，可以通过一个方法枚举控制流路径并在整数变量上计算范围约束？ （A周六 - 求解将是巨大的，以及） - 编辑 - This is the answer触发此问题。我想这是the commercial version of the tool。 我的问题是 - 什么是最接近开源的等价物？

java parsing control-flow sat-solvers 2012-02-15

---