Alloy Community

User login

SAT solver (minisat) crashed. How to know the reason?

Home » Forums » Help » General Alloy Questions
 
Posted on: Thu, 10/08/2009 - 10:02
sun4384
Joined: 2008-10-20
Points: 71
User is offline
SAT solver (minisat) crashed. How to know the reason?
While analyzing a model, MiniSat crashed with a message saying "An error has occurred!". Model bound was quite high: four top level signatures with 30, 30, 60, 60 for their bounds.

 - Is it possible to look at the log to find out the reason? If so, where can I find the log? (I'm using Windows XP, by the way.)
 - Is it safe to assume this is because of insufficient memory? If so, how to solve the problem? (I remember the memory setting in Alloy menu is for CNF generation, and SAT solvers handle their own memory, right?)
 
Posted on: Thu, 10/08/2009 - 11:32    #1
sun4384
Joined: 2008-10-20
Points: 71
User is offline
Running the same analysis in a different machine (inferior CPU, less memory) got the job done successfully. I used the latest Alloy Analyzer for both. Things are getting confusing... Can you guess any possible explanation? Machines are not overclocked, and while running analyses, they were unattended.
 
Posted on: Thu, 10/08/2009 - 22:29    #2
Felix Chang
Joined: 2008-05-15
Points: 334
User is offline
No log sorry. Minisat runs via JNI and connects to the java runtime environment in a very memory unsafe way. When it crashes there is nothing we can get from our java code.
 
Posted on: Thu, 10/15/2009 - 04:23    #3
leberre
leberre's picture
Joined: 2008-04-23
Points: 115
User is offline
Just check the number of variables and clauses of the generated formula.

If those numbers are greater than a few million variables, a few tens of millions of clauses, then you should not expect the SAT solver to handle without problem the CNF :)

Syndicate content  

The development of this site is supported by the National Science Foundation under Computing Research Infrastructure Grant No. 0707612.

Theme originally designed by Chris Herberte