Clojure core.logic CLP(FD) 投影 FD 变量

Posted 2023-05-08

【中文标题】Clojure core.logic CLP(FD) 投影 FD 变量

【英文标题】：Clojure core.logic CLP(FD) projecting FD variables

【发布时间】：2013-04-21 13:15:38

【问题描述】：

我正在使用 Clojure 的 core.logic CLP(FD) 库（core.logic 版本 0.8.3）研究一种简单的平方打包算法。

正方形表示如下：

[[[x11 y11] [x12 y12]] 
 [[x21 y21] [x22 y22] ...]]

每个正方形都表示为其左上角和右下角的坐标。

坐标是FD变量，在一定的区间内。

我想将解的大小分别定义为离原点最近和最远的正方形的右上角和右下角之间的距离

(defne solution-size-o [size squares]
  ([s sqrs]
    (fresh [closest farthest 
            x11 y11 x22 y22 _1 _2]
    (closest-square   [[x11 y11] _1] sqrs)
    (farthest-square  [_2 [x22 y22]] sqrs)
    (project [x11 y11 x22 y22]
      (let [a (- y22 y11)
            b (- x22 x11)]
        (== s (-> (+ (* a a) (* b b)) Math/sqrt Math/ceil int)))))))

这似乎适用于纯整数：

(run 1 [q]
  (solution-size-o q [[[0 0] [1 1]] [[1 1] [2 2]]]))
=> (3)

即使是完全约束的 FD 变量

(defn constrained-solution-size []
  (run 1 [q] 
    (fresh [size x11 y11 
                 x12 y12 
                 x21 y21 
                 x22 y22 squares]
      (fd/in x11 y11 x12 y12 x21 y21 x22 y22 (fd/interval 0 2))
      (fd/eq 
        (= x11 0) (= y11 0) (= x21 1) (= y21 1)
        (= x12 (+ x11 1)) (= y12 (+ y11 1))
        (= x22 (+ x21 1)) (= y22 (+ y21 1)))
      (== squares [[[x11 y11] [x12 y12]] [[x21 y21] [x22 y22]]])
      (solution-size-o size squares)
      (== q :squares squares :size size))))

(constrained-solution-size)
=> (:squares [[[0 0] [1 1]] [[1 1] [2 2]]], :size 3)

但是当变量的域没有受到完全约束时，它似乎会中断。例如，如果我删除y21 = 1 的约束，这意味着y11 和y21 在它们的域中剩下多个值：

(defn unconstrained-solution-size []
  (run 1 [q] 
    (fresh [size x11 y11 
                 x12 y12 
                 x21 y21 
                 x22 y22 squares]
      (fd/in x11 y11 x12 y12 x21 y21 x22 y22 (fd/interval 0 2))
      (fd/eq 
        (= x11 0) (= y11 0) (= x21 1)
        (= x12 (+ x11 1)) (= y12 (+ y11 1))
        (= x22 (+ x21 1)) (= y22 (+ y21 1)))
      (== squares [[[x11 y11] [x12 y12]] [[x21 y21] [x22 y22]]])
      (solution-size-o size squares)
      (== q :squares squares :size size))))

我明白了

(unconstrained-solution-size)
=> ClassCastException clojure.core.logic.LVar cannot be cast to java.lang.Number     clojure.lang.Numbers.minus (Numbers.java:135)

似乎project 仅在其域受到完全约束时才对 FD 变量起作用。这是应该的吗？如果是，有人对如何对 FD 变量进行非关系运算有任何建议吗？

谢谢！

【参考方案1】：

是的，您不能投影未限制为单个值的有限域变量。我建议查看利用 CLP(FD) 在 Prolog 中解决问题的现有解决方案。很可能是我们不支持足够的约束来简化这个问题的表达——我们正在努力解决这个问题。

【讨论】：

需要一种形式的量词消除来减少约束的数量，这在域无限时并不总是可行的。但是没有人阻止返回一个前面有量词的解决方案。如果量词是一个存在量词，你甚至不需要显示它，除了记住可能的消除选项。当变量本身没有被标记时，它可以参与前向常数消除。这就是为什么新鲜的 Prolog 变量，例如在使用 CLP(FD) 的递归谓词中引入的变量，最常起作用的原因。