腾讯云
开发者社区
文档
建议反馈
控制台
首页
学习
活动
专区
工具
TVP
最新优惠活动
文章/答案/技术大牛
搜索
搜索
关闭
发布
登录/注册
精选内容/技术社群/优惠产品,
尽在小程序
立即前往
文章
问答
(9999+)
视频
沙龙
2
回答
使
约束
求解
器
的
约束
更难
求解
?
constraints
、
z3
、
smt
、
satisfiability
、
constraint-satisfaction
我是SMT
求解
的
新手,我写信是为了询问一些建议和指示,以了解什么是SMT
求解
器
要解决
的
真正
的
difficult constraint,例如Z3。我尝试调整位向量
的
长度,例如,通过以下方式: >>> a = BitVec("a", 10000)>>> c = a >> 18 + 6 - 32我知道一些密码散列函数
浏览 27
提问于2019-01-29
得票数 2
回答已采纳
1
回答
在
约束
求解
中,SMT-solver比CSP-solver有什么优势?
constraint-programming
、
satisfiability
SMT-Solver可用于
约束
求解
。正如我们所知,CSP
求解
器
也用于多年来
的
约束
求解
。那么,与CSP
求解
器
相比,SMT-solver有什么优势呢?
浏览 6
提问于2012-05-14
得票数 8
2
回答
如何在Excel
求解
器
约束
中使用"or“
excel
、
excel-2010
我正在向Excel
求解
器
添加
约束
。由于我在
求解
器
约束
框中找不到'or‘函数,如何在Excel
求解
器
中添加此
约束
。
浏览 2
提问于2013-10-11
得票数 0
1
回答
约束
求解
器
与SMT
求解
器
z3
、
smt
、
constraint-programming
、
gecode
有人能给我举一些例子,这些例子可以用SMT
求解
器
(比如microsoft z3 )来解决,但是不能通过
约束
求解
器
(比如Gecode )来解决吗?
约束
求解
器
和SMT
求解
器
的
基本区别是什么?
浏览 5
提问于2020-05-27
得票数 1
1
回答
Z3解决程序()中
约束
的
大小
python
、
z3
、
smt
、
z3py
有什么方法可以让我们得到在
求解
器
中添加了多少
约束
吗?例如,我们初始化一个z3
求解
器
s = Solver(),然后使用s.add()向它添加
约束
。我们如何才能得到最终被添加到
求解
器
中
的
约束
数?
浏览 0
提问于2019-01-08
得票数 1
回答已采纳
1
回答
带stp
的
Klee和其他卫星解算
器
的
Klee
llvm
、
klee
Klee使用STP作为
约束
求解
器
,但理论上可以改变其
求解
器
。STP不允许浮点操作。如果我们决定用另一个
约束
求解
器
代替STP,比如z3,klee是否能够生成浮点
约束
?它是在smt语言中生成fp
约束
,stp不能处理这些
约束
,还是根本不生成fp
约束
? 如能提供你
的
答复,我将不胜感激。
浏览 0
提问于2015-05-11
得票数 1
回答已采纳
1
回答
使用持久
求解
器
处理ConstraintList
pyomo
我想尝试对迭代地向问题添加新
约束
的
算法使用持久
求解
器
,并希望避免在每次迭代之前必须完全重新构建提供给
求解
器
的
文件。在使用中描述
的
持久
求解
器
之前,我使用了一个ConstraintList对象来迭代地添加我
的
新
约束
,而不必单独命名它们。我认为这是一个非常优雅
的
解决方案,我想看看是否有一种方法可以在新
约束
添加到ConstraintList时通知持久<e
浏览 0
提问于2018-11-13
得票数 0
1
回答
Cola.js + d3.js在强制
求解
器
运行期间/之后强制定向网络
约束
节点
svg
、
d3.js
、
hierarchy
我正在使用Cola.js和d3.js创建一个有力引导
的
传家宝阴谋。节点是使用Y
约束
在行上堆叠
的
,我已经根据给定节点
的
最大深度进行了预先计算。是否有一种好
的
方法使用Cola.js将节点与力
求解
器
结合起来
约束
为列?我想中心
的
节点围绕Y,但也使用力
求解
器
的
定位,以计算最短
的
边缘距离,从而减少边缘交叉。这样做
的
目的是
使
图中
的</
浏览 1
提问于2014-09-15
得票数 4
回答已采纳
1
回答
EXCEL:
求解
器
约束
excel
、
constraints
、
solver
我想请求帮助设置
求解
器
。 假设我有5个单元格,必须分配总和为1000
的
值。但是,如果可以容纳其他
约束
,则其中一些可以为零。在这一点上,我得到了一些
求解
器
输出,
使
5个零中
的
4个,并将1000分配给1个单元格。 我想知道如何添加另一个
约束
来告诉
求解
器
,比如说,5个中至少有3个不能为零(任意5个)。 您
的
协助将不胜感激。谢谢
浏览 24
提问于2020-01-29
得票数 0
2
回答
vba :似乎无法关闭
求解
器
的
“将无
约束
变量设为非负”选项
vba
、
setting
在SolverReset之后在
求解
器
中关闭
使
无
约束
变量为非负数
的
命令有哪些?我试着录制了一个宏但我得到
的
只是,'' SolverOk SetCell:="$D$26", MaxMinVal:=2, ValueOf
浏览 1
提问于2011-10-13
得票数 3
1
回答
如何让solverstudio (纸浆和cbc)在不可行
的
情况下报告冲突
约束
?
pulp
如何
使
求解
器
报告出冲突
约束
?谢谢。
浏览 3
提问于2017-05-09
得票数 1
1
回答
从C/C++调用Prolog时将事实传递给Prolog(不使用assert)
c++
、
prolog
我已经用Prolog编写了
约束
求解
逻辑,但是代码解析和
约束
生成是在C++前端进行
的
。因此,我想从C++调用Prolog,我目前正在通过SWI-Prolog API执行此操作。我需要提供Prolog
求解
器
关于解析
的
代码(例如,变量名)
的
事实,以及为它生成
的
约束
来
求解
它们。现在,我通过Prolog调用assert(fact) (首先在C++
求解
器
中将这些谓词声明为动态
浏览 1
提问于2014-04-09
得票数 3
1
回答
如何使用c++为z3中已有的声明函数添加新
的
约束
?
z3
我想知道有什么方法可以在不获取模型
的
情况下为
求解
器
中现有的声明变量添加一些新
的
约束
。(declare-fun k!647 () (_ BitVec 8))我怎么才能得到他们一般声明
的
名字呢? 情况是,我想为现有的“变量?”添加更多
的
约束
。在
约束
中,并一起
求解
它们。然后形成新
的
约束
,这
浏览 18
提问于2019-07-08
得票数 0
1
回答
OptaPlanner (
约束
求解
器
)在Node.JS中
的
替代方案
javascript
、
node.js
、
constraints
、
optaplanner
干杯社区,是否有人有在NodeJs环境中使用
约束
求解
器
的
经验,或者对时间表有经验?目前
的
限制是: 谢谢你
的
帮忙!
浏览 4
提问于2022-04-01
得票数 0
回答已采纳
1
回答
二维点间距离参数化
的
有效方法
algorithm
、
drawing
、
vertices
、
cad
、
parameterization
我们一直在开发一个小
的
简单
的
"CAD“解决方案,
使
我们可以参数化一些特定
的
,简单
的
形状
的
宽度和长度。 我们已经对如何处理这个问题进行了严格
的
讨论。 维护所有顶点之间所有关系
的
方程列表。假设我们有点A,B,C。让W是某个用户定义
的
浏览 3
提问于2017-08-18
得票数 0
回答已采纳
1
回答
fmincon中目标函数和
约束
函数
的
单次计算
matlab
、
optimization
、
differential-equations
在我
的
程序中,我需要在优化程序中
求解
一个边值问题,它也有非线性
约束
。用fmincon
求解
问题,需要用BVP
的
解来求目标函数和非线性
约束
函数。 目前,我正在
求解
目标函数和
约束
函数中
的
BVP。在对目标函数中
的
BVP进行一次评价后,是否有一种更有效
的
方法,通过对
约束
函数
的
求解
来减少另一次BVP
的
评价。任何想法
浏览 1
提问于2017-01-06
得票数 0
回答已采纳
2
回答
android studio SDK工具中"ConstraintLayout for android“和"Solver for ConstraintLayout”
的
区别
android
、
android-sdk-tools
、
android-constraintlayout
截图如下: 这两个选项之间
的
区别是什么?
浏览 1
提问于2017-04-12
得票数 14
1
回答
SciPy最小化函数
的
圆形/径向界限
python
、
python-3.x
、
optimization
、
scipy
我正在尝试使用优化子模块中
的
SciPy最小化函数来优化x-y平面中距原点0.15半径范围内
的
曲面方程。minimize(minimum_objective_3d, (.10,.10), args=(args), bounds=[(-.150,.150),(-.150,.150)]) 我知道我正在使用
的
边界参数指定了操作
的
矩形边界我
的
问题是。有没有办法将这些边界指定为以原点为中心
的
圆形半径? 提前感谢你
的
帮助。
浏览 4
提问于2021-03-28
得票数 0
1
回答
Proc Optmodel MILP
求解
器
,如何查找不可行
约束
sas
我正在使用MILP
求解
器
,并且一次又一次地陷入不可行解。当预解算
器
不能得到冲突
的
约束
时,问题就发生了,我在日志中得不到任何关于去哪里和做编辑
的
信息,并且在1000个
约束
中找出它是一个漫长而乏味
的
过程。 如果有办法在
求解
运行后识别不可行
的
约束
,请告知。我试过使用IIS选项,它不适用于MILP
求解
器
,PRESTOL选项可以得到即使是最轻微
的
不可行<e
浏览 2
提问于2017-03-29
得票数 0
1
回答
Gurobi Python敏感性分析日志文件
python
、
optimization
、
linear-programming
、
gurobi
、
pulp
我正在用Gurobi / PuLP解决一个线性规划,我想从
求解
器
中访问额外
的
日志-至少知道哪些
约束
对解决方案
的
约束
最大,或者在这种情况下,哪些
约束
使
我
的
问题变得不可行。
浏览 2
提问于2017-05-02
得票数 0
点击加载更多
扫码
添加站长 进交流群
领取专属
10元无门槛券
手把手带您无忧上云
相关
资讯
Simulink求解器的使用
小改进,大飞跃:深度学习中的最小牛顿求解器
Z3Py在CTF逆向中的运用
Ansys Mechanical | 软件介绍:业界一流的有限元求解器
汽车断面设计软件-SuperSection简介
热门
标签
更多标签
云服务器
ICP备案
实时音视频
即时通信 IM
对象存储
活动推荐
运营活动
广告
关闭
领券