Clojure core.logic CLP(FD), проецирующий переменные FD

Я работаю над наивным алгоритмом квадратной упаковки, используя библиотеку 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?

Спасибо!


person Pascal Chatterjee    schedule 27.04.2013    source источник


Ответы (1)


Да, вы не можете проектировать переменные конечного домена, которые не были ограничены одним значением. Я рекомендую просмотреть существующие решения вашей проблемы на Прологе, использующие CLP(FD). Очень может быть, что мы не поддерживаем достаточное количество ограничений, чтобы упростить формулировку этой проблемы — мы работаем над этим.

person dnolen    schedule 27.04.2013
comment
Потребуется форма устранения квантификатора, чтобы уменьшить количество ограничений, что не всегда возможно, когда домен бесконечен. Но никто не мешает вернуть решение с кванторами впереди. Если квантор является квантором существования, то его даже показывать не нужно, разве что иметь в виду возможный вариант исключения. Переменная может участвовать в устранении прямой константы, если она сама не помечена. Вот почему новые переменные Пролога, например введенные в рекурсивные предикаты с помощью CLP(FD), чаще всего работают. - person Mostowski Collapse; 26.03.2016