core.logic

OOM when setting (interval 1 2) for 20 logic vars

Details

  • Type: Defect Defect
  • Status: Closed Closed
  • Priority: Major Major
  • Resolution: Completed
  • Affects Version/s: None
  • Fix Version/s: None
  • Component/s: None
  • Labels:
    None
  • Environment:
    Clojure 1.5.1, both 0.8.3 and 0.8.4--994a7a3

    Running on a 1GB VM.

Description

The following two programs (presumably equivalent) both give me OOM (heap space):

(let [vs (repeatedly 20 l/lvar)]
  (l/run 1 [q]
     (l/== q vs)
     (l/everyg (fn [v] (fd/in v (fd/interval 1 2))) vs)))
(l/run 1 [q]
         (l/fresh [x1 x2 x3 x4 x5 x6 x7 x8 x9
                   x10 x11 x12 x13 x14 x15
                   x16 x17 x18 x19 x20]
                  (l/== q [x1 x2 x3 x4 x5 x6 x7 x8 x9
                           x10 x11 x12 x13 x14 x15
                           x16 x17 x18 x19 x20])
                  (fd/in x1 x2 x3 x4 x5 x6 x7 x8 x9
                         x10 x11 x12 x13 x14 x15
                         x16 x17 x18 x19 x20
                         (fd/interval 1 2))))

I assume the expected value is something like ([1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1]).

Activity

Hide
David Nolen added a comment - - edited

We got another report about this issue. Consider:

(let [vs (into [] (take 17 (repeatedly lvar)))]
  (doall
    (run 1 [q]
      (== q vs)
      (everyg #(fd/in % (fd/interval 60 69)) vs))))

The behavior seems exponential in N, currently here at 17, but on my Macbook Air going to 20 results in hanging my REPL.

Show
David Nolen added a comment - - edited We got another report about this issue. Consider:
(let [vs (into [] (take 17 (repeatedly lvar)))]
  (doall
    (run 1 [q]
      (== q vs)
      (everyg #(fd/in % (fd/interval 60 69)) vs))))
The behavior seems exponential in N, currently here at 17, but on my Macbook Air going to 20 results in hanging my REPL.
Hide
Gary Fredericks added a comment -

It looks like this has nothing to do with domains actually. I get the same effect with the following:

(let [vs (repeatedly 16 lvar)]
  (run 1 [q]
       (everyg #(conde [(== % 1)] [(== % 2)]) vs)
       (== q vs)))
Show
Gary Fredericks added a comment - It looks like this has nothing to do with domains actually. I get the same effect with the following:
(let [vs (repeatedly 16 lvar)]
  (run 1 [q]
       (everyg #(conde [(== % 1)] [(== % 2)]) vs)
       (== q vs)))
Hide
David Nolen added a comment -

Thanks for the extra details!

Show
David Nolen added a comment - Thanks for the extra details!
Hide
Gary Fredericks added a comment -

In hindsight this seems obvious.

I think it must follow directly from the breadth-first-search approach ensured by conde's interleaving.

If the expression in my previous comment creates a binary tree of depth 16, and the single answer we want is in the leftmost leaf, we still can't get to that leaf before searching through the entire tree (breadth first), which means having the whole thing in memory in some sense, which means OOM whenever the tree isn't too small.

I assume this is a fundamentally difficult problem. Should this still be considered a bug?

Show
Gary Fredericks added a comment - In hindsight this seems obvious. I think it must follow directly from the breadth-first-search approach ensured by conde's interleaving. If the expression in my previous comment creates a binary tree of depth 16, and the single answer we want is in the leftmost leaf, we still can't get to that leaf before searching through the entire tree (breadth first), which means having the whole thing in memory in some sense, which means OOM whenever the tree isn't too small. I assume this is a fundamentally difficult problem. Should this still be considered a bug?
Hide
David Nolen added a comment -

`conde` isn't bread-first, it's interleaving. I will need to think about it some more. I'm mostly concerned with the FD case because we rely on `map-sum` which uses `conde`, perhaps there's something clever we can do for domain enumeration?

Show
David Nolen added a comment - `conde` isn't bread-first, it's interleaving. I will need to think about it some more. I'm mostly concerned with the FD case because we rely on `map-sum` which uses `conde`, perhaps there's something clever we can do for domain enumeration?
Hide
Gary Fredericks added a comment -

One thing that seems to clear up the issue but which could easily have subtle performance issues I don't understand is removing the -inc from conde. This clears up all the test cases given here, and the test suite still passes.

I don't think the -inc is necessary in the cases where we know that the goals are simple ones (like unification) that don't diverge. So another approach is to have a special goal for disjunctively unifying with a bunch of concrete values:

(defn ==any
  "Like membero, but requires that vals be a ground sequence, and probably                                                                                                                     
   performs better."
  [x vals]
  (fn [s]
    (if-let [[v & vs] (seq vals)]
      (choice (unify s x v)
              (fn []
                ((==any x vs) s))))))

Using this (like you would membero) instead of conde seems to clear it up, and could presumably be used instead of conde in map-sum.

What do you think? Is there anything in particular that should be investigated regarding this approach?

Show
Gary Fredericks added a comment - One thing that seems to clear up the issue but which could easily have subtle performance issues I don't understand is removing the -inc from conde. This clears up all the test cases given here, and the test suite still passes. I don't think the -inc is necessary in the cases where we know that the goals are simple ones (like unification) that don't diverge. So another approach is to have a special goal for disjunctively unifying with a bunch of concrete values:
(defn ==any
  "Like membero, but requires that vals be a ground sequence, and probably                                                                                                                     
   performs better."
  [x vals]
  (fn [s]
    (if-let [[v & vs] (seq vals)]
      (choice (unify s x v)
              (fn []
                ((==any x vs) s))))))
Using this (like you would membero) instead of conde seems to clear it up, and could presumably be used instead of conde in map-sum. What do you think? Is there anything in particular that should be investigated regarding this approach?
Hide
Gary Fredericks added a comment -

I just looked at the code that uses map-sum closer and realized I don't understand everything that's going on, so am not totally sure if/how ==any would fit there.

Show
Gary Fredericks added a comment - I just looked at the code that uses map-sum closer and realized I don't understand everything that's going on, so am not totally sure if/how ==any would fit there.
Hide
Gary Fredericks added a comment -

In playing around with it I realized the definition of ==any should not use choice directly but rather mplus, which should still have the same performance gain.

Then I was able to use the same technique inlined with map-sum, which gives:

(defn map-sum [f]
  (fn loop [ls]
    (if (empty? ls)
      (fn [a] nil)
      (fn [a]
        (mplus
         ((f (first ls)) a)
         (fn []
           ((loop (rest ls)) a)))))))

The tests pass, and the FD examples are fast.

I started a branch here: https://github.com/fredericksgary/core.logic/compare/LOGIC-137

Show
Gary Fredericks added a comment - In playing around with it I realized the definition of ==any should not use choice directly but rather mplus, which should still have the same performance gain. Then I was able to use the same technique inlined with map-sum, which gives:
(defn map-sum [f]
  (fn loop [ls]
    (if (empty? ls)
      (fn [a] nil)
      (fn [a]
        (mplus
         ((f (first ls)) a)
         (fn []
           ((loop (rest ls)) a)))))))
The tests pass, and the FD examples are fast. I started a branch here: https://github.com/fredericksgary/core.logic/compare/LOGIC-137
Hide
David Nolen added a comment -

Please attach a patch with the `map-sum` improvement. Thanks!

Show
David Nolen added a comment - Please attach a patch with the `map-sum` improvement. Thanks!
Hide
Gary Fredericks added a comment -

Attached patch with the altered map-sum.

Show
Gary Fredericks added a comment - Attached patch with the altered map-sum.

People

Vote (0)
Watch (0)

Dates

  • Created:
    Updated:
    Resolved: