我正在尝试解决 Sympy 中的一些简单的布尔可满足性问题。在这里，我尝试解决包含逻辑运算符的约束Or：
from sympy import *
a,b = symbols("a b")
print(solve(Or(Eq(3, b*2), Eq(3, b*3))))
# In other words: (3 equals b*2) or (3 equals b*3)
# [1,3/2] was the answer that I expected
令人惊讶的是，这会导致错误：
TypeError: unsupported operand type(s) for -: 'Or' and 'int'
我可以使用 解决这个问题Piecewise，但这更加冗长：
from sympy import *
a,b = symbols("a b")
print(solve(Piecewise((Eq(3, b*2),Eq(3, b*2)), (Eq(3, b*3),Eq(3, b*3)))))
#prints [1,3/2], as expected
不幸的是，当我尝试求解两个变量而不是一个变量时，这种解决方法失败了：
from sympy import *
a,b = symbols("a b")
print(solve([Eq(a,3+b),Piecewise((Eq(b,3),Eq(b,3)), …我正在尝试使用 Minizinc 中的热启动注释来为模型提供已知的次优解决方案。
我首先尝试执行 Minizinc 文档（他们提供的唯一一个）中的这个热启动示例：
array[1..3] of var 0..10: x;
array[1..3] of var 0.0..10.5: xf;
var bool: b;
array[1..3] of var set of 5..9: xs;
constraint b+sum(x)==1;
constraint b+sum(xf)==2.4;
constraint 5==sum( [ card(xs[i]) | i in index_set(xs) ] );
solve
:: warm_start_array( [ %%% Can be on the upper level
warm_start( x, [<>,8,4] ), %%% Use <> for missing values
warm_start( xf, array1d(-5..-3, [5.6,<>,4.7] ) ),
warm_start( xs, array1d( -3..-2, [ 6..8, 5..7 ] ) )
] )
:: …我使用 Google OR Tools in Python 编写了一个约束编程模型，它使用 CP 求解器。我需要多次运行该模型，并且在每次运行中我都会修改约束。目前，每次我想运行模型时，我都会从头开始创建模型对象。无论如何，我可以修改现有模型的变量/约束，这样我就不需要每次都从头开始构建模型吗？
为了提供更好的上下文，请考虑以下示例模型。
from ortools.sat.python import cp_model
model = cp_model.CpModel()
num_vals = 3
a = model.NewIntVar(0, num_vals -1, 'a')
b = model.NewIntVar(0, num_vals -1, 'b')
c = model.NewIntVar(0, num_vals -1, 'c')
model.Add(a == b)
solver = cp_model.CpSolver()
solver.Solve(model)
现在，在问题的第二次运行中，我想做以下更改。
5a==ba==c在不从头开始构建模型的情况下如何实现这一目标？
python mathematical-optimization constraint-programming or-tools cp-sat
我是约束编程和 OR-Tools 的新手。关于问题的简要说明。有 8 个位置，对于每个位置，我需要决定应选择哪种类型 A (move_A) 的移动和类型 B (move_B) 的移动，以便从 2 个移动的组合（在每个位置）获得的值是最大化。（虽然这只是更大问题的一部分）。我想用AddElement方法来做子设置。
请看下面的尝试
from ortools.sat.python import cp_model
model = cp_model.CpModel()
# value achieved from combination of different moves of type A
# (moves_A (rows)) and different moves of type B (moves_B (columns))
# for e.g. 2nd move of type A and 3rd move of type B will give value = 2
value = [
[ -1, 5, 3, 2, 2],
[ 2, 4, 2, -1, 1],
[ …我正在探索 Google 的 Cp-SAT 来模拟特定类型的约束，如下所示：
约束：
变量 X 可以取值为 1、2 和 3
变量 Y 可以取值为 2、3 和 4
变量 Z 可以取值为 5、6 和 7
当变量 X 值为 1 时，则 Y 只能
取值为3 或 4当变量 Y 值为3，那么Z只能假设为7
给定变量 Y 值是 3 而 Z 值不是 7，找出 X 和 Z 的可能值。
我无法使用 Google 的 CP-SAT java 接口对此进行建模。任何人都可以帮忙吗？
我探索了以下示例，但仍然无法弄清楚：https : //github.com/google/or-tools/blob/stable/ortools/linear_solver/samples/LinearProgrammingExample.java
https://github.com/google/or-tools/blob/stable/ortools/linear_solver/samples/SimpleMipProgram.java
我想使用Choco 求解器编写一个 Java 程序，该程序生成满足许多约束的数学问题。问题必须采用以下形式：
x @ y ? z = r
在哪里：
x, y&z是正整数，彼此不一定不同，其中一个为 2 位数，另外两个为 1 位数
@&?是运算符 +、- 或 *（请注意，两者也可以代表同一个运算符）
? r是一位正整数
我想“按需”生成这些数学问题（例如，当时一个）并且它们需要随机化（即，生成的问题不应该没有模式或固定顺序）。
自从我做约束（满足）编程以来已经有 10 多年了，但我相信 C(S)P（最好通过 Choco 的方式）是一个适合在这里应用的工具。这是正确的，有人可以帮助我开始吗？