sat相关内容

Z3-Python中的SAT查询变慢了：增量式SAT怎么办？

在Z3(Python)中，循环内的SAT查询速度变慢，我可以使用增量SAT来解决此问题吗？ 问题如下：我在循环中执行具体的SAT搜索。在每次迭代中，我都会得到一个模型(当然，我存储了该模型的否定，以便不会再次探索相同的模型)。此外，如果该模型满足某个属性，我还会添加它的子查询，并将其他限制添加到公式中。然后再次迭代，直到获得UNSAT(即不再有模型)。 我提供代码的定向快照： ..

发布时间：2022-08-22 00:00:00 z3 z3py theorem-proving sat 其他开发

在Z3-Python中，我在执行模型搜索时得到"；Builtin_Function_or_Method'；对象不可迭代

我正在探索在Z3(Python)中执行SAT解算的快速方法。为此，我尝试模仿https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-blocking-evaluations第5.1章的结果。 我使用的代码如下： def block_modelT(s, terms): #I used the name 'block_mode ..

发布时间：2022-08-21 22:00:41 python z3 z3py theorem-proving sat Python

如何使Z3'；(Python)的SAT解算偏向某个标准，例如更倾向于有更多否定的文字

在Z3(Python)中，有没有办法将SAT搜索“偏向”“条件”？ 一个案例：我希望Z3获得一个模型，但不是任何模型：如果可能，请给我一个有大量否定文字的模型。 例如，如果我们必须搜索A or B，可能的模型是[A = True, B = True]，但我宁愿收到模型[A = True, B = False]或模型[A = False, B = True]，因为它们有更多的False分 ..

发布时间：2022-08-21 21:35:15 z3 z3py theorem-proving sat satisfiability 其他开发

Z3 或 Z3Py 中的假设

有没有办法在 Z3 中表达假设(我使用的是 Z3Py 库)，这样引擎就不会检查它们的有效性，而是将它们作为基础理论，就像在定理证明中一样? 例如，假设我有两个参数为 Real 类型的一元函数.我想告诉 Z3 引擎，对于所有输入值，f1(t) 等于 f2(t). 在 Z3Py 中编码，如下所示: t = Real("t") 假设 1 = ForAll(t, f1(t) = f2(t) ..

发布时间：2021-10-04 20:38:09 z3 z3py satisfiability sat 其他开发

为什么已经弹出的范围会影响后续范围中的 check-sat 时间?

一般问题 我多次注意到已经弹出的 push-pop 作用域似乎会影响后续作用域中 check-sat 所需的时间. 也就是说，假设一个程序有多个(可能是任意嵌套的)push-pop 作用域，每个作用域都包含一个 check-sat 命令.此外，假设第二次 check-sat 需要 10s，而第一个只需要 0.1s. ...(推)(断言(不是 P))(检查周六)；可能是坐的、不坐的或未 ..

发布时间：2021-07-16 21:37:35 scope z3 sat 其他开发

使用 google or-tools SAT 求解器舍入 Non-LinearExpr

使用谷歌或工具的CP-SAT我'我正在尝试编写此约束: q >= (50x + 100y + 150z + 200k + 250p + 300v)/(x + y + z + k + p + v) 其中 q 是一个简单的整数. 问题是我需要将等式的右侧四舍五入(我们称之为 expression)如下: if(表达式 所以我需要对表达式进行四舍五入 (50x + 100y + 1 ..

发布时间：2021-06-12 20:54:30 optimization nonlinear-optimization or-tools sat 其他开发

CNF按真值表

我有一个由真值表显示的布尔函数. 总共有10个变量，我想获得具有合理长度的CNF(不必最短，但足够短). 我该怎么办? Python脚本或任何公共可用的软件(例如Mathematica/Mapple/etc)对我也可以正常工作. 解决方案 sympy 包使您可以立即执行此操作.( https://www.sympy.org/en/index.html ) 这是一个简 ..

发布时间：2021-05-31 20:49:46 python math sat boolean-algebra cnf Python

基于SAT的运动计划

SAT BASED MOTION PLANNING ALGORITHM 一个简单的运动计划问题可以重构为 SAT解决问题.谁能解释这怎么可能? 在这个问题中，我们必须找到从起点到终点的无碰撞路径. 解决方案 最简单的示例如下所示. 让我们介绍N行和M列的2D网格，移动代理A从节点(x，y)开始.他的目标T的坐标为(x_i，y_j): 要达到 ..

发布时间：2020-07-06 05:40:39 sat motion-planning 其他开发

简化CNF公式，同时保留所有包含某些变量的解

相关: CNF简化(实际上，我认为该问题的提交者可能是在我之后要在这里 存在许多用于简化(或在求解之前进行“预处理")DIMACS格式CNF公式的工具，并且大多数SAT求解器都包含一些工具.但是，我所知道的全部都是将一个可满足条件的公式简化为具有零个或一个变量的可满足条件的CNF，即它们仅试图保持该公式的可满足性.我至少尝试过SatELite和cryptominisat的预处理模式. ..

发布时间：2020-07-06 05:40:35 z3 simplify sat 其他开发

Z3:非线性算法的奇怪行为

我刚刚开始使用Z3(v4.4.0)，我想尝试其中一个教程示例: (declare-const a Int) (assert (> (* a a) 3)) (check-sat) (get-model) (echo "Z3 will fail in the next example...") (declare-const b Real) (declare-const c Real) (ass ..

发布时间：2020-07-06 05:40:32 z3 solver smt sat 其他开发

如何使z3返回多个unsat核心，多个令人满意的分配

我正在研究一种研究工具； 我有兴趣检索(针对QF_LRA) -多个(最小或其他)UNSAT核心和 -多个SAT作业 我已经在论坛上检查了有关此主题的较早讨论，例如， 如何获取不同的unsat核心在逻辑QF_LRA上使用z3时 它们指的是z3 Python教程 例如 http://rise4fun.com/Z3Py/tutorial/musmss ，目前似乎已离线.我尝试了 ..

发布时间：2020-07-06 05:40:28 z3 smt sat 其他开发

为什么Z3Py无法提供所有可能的解决方案

我遇到了一个问题，其中Z3Py并未枚举给定布尔条款的所有可能解决方案.我想知道是否有人知道为什么会这样. 这是我用于Z3Py的代码.有5个布尔值:1 2 3 4和5. from z3 import * a,b,c,d,e = Bools('1 2 3 4 5') solver = Solver() solver.add(Or(Not(a), Not(b))) solver.add(O ..

发布时间：2020-07-06 05:40:25 python z3py sat Python

Z3Py中的K出N约束

我正在为 Z3定理证明器(Z3Py)使用Python绑定.我有N个布尔变量x1，.. xN.我想表达一个约束，即其中N个中的K个应该正确.如何在Z3Py中做到这一点?有内置的支持吗?我检查了在线文档，但是 Z3Py文档没有提及为此的任何API. 对于N分之一的约束，我知道我可以分别表示至少一个为真(断言Or(x1，..，xN))，至多一个为真(断言Not(And( xi，xj))对于所有i， ..

发布时间：2020-07-06 05:40:21 z3 z3py sat 其他开发

具有自定义理论的SMT求解器?

我正在做一些验证工作，在这些工作中我将常规树语法作为基础理论. Z3允许您使用未解释的函数来定义自己的东西，但是在您的决策过程是递归的时候，这往往无法正常工作.我认为他们曾经允许使用插件，但是已经过时了. 我想知道，有没有人建议过像样的SMT求解器，使您可以编写自定义理论的决策程序? 解决方案 鉴于最合理的SMT求解器是开源的，因此您有多种选择，您可以根据需要花费的时间和精力来 ..

发布时间：2020-06-15 19:01:51 z3 verification smt formal-verification sat 其他开发

.SAT（ACIS）文件操纵脚本

我需要为ACIS文件操作创建脚本，例如： 我有1个SAT文件，该文件是从带有3D模型的CAD软件中导出的，我想要创建以某种语言（php，python等，甚至.BAT，如果可以工作的话）打开SAT文件的脚本，请删除3D模型中的所有组件。我只想要3D模型的外部。 有什么方法可以做到？因为我查看SAT文件，而且其中包含大量文本行，也许可以使用RFC和一些棘手的工具来做到这一点。 任何想 ..

发布时间：2020-05-31 21:25:09 scripting 3d cad file-manipulation sat 其他开发

SCIP代码如何处理SAT问题?

我正在尝试找出SCIP如何处理SAT问题. 在SCIP网站上，建议在读取cnf文件后在SAT问题中的命令行中键入"set强调cpsolver".然后，在键入"optimize"之后，SCIP求解器将做自己的事情.我对代码跟踪不是特别熟练，并且想知道SCIP求解器在键入“设置强调cpsolver"命令后采用的途径. 此命令是否处理SAT问题并从其他地方简单地调用SAT解算器?还是将SAT ..

发布时间：2020-05-06 11:55:22 mathematical-optimization scip sat 其他开发

解决命题逻辑/布尔表达式的工具(SAT解算器?)

我是命题逻辑和布尔表达式的新手.所以这就是为什么我需要帮助.这是我的问题: 在汽车工业中，购买汽车时可以选择成千上万种不同的组件.并非每个组件都是可组合的，因此对于每辆汽车，都有很多以命题逻辑表示的规则.就我而言，每辆车都有2000到4000条规则. 它们看起来像这样: A→B∨C∨D C→¬F F∧G→D ... 其中“∧" =“和"/“∨" =“或"/“¬" =“ ..

发布时间：2020-05-03 08:58:05 logic boolean-logic boolean-expression sat satisfiability 其他开发

流量/车间到布尔可满足性[多项式时间减少]第2部分

这里是我的第一个问题的延续（由于什么是错的，我也没成功，知道在什么地方。我问了计算器的主人的帮助下再次：） 对于和行动的是我对现在的： 在我有谁是这样的输入文件： 3 2 1 1 1 1 1 1 谁再presents：3的工作，2店（机），并在每个车间（机）每个作业的时间。而且我要为论文的问题，找到最佳C_max值。 因此​​，例如，它应该在输出给这个结果（对不 ..

发布时间：2015-11-30 22:03:02 c algorithm optimization reduction sat C/C++

流水车间到布尔可满足性[多项式时间减少]

我为了得到一个想法上与您联系“如何改造一个流水车间调度问题”变成了布尔可满足性。 我已经做了这样减少了A N * N的数独，一个N皇后与一类调度问题，但我对如何在流水车间改造成SAT一些问题。 一个SAT问题是这样的： 的目标是：用不同的布尔变量，以找到每一个变量的做作，以使“句子”如此。 （如果找到一个解决方案是可能的）。 创建我自己的求解器遗传算法能够找到一个解决方案，以证明时，有 ..

发布时间：2015-11-30 21:29:33 algorithm optimization reduction sat C/C++

排课布尔可满足性[多项式时间减少]

我有一些理论框架/实际的问题，我没有线索，现在如何管理，这就是： 我创建了一个 SAT求解能够发现，当一个人存在，并证明的矛盾时，它的一个模型不使用遗传算法用C CNF 问题的情况下。 一个SAT-问题基本上是这样那样的问题： 我的目标是利用该解算器找到了很多型动物的 NP-完成的问题的解决方案。基本上，我翻译型动物问题转化为SAT，SAT解决我的解算器，然后变压器的解决方案到解决方案接受了原 ..

发布时间：2015-11-30 13:50:02 c algorithm scheduling reduction sat C/C++