Issues with .Mul operator for constraints.

[jbum]

Here is sample code for a KenKen solver that I'm working on.

https://gist.github.com/jbum/796dc1c808475eae7f7f9b01fa8d0537

More info about this puzzle: https://en.wikipedia.org/wiki/KenKen

Two issues.

1) Ideally, I'd like to see a Product() method which is the analogue to the Sum() method, (or a lambda comprehension) This would be useful for setting up clues in KenKens that involve multiplication. Since this doesn't exist, I'm doing explicit multiplications, based on the number of cells in the cage:

      ls = len(cage)
      if ls == 2:
        model += (cage[0] * cage[1]) == res
      elif ls == 3:
        model += (cage[0] * cage[1] * cage[2]) == res
      elif ls == 4:
        model += (cage[0] * cage[1] * cage[2] * cage[3]) == res
     # etc...

However this is not working as expected. When the code is included, the solver fails to solve the puzzle. When the code for the multiply operator is omitted, the solver finds multiple solutions (as I would expect), which leads me to believe it is only the multiply operator that is causing problems.

This is all with Mistral. When I use MiniSat, I get multiple solutions. These are known valid puzzles with a single solution.

[ehebrard]

Hi Jim,

Can you please try Mistral2 and let us know if you get the expected result? Mistral is no longer maintained, and the mul constraint is buggy (I'll make it raise some exception).

Cheers,

[jbum]

Mistral2 is solving the first 4 and then segfaults on the last one. There was a bug in the way I was handling division. It's fixed here.

https://gist.github.com/jbum/d5ce6a4b7f9de959d768305a4d67d6a9

Thread 0 Crashed:: Dispatch queue: com.apple.main-thread
0   _Mistral2.so                   0x0000000106e60449 Mistral::Solver::restore() + 41
1   _Mistral2.so                   0x0000000106e5edc8 Mistral::Solver::restore(int) + 40
2   _Mistral2.so                   0x0000000106de2a7a _wrap_Mistral2Solver_reset(_object*, _object*) + 54
3   org.python.python             0x00000001069f692b PyEval_EvalFrameEx +14229
4   org.python.python             0x00000001069f967d fast_function + 262
5   org.python.python             0x00000001069f6505 PyEval_EvalFrameEx + 13167
6   org.python.python             0x00000001069f2f64 PyEval_EvalCodeEx + 1387
7   org.python.python             0x00000001069f95ec fast_function + 117
8   org.python.python             0x00000001069f6505 PyEval_EvalFrameEx + 13167
9   org.python.python             0x00000001069f967d fast_function + 262
10  org.python.python             0x00000001069f6505 PyEval_EvalFrameEx + 13167
11  org.python.python             0x00000001069f2f64 PyEval_EvalCodeEx + 1387
12  org.python.python             0x00000001069f29f3 PyEval_EvalCode + 54
13  org.python.python             0x0000000106a129e2 run_mod + 53
14  org.python.python             0x0000000106a12a85 PyRun_FileExFlags + 133
15  org.python.python             0x0000000106a125c5 PyRun_SimpleFileExFlags + 711
16  org.python.python             0x0000000106a23e81 Py_Main + 3057
17  libdyld.dylib                 0x00007fff912015c9 start + 1

MiniSat is almost working, but it appears to be generating multiple solutions (the subsequent call to solver.getNextSolution() returns SAT, however the solution is identical to the first one). Mistral2 does not return SAT when I'm checking for extra solutions.

On Tue, May 24, 2016 at 12:06 PM, ehebrard notifications@github.com wrote:

Hi Jim,

Can you please try Mistral2 and let us know if you get the expected result? Mistral is no longer maintained, and the mul constraint is buggy (I'll make it raise some exception).

Cheers,

— You are receiving this because you authored the thread. Reply to this email directly or view it on GitHub https://github.com/eomahony/Numberjack/issues/42#issuecomment-221368059

[jbum]

I've got a few more puzzle varieties that are generating spurious multiple solutions in Mistral as well. I think this is operator error - I need a canonical example of iterating through solutions (ideally that doesn't do extra work, so I can bail after 2 solutions).

[ehebrard]

The two bugs on Mistral2 (multiple solutions and seg-fault) should be fixed now. Thank you for the feedback!

[jbum]

Cool! It's doing much better, and solves those particular puzzles now.

On a larger test suite I found a few more puzzles that trigger errors, three of which I've included in this modified code (see comments next to puzzles):

https://gist.github.com/jbum/b35f1a79d95b89c3bb0cf3d6a9fe5e46

Failure messages look like this:

Error: solution does not satisfy c58: x65 == (x22 * 3) 1 5 (backtracking)

On Wed, May 25, 2016 at 5:49 AM, ehebrard notifications@github.com wrote:

The two bugs on Mistral2 (multiple solutions and seg-fault) should be fixed now. Thank you for the feedback!

— You are receiving this because you authored the thread. Reply to this email directly or view it on GitHub https://github.com/eomahony/Numberjack/issues/42#issuecomment-221565318

[jbum]

Also note that MiniSat produces false multiple solutions on this test.

[ehebrard]

The buggy constant factor constraint is fixed.

About MiniSat, perhaps Barry you might have an idea? I quickly checked and getNextSolution() is not implemented for MiniSat as far as I see! I guess it must raise an exception that is caught without exit or something.

There is a branch_right() method, but I don't think it is the best way to implement getNextSolution() with MiniSat.

[jbum]

Sweet!

FYI A few warnings that show up when I build:

_Numberjack/solvers/Mistral2/mistral/src/lib/mistral_scheduler.cpp:2160:20: _warning: comparison of constant 0 with expression of type 'bool' is always false

• [-Wtautological-constant-out-of-range-compare]*
  
  Outcome result = (IS_OK(propagate()) ? UNKNOWN : UNSAT);

•                    ^~~~~~~~~~~~~~~~~~*

_Numberjack/solvers/Mistral2/mistral/src/include/mistral_global.hpp:364:20: _note: expanded from macro 'IS_OK'

define IS_OK(o) (o<0)

And this error, which prevents Toulbar2 from building on OSX.

_Numberjack/solvers/Toulbar2/include/tb2system.hpp:94:47: _error: use of undeclared identifier 'exp10l'

    inline Double Exp10(Double x) {return exp10l(x);}

On Thu, May 26, 2016 at 9:19 AM, ehebrard notifications@github.com wrote:

The buggy constant factor constraint is fixed.

About MiniSat, perhaps Barry you might have an idea? I quickly checked and getNextSolution() is not implemented for MiniSat as far as I see! I guess it must raise an exception that is caught without exit or something.

There is a branch_right() method, but I don't think it is the best way to implement getNextSolution() with MiniSat.

— You are receiving this because you authored the thread. Reply to this email directly or view it on GitHub https://github.com/eomahony/Numberjack/issues/42#issuecomment-221920726

[jbum]

I found 3 more puzzles that are still triggering the same type of error in Mistral2, you can paste these into the test_puzzles list in the above code:

(6,"ABCDDEABCCFEGGHIFJKKHILJMNOOLPMNQQLP;5+,2-,16*,1-,2/,2/,4*,7+,8+,2-,3/,8*,6+,24*,6*,2-,1-","234651351462412536625314546123163245"), # easy boom
(6,"ABBCDEAFGCDEHFGIJKHLMIJKNLMOOPNQQRRP;6*,2/,1-,3/,9+,15*,2/,10*,2/,24*,9+,3-,9+,1-,4-,2/,1-,5+","124635632514251463513246346152465321"), # med boom
(6,"ABBCDEAFFCDEGHIJJKGHILMKNHILMONPPPMO;3-,3-,1-,3/,24*,5+,4*,13+,10+,8+,2/,2/,48*,2/,2-,20*","214536532614426351153462361245645123"), # hard boom

(FYI, I'm working on 10 additional puzzle varieties for the example folder, will submit these today...)

[ehebrard]

I can't reproduce the bug here, I get correct answers on all three.

Though I too cannot compile Toulbar, Barry, does Simon receive these emails? Also, if you can try the puzzles above with Mistral2 and let me know what you see, that would be great!

Cheers,

[9thbit]

I believe Simon does but I have just pushed a fix to compile Toulbar2. I'll take a look into the other bug now.

[9thbit]

Hi @jbum, I've added support for enumerating multiple/all solutions with MiniSat and added an example in the examples for this too. I've also added a Product predicate which is just syntactic sugar for what you're looking for in your examples.

I didn't spot any other bugs with the code you sent there, let us know if there are more.

[jbum]

Sweet - will tweak my KenKen, and Cryptic KenKen examples :)

On Fri, May 27, 2016 at 6:42 AM, Barry Hurley notifications@github.com wrote:

Hi @jbum https://github.com/jbum, I've added support for enumerating multiple/all solutions with MiniSat and added an example in the examples for this too. I've also added a Product predicate which is just syntactic sugar for what you're looking for in your examples.

I didn't spot any other bugs with the code you sent there, let us know if there are more.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/eomahony/Numberjack/issues/42#issuecomment-222149473, or mute the thread https://github.com/notifications/unsubscribe/AARk6fG9PNRkQQCeq6SEfSts_laAHETIks5qFvS8gaJpZM4IlvEW .

[jbum]

testInkies.zip

I'm having some issues with puzzles not solving when I run through large test suite, but when I isolate the puzzles, they solve okay. The attached archive contains a number of large test suites of valid KenKen (Inky) puzzles, and a solver for them. You may find these large suites useful for performance testing / profiling.

$ python testInkies_nj.py inkies_6KX.txt -s Mistral2 There are 4 puzzles that fail to solve for me. If I paste them into the KenKen solver, which is essentially the same but has embedded puzzles, they solve.

(example modified KenKen solver) https://gist.github.com/jbum/4b39259edd3dc903e0243d76cd125502

$ python testInkies_nj.py inkies_6E.txt -s Mistral2 This one produces the constraint problem from above (on a Mac). The puzzles that have this problem DO fail in the above KenKen solver on my mac.

[jbum]

The most recent Mistral2 updates have fixed the previous constraint issues. Sweet! (MiniSat is segfaulting, tho...)