Strange core.logic behavior

[Mauro Lopes]

Hello everyone,

I am new to core.logic but have been using it for the past few days (version 0.8.7).

I have found a behavior that seems strange to me. I have written a search (run*) that does not always return the same set of results if I run it a few times with the same input. Not even the number of results is the same. Can that somehow be the right thing to expect? Maybe I have misunderstood some basic concept, so please clarify what is going on.

I have simplified my program to the minimum version I could find that still shows this behavior. Here is the gist:

gist.github.com/maurolopes/9163407

Thanks!

[David Nolen]

Sounds like a bug, please file a bug in JIRA with this code and I will take a look. Thanks!

David

--
You received this message because you are subscribed to the Google Groups "minikanren" group.
To unsubscribe from this group and stop receiving emails from it, send an email to minikanren+...@googlegroups.com.
To post to this group, send email to minik...@googlegroups.com.
Visit this group at http://groups.google.com/group/minikanren.
For more options, visit https://groups.google.com/groups/opt_out.

[Mauro Lopes]

Done. Ticket is at http://dev.clojure.org/jira/browse/LOGIC-156

Thanks, David.

[David Nolen]

So I took a closer look at this and noticed that you're not using fd/in in all the locations where you create fresh vars and then apply finite domain operation on them. This is not correct.

Can you fix your code and then let us know if the problem continues to persist?

Thanks,

David

[Mauro Lopes]

Sure. I have added fd/in for all vars involved in fd operations and the problem persists. I uploaded the new code to JIRA. See if it helps. Thanks.

Regards,

Mauro

[David Nolen]

Thanks I can confirm. I'm assuming the case where you get 5 results in the set is simply not correct?

David

[Mauro Lopes]

Actually what I desire to get as a result is only the first three solutions:

#{(0 1 1 0) (1 1 0 0) (0 0 1 1)}

I noticed that, in order to get this solution, I can just replace

([[] vars])

with

([[] vars]

    (l/everyg #(l/== % 0) vars))

and it seems to work fine for my program, and I agree that this change is necessary for it to work as intended.

Anyway, without this change, what I really think it should return is:

#{(0 1 1 0) (1 1 0 0) (0 0 1 1) (1 1 1 0) (1 1 0 1) (1 1 1 1) (0 1 1 1)}

So, in my opinion, both of the solutions (4 or 5 results) are incorrect, core.logic is adding a few extra results and missing others.

--
You received this message because you are subscribed to a topic in the Google Groups "minikanren" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/minikanren/fjL-vGpwK6g/unsubscribe.
To unsubscribe from this group and all its topics, send an email to minikanren+...@googlegroups.com.

[David Nolen]

Which results are making it through that you don't think should?

Just trying to figure out what the main part of your program is doing. sumo and dropo appear to be just fine by themselves.

David

[Mauro Lopes]

(1 0 0 1) and (0 1 0 1) are wrong for me.

The idea is that, say, (f 8 [2 3]) should give me all ways of putting two sequences of ones (with sizes 2 and 3, in this order), separated by some zeros, in an 8-length row.

It is like solving a one-row nonogram. Then I just use it for all rows and columns to make a full nonogram solver:

http://github.com/maurolopes/nonogramsolver

As I said, my program seems to be working now. I'm only giving you context so it is easier to understand my code and debug core.logic.

[David Nolen]

On Thu, Mar 6, 2014 at 12:10 PM, Mauro Lopes <mauro...@gmail.com> wrote:

(1 0 0 1) and (0 1 0 1) are wrong for me.

But which portion of your program should disallow this? If I can identify that it will be much simpler for me to determine the flaw in core.logic's FD functionality. I've encountered bugs like this in the past - they almost always boil down to some subtle problem around logic var aliasing. We have a bunch of tests to check for this but it looks like you've come across a case I've missed.

Thanks,

David

[Mauro Lopes]

I see.

The only clause that adds a 1 to the solution is in line 26. It takes the first number (in the example, n=2), takes the first n vars (line 34) and force their sum to be n, making all of them equal to 1. So there is no way to have a solution starting with (1 0)

--

[Mauro Lopes]

Oops, sorry for the wrong line numbers. I opened the old version of the file (the one before those extra fd/in).

[Mauro Lopes]

So, the only clause that adds a 1 to the solution is ([[n . ns] vars] ...). It takes the first number (in the example, n=2), takes the first n vars using dropo, and forces their sum to be n.

[David Nolen]

Ok but what logic disallows the results that you don't think should be in there? I'm assuming something in your program prevents (1 0 0 1)?

David

On Thu, Mar 6, 2014 at 11:56 AM, Mauro Lopes <mauro...@gmail.com> wrote:

[Mauro Lopes]

Well, I've just noticed that the version we are using has some clauses removed. See the last clause of solve-row in

http://github.com/maurolopes/nonogramsolver/blob/master/src/nonogramsolver/core.clj

The idea is that, whenever a var becomes 0, the sum of all the remaining vars have to be equal to the sum of the remaining numbers. So, in (1 0 0 1), when the second var becomes zero, the sum of the last two must be equal to 0, which is not the case.

Also, I suspect there is some error in my code, since in this case there should be no 1 followed by 0.

Sorry for the confusion. When reporting the problem to the list, I removed all the clauses I could to make the example minimal, hoping it would make debugging easier. The only problem is that it made the expected results no longer the same. But the problem still exists.

[Mauro Lopes]

When you asked what result I expected, I have answered regarding my whole program, and I think this has created this confusion. I should have focused on the gist only. Sorry for that.

Considering this, I think the correct answer is the one with 5 results in the set. I think all five of them satisfy the constraints. Do you think (1 0 0 1) does not satisfy?

[David Nolen]

OK this is informative :) The bug in your program is helping me find a bug in core.logic :)

David

--

You received this message because you are subscribed to the Google Groups "minikanren" group.
To unsubscribe from this group and stop receiving emails from it, send an email to minikanren+...@googlegroups.com.
To post to this group, send email to minik...@googlegroups.com.
Visit this group at http://groups.google.com/group/minikanren.

For more options, visit https://groups.google.com/d/optout.