标签: constraint-programming

任何或多或少的实用编程语言和编译器都必须处理约束.最常见的约束是类型.通常,类型推导和统一是通过简单的算法(例如Hindley-Milner)完成的,其中最终程序中的所有项都被赋予唯一类型.如果没有发生,则会出现错误指示.

在编译器中可能存在更复杂的约束,其中完全统一是不可能的,并且解决方案仅在某些限制下存在.可能的例子是

• 数据流分析.仿射相等约束的解可以用于循环矢量化.

• 内存管理.如果我们对引用和数据访问模式有一些约束,编译器可以从优化引用计数和垃圾收集中受益.

从另一点来看,约束求解器(如Z3或Yices)在为不同类型的约束寻找可满足的模型方面非常强大.

我正在寻找有关编译器如何从SMT求解器的强大功能以及他们正在解决的任务类型中受益的成功案例.我列出了一些区域,但我没有找到任何具体的例子.你能建议吗？

我对Choco和CP完全不熟悉,但是我正在制作一个小模型来解决Steiner树问题,而Choco一直强迫第一个节点无论图形是什么(并且它不正确,我检查过).

我有一个esIntVar 数组,如果边缘在解决方案中== 1,否则== 0.对于vs设置顶点的数组也是如此.我使用数组activeEdgeW能够有一个标量约束,其中coeffs是可变的.然后我只有通道约束,树约束和sum == w约束.并尽量减少w.相当简单,但由于某种原因vs[0] == true总是,任何图形.

我的模型老实说非常简单,我真的不知道它来自哪里:

    s = new Solver("Solver");
    vs = VF.boolArray("vs", nbV, s);
    es = VF.boolArray("es", nbE, s);
    w = VF.integer("w", 0, maxW, s);

    IntVar[] activeEdgeW = new IntVar[nbE];
    for(int i = 0; i < nbE; i++) { 
        activeEdgeW[i] = VF.enumerated("activeEdgeW["+i+"]", new int[]{0,ws[i]}, s); //Weight is either 0 or ws[i]
        ICF.arithm(activeEdgeW[i], "=", ws[i]).reifyWith(es[i]); //weight of edge is ws[i] if edge is in, 0 otherwise
    }


    UndirectedGraph …

我正在尝试使用loco进行优化的基本示例.

我有一个成本向量,其索引对应于多个时隙的整数值,并希望最小化时隙的不同子集的成本之和.

请参阅下面的我的尝试,但由于所选插槽与成本之间没有"链接",因此无效.

(def costs [10 10 20 20 30 30 40 40 10 10])

(let [slot-vars (for [i (range 5)] ($in [:slot i] 1 10))
      cost-vars (for [i (range 10)] ($in [:cost i] 10 40))]
  (solution
   (concat
    slot-vars
    cost-vars
    [($distinct (for [i (range 5)] [:slot i]))]
    (for [i (range 5)]
      ($= [:cost i] (get costs i))))
   :minimize (apply $+ (for [i (range 5)] [:slot i]))))

我有一个非常简单的方程，我希望能够在序言中解决：

A = B + C

我希望能够编写一个表达这种关系的谓词，它可以处理任何一个未被实例化的参数。无需推广到更复杂的关系或方程。

myEquation(A, B, C) :-
...something...

我可以使用以下语义调用：

myEquation(A,1,2).
>    A = 3.
myEquation(3,B,2).
>    B = 1.
myEquation(3,1,C).
>    C = 2.

有任何想法吗？使用算术运算符会产生很多“参数未充分实例化”的错误。看起来求解任意方程组超出了大多数 prolog 实现的范围，但我希望这个极其简单的方程易于处理。

我正在构思一个名为multi-sudoku的数独变种的解算器,其中多个板重叠如下:

如果我正确理解游戏,您必须以这样的方式解决每个网格,即任何两个或更多网格之间的重叠是每个网格解决方案的一部分.

我不确定我应该怎么想这个.任何人都有任何提示/概念线索？此外,如果想到人工智能中的任何主题,我也想听听.

我之前曾问过这个问题,并希望继续跟进,因为我尝试了其他一些事情并且他们没有完全解决问题.

我本质上是在尝试优化R中的NLP类型问题,它具有二进制和整数约束.相同的代码如下:

# Input Data
DTM <- sample(1:30,10,replace=T)
DIM <- rep(30,10)
Price <- 100 - seq(0.4,1,length.out=10)

# Variables that shall be changed to find optimal solution
Hike <- c(1,0,0,1,0,0,0,0,0,1)
Position <- c(0,1,-2,1,0,0,0,0,0,0)

# Bounds for Hikes/Positions
HikeLB <- rep(0,10)
HikeUB <- rep(1,10)
PositionLB <- rep(-2,10)
PositionUB <- rep(2,10)

library(Rsolnp)

# x <- c(Hike, Position)
# Combining two arrays into one since I want 
# to optimize using both these variables

opt_func <- function(x) {

  Hike <- head(x,length(x)/2)
  Position …

该MiniZinc约束求解器允许表达基数约束很容易使用内置的sum()功能：

%  This predicate is true, iff 2 of the array
%  elements are true
predicate exactly_two_sum(array[int] of var bool: x) =
    (sum(x) == 2);

满足基数约束，当且仅当布尔变量数组中的真实元素的数量符合指定。布尔值自动映射到整数值0并1计算总和。

我将自己的基数约束谓词实现为一组计数器切片：

%  This predicate is true, iff 2 of the array
%  elements are true
predicate exactly_two_serial(array[int] of var bool: x) =
    let 
    {
      int: lb = min(index_set(x));
      int: ub = max(index_set(x));
      int: len = length(x);
    }
    in
    if len < 2 then
      false …

我有一个系统,我需要计算每个变量的可能值范围(我不需要找到系统的解决方案).以下是示例系统的说明:

每条蓝线都是一个节点(由它上面的标签命名),灰线是节点之间的边缘.给出了初始约束:例如,边缘BC可以是0和1之间的任何实数,并且边缘BE可以是大于或等于9的任何数.节点不能跨越其他节点.将它们想象成可以伸展和缩回的金属条是有帮助的,推动蓝色板周围.

我的目标是为每条边计算它们的最小和最大长度.起始约束设置了系统,但最终结果可能比它们更受限制.例如,边缘DF的起始最小值/最大值为(2,∞),但是你可以看到它实际上不能短于3,因为收缩它将D拉入E,E拉向F,而EF有一个至少为3.最终的结果就是这个,我相信:

需要注意的是,我需要一种可以扩展到数十万个节点的算法,这个节点比这个例子更密集.它不能以指数方式增加运行时间,因为我还必须运行这个算法数十万次.

我尝试了一种方法,它给出了一些更多约束值,但不是最受约束的值.为了使方法可视化,我基本上尽可能地将所有板拉到左边,然后记录每个板的最大位置.然后我做了同样的事情,将它们拉到右边.然后,对于每个边,我只是找到每个板的值之间的差异.此方法非常有效地找到最大值,但问题是当您遇到类似于此示例的情况时,其中CD被BC和DE"锁定"到BE.它不能是6,因为系统只允许它比9短.我需要一种方法来找到真正的最小值7.我的方法不捕获"锁定"关系:当你拉C全部在左边的路上,BC是0,当你把D一直拉到右边时,DE是0,但如果CD是6,它们不能都是0.

在这个例子中,很容易看出CD受到BE的约束,但在实践中,系统会比例子更密集和更大,并且发现这种情况似乎并非易事.如果该方法涉及在本地搜索它,我担心它会扩展得很差,但这可能是唯一的方法.

如果将其建模为线性规划问题(AB + BC = AC,AB> 1等),则可能会利用该系统的某些属性:约束的所有系数均为1,并且约束中只有加法和减法.

有没有人对如何解决这个问题有任何建议？或者对我应该实际希望的运行时间复杂程度有任何见解？谢谢!

我正在重新使用 Google 的 OR 工具并尝试（相对）简单的优化。我正在使用 CP SAT 求解器，但我可能在这里遗漏了一些基本内容。我有一些变量 x、y 和一些常量 c。如果 y 小于 c，我希望 x 等于 1，否则等于 0。

from ortools.sat.python import cp_model

solver = cp_model.CpSolver()
model = cp_model.CpModel()
c = 50
x = model.NewBoolVar(name='x')
y = model.NewIntVar(name='y', lb=0, ub=2**10)

model.Add(x == (y < c))

model.Maximize(x+y)

status = solver.Solve(model)

我收到一条错误消息

TypeError: bad operand type for unary -: 'BoundedLinearExpression'

看来我在这里滥用 OR 工具语法来限制我的约束。我很难理解在线 OR 工具的文档，而且我似乎忘记的东西比我想象的要多得多。

我需要找到所有 16 位数字 ( x, y, z) 的三元组（实际上只有在不同三元组中与相同位置的位完美匹配的位），这样

y | x = 0x49ab
(y >> 2) ^ x = 0x530b
(z >> 1) & y = 0x0883
(x << 2) | z = 0x1787

直接使用 8700K 的策略需要大约 2 天，这太多了（即使我会使用我可以访问的所有 PC（R5-3600、i3-2100、i7-8700K、R5-4500U、3xRPi4、RPi0/W）这将花费太多时间）。

如果位移位不在等式中，那么这样做将是微不足道的，但是使用位移位很难做同样的事情（甚至可能是不可能的）。

所以我想出了一个非常有趣的解决方案：将方程解析为关于数字位的语句（类似于“x XOR 的第 3 位 XOR y 的第 1 位等于 1”），并且所有这些语句都用 Prolog 语言之类的语言编写（或只是解释他们使用真值表操作）执行所有明确的位将被发现。这个解决方案也很困难：我不知道如何编写这样的解析器，也没有 Prolog 的经验。(*)

所以问题是：这样做的最佳方法是什么？如果是 (*) 那么怎么做呢？

编辑：为了更容易在此处编码数字的二进制模式：

0x49ab = 0b0100100110101011
0x530b = 0b0101001100001011
0x0883 = 0b0000100010000011
0x1787 = 0b0001011110000111