sat

1热度

2回答

我正在使用Python和Sympy。我有以下几点： x,y,z = Symbols('x,y,z') doc = {x : False, y : True, z: True} rule = Or(x, And(y,z)) 我要寻找一个在Sympy一个函数，将在rule.eval(doc)返回True？编辑：目前我正在使用rule.subs和rule.xreplace两个缓慢地执行，每

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变量公式路径是解算

6热度

1回答

Z3Py中的K-out-of约束

我正在使用Z3 theorem prover（Z3Py）的Python绑定。我有N个布尔变量，x1，..，xN。我想表达这样一个约束，即它们中的N个应该是正确的。我该怎么做，在Z3Py？有没有内置的支持？我查看了在线文档，但Z3Py docs没有提及任何API。我知道我可以分别表示至少有一个是真的（assert Or（x1，..，xN）），并且至多有一个是真的（assert Not（And）（x

-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添加单位子句）。但是如果我有多重假设呢？这可能吗？

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

3热度

1回答

SMT解决方案与自定义理论？

我在做一些验证工作，我已经将常规树语法作为基础理论。 Z3允许您定义自己的东西与未解释的函数，但是，如果您的决策过程是递归的，那么这种方法并不适用。他们曾经允许使用插件，但我认为这已经被删除了。我想知道，有没有人有一个体面的SMT解决方案的建议，让你写定制理论的决策程序？