<< Back to previous view

[LOGIC-137] OOM when setting (interval 1 2) for 20 logic vars Created: 11/May/13  Updated: 28/Jul/13  Resolved: 08/Jun/13

Status: Closed
Project: core.logic
Component/s: None
Affects Version/s: None
Fix Version/s: None

Type: Defect Priority: Major
Reporter: Gary Fredericks Assignee: David Nolen
Resolution: Completed Votes: 0
Labels: None
Environment:

Clojure 1.5.1, both 0.8.3 and 0.8.4--994a7a3

Running on a 1GB VM.


Attachments: Text File LOGIC-137.patch    

 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]).



 Comments   
Comment by David Nolen [ 31/May/13 11:49 AM ]

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.

Comment by Gary Fredericks [ 05/Jun/13 7:51 PM ]

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)))
Comment by David Nolen [ 05/Jun/13 8:09 PM ]

Thanks for the extra details!

Comment by Gary Fredericks [ 07/Jun/13 10:53 PM ]

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?

Comment by David Nolen [ 08/Jun/13 1:51 PM ]

`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?

Comment by Gary Fredericks [ 08/Jun/13 2:53 PM ]

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?

Comment by Gary Fredericks [ 08/Jun/13 3:05 PM ]

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.

Comment by Gary Fredericks [ 08/Jun/13 3:28 PM ]

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

Comment by David Nolen [ 08/Jun/13 5:21 PM ]

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

Comment by Gary Fredericks [ 08/Jun/13 6:03 PM ]

Attached patch with the altered map-sum.

Comment by David Nolen [ 08/Jun/13 8:30 PM ]

fixed http://github.com/clojure/core.logic/commit/5afeace2761eeb6731cf558bed354607e5401631

Generated at Sat Aug 23 06:41:06 CDT 2014 using JIRA 4.4#649-r158309.