Alloy - Can't find unsat core

Question

I have a "No instance found" Alloy file, and would like to debug it. The docs say to go to Options and choose SAT Solver > unsat-core. Yet, I don't see that, only SAT4J.

I'm running the latest Alloy 4.2, just downloaded. When I ran it, there was a note about not supporting JNI. If I need to download a different configuration to see unsat core, please tell me how to do it. Otherwise, how do I debug the Alloy file?

That was the latest stable. I also just tried the latest experimental and had similar (not identical) results. Note this warning, though:

Alloy Analyzer 4.2_2015-02-22 (build date: 2015-02-22 18:21 EST)

Warning: JNI-based SAT solver does not work on this platform.
This is okay, since you can still use SAT4J as the solver.
For more information, please visit http://alloy.mit.edu/alloy4/
.

Warning: Alloy4 defaults to SAT4J since it is pure Java and very reliable.
For faster performance, go to Options menu and try another solver like MiniSat.
If these native solvers fail on your computer, remember to change back to SAT4J.

Answer 1

You see only SAT4J? Just a sanity check: you're clicking on the Options menu, and then on the line that reads Solver: SAT4J, right?

When you do that, you should get a submenu with a list of SAT solvers; on my system, it looks something like this:

I hope this helps. If it doesn't, I expect the next thing to ask is what build the About Alloy dialog box shows. (For comparison: the screen shot just given was produced by the build of 2014-05-16.)

[Postscript]

Ah. Right. Your experience is making clear what is meant by the remark in the documentation:

By default, the pure Java solver "SAT4J" is chosen since it runs on every platform and operating system. If you require faster performance, you can try one of the native solver such as MiniSat or ZChaff.

I infer from that (now) that solvers other than SAT4J are not all (or perhaps any of them) pure Java, but require a native interface (i.e. an interface to code written in other languages). If JNI doesn't work on your platform, as your warning message indicates, SAT4J may be the only solver available.

Perhaps someone from the development team can comment.

---

So if you can't switch to Unsat Core as a way to find why your model has no instances, you are thrown back on other methods.

One method is obvious (though kind of tedious): a binary search through the set of constraints in the model.

If you know what I mean, and can't think of a better approach, then so long and good luck.

If you know what I mean and can think of a better approach, please tell the rest of us what it is.

If you don't know what I mean, the method I have in mind resembles a widely used technique for finding syntax errors in a program when you have no idea where they are. (A dim memory tells me I may have learned this from reading Jon Bentley's Programming Pearls. Maybe.) Here is one way to do it.

1. Make a backup of the model in its current state. You'll need it later, when you start to wonder whether this or that tiny detail has changed or not.

2. Change all of your named facts to named predicates. (If it proves necessary, also change all of your signature facts, and even other constraints, to named predicates. I only do this when I have no alternative, since it requires rewriting more of the model than I would like.)

3. Make a new predicate ANDing together all of your named predicates. In what follows I'll call this AllTogetherNow. It will have a form something like

   pred AllTogetherNow {
     P1
     P2
     P3
     ...
     Pn
   }
   

At this point, your model should consist of signatures (with or without signature facts) and named predicates, no facts.

4. Check to ensure that the model can be instantiated when AllTogetherNow is not true.

   If it can't be instantiated, and you still have signature facts, then return to step 2 and factor some or all of them out. Revise AllTogetherNow to include the newly factored constraints.

   If it can't be instantiated, and you don't have any signature facts, then return to step 2 and factor out the constraints implicit in the cardinality constraints on your signatures. Revise AllTogetherNow to include the newly factored constraints.

5. Check to see whether AllTogetherNow can be instantiated.

   If it can be instantiated, then something has changed between your original model and now. That thing that changed was what was wrong in the original model.

6. Comment out half of the predicates currently live in AllTogetherNow, selected either by cunning or at random.

7. Check to see whether AllTogetherNow can be instantiated.

   If it cannot, then some subset of the predicates currently alive in AllTogetherNow contains a contradiction. Return to step 6 to comment out some more predicates.

   If AllTogetherNow can now be instantiated, then some subset of the predicates you just commented out are the reason the model cannot be instantiated as originally written. Continue to step 8.

8. Uncomment half of the constraints currently commented out in AllTogetherNow, chosen either randomly or by cunning. Return to step 7.

My experience is that a few loops through steps 6-8 generally help focus my attention enough that I can eventually see where the contradiction lies. The main complications I've experienced (YMMV) are (1) that one's initial draft model isn't limited to a single contradiction, (2) that contradictions may arise from unhappy combinations of predicates which are individually harmless, and (3) there may be more than one way to build up a contradictory combination (predicates, A, B, C, and D are each fine; A is fatal in conjunction with B or C ...).

One psychological difficulty that may arise is that the contradictions arise not in the 'interesting' part of the model, but in one's attempt to set the stage for the interesting questions. I don't know any cure for that except to tell oneself that any unexpected contradiction is automatically interesting, and worth spending time on. Sometimes I am able to persuade myself.