There have been some questions asked about how to use CryptoMiniSat as a library. Here, I give a simple example usage to help any future potential users. If there are any question that seems unanswered, please feel free to add them as a comment to this post.
First, we initialize the solver with high verbosity:
#include "cmsat/Solver.h" using namespace CMSat; SolverConf conf; conf.verbosity = 2; Solver solver(conf);
Then we add the variables 0..9:
for(int i = 0; i < 10; i++) { solver.newVar(); }
And add a clause that would look in the DIMACS input format as "2 -5 10 0":
vecclause; clause.push(Lit(1, false)); clause.push(Lit(4, true)); clause.push(Lit(9, false)); solver.addClause(clause);
We now create the assumptions that would look in DIMACS input format as "1 0" and "-5 0":
vecassumps; assumps.push(Lit(0, false)); assumps.push(Lit(4, true));
We now solve with these assumptions:
lbool ret = solver.solve(assumps);
Let's see if the state of the solver after solving is UNSAT regardless of the assumptions:
if (!solver.okay()) { printf("UNSAT!\n"); exit(0); }
Note that okay() can only be FALSE if "ret" was "l_False". However, it is important to distinguish between two kinds of l_False: one where only the assumptions couldn't be satisfied, and one where no matter what the assumptions are, the problem is unsatisfiable. See below for more.
Now let's check that the solution is UNSAT relative to the assumptions we have given. In this case, let's print the conflicting clause:
if (ret == l_False) { printf("Conflict clause expressed in terms of the assumptions:\n"); for(unsigned i = 0; i != solver.conflict.size(); i++) { printf("%s%d ", (solver.conflict[i].sign()) ? "" : "-", solver.conflict[i].var()+1); } printf("0\n"); }
The above will print an empty clause if solver.okay() is FALSE.
Now, let's see if the solution is SAT, and if so, print the solution to console, using DIMACS notation:
if (ret == l_True) { printf("We have the solution, it's here: \n"); for (unsigned var = 0; var != solve.nVars(); var++) if (S.model[var] != l_Undef) { printf("%s%d ", (solver.model[var] == l_True)? "" : "-", var+1); printf("0\n"); } }
If solver.okay()
is still TRUE (which it must be, if the ret was l_True), we can now add new clauses and new variables without restriction, and solve again (potentially with different assumptions). Note that most of the above applies to MiniSat as well.
When compiling the code, you have to pass the parameters such as:
$ g++ -fopenmp -lcryptominisat myprogram.cpp -o myprogram
PS: Thanks go to Martin Albrecht for pointing out some ambiguities in my explanation of the library usage, which have now been fixed.
Comments
0 responses to “How to use CryptoMiniSat 2.9 as a library”
Hi, I am confused that you check okay(). Shouldn’t just looking at ret be enough? When is ret != okay() except when ret is neither True nor False?
Thanks, good point! I fixed it now, and I think it’s made the explanation clearer. Thanks again!
Hi Mate,
Is there a way to feed CMS directly using Dimacs variables?
e.g.
Daniel
Not as simply as you mention above, because I explicitly disabled the functionality — I think it would be very dangerous in code. However, I can make a class like “DimacsClause” for your convenience and then you could do:
Would this be OK?
If you enable C++11 support in your compiler (-std=c++0x with GCC), you can do really nice stuff like this:
Now you can add clauses like this:
Yay for C++11! :-D
Wow, this sounds absolutely unbelievable!
I’m not managing to get the code to compile (g++ 4.6.3). The problem with
#include “cmsat/Solver.h”
is that that header file itself contains lines like
#include “cmsat/PropBy.h”
and since PropBy.h is in fact in the same folder as Solver.h, not in a subfolder of cmsat which is also called cmsat, compilation fails.
This seems to be the case for almost all the cmsat header files, and no cmsat subfolder of /usr/local/include/ or /usr/include was created when I installed CryptoMiniSat 2.9.5.
I went through the header files changing all the #includes, and simply got
linuxuser@i5-480M:~/York/latest/cpp$ g++ -o testbed_cryptominisat testbed_cryptominisat.cpp -lcryptominisat
/usr/bin/ld: cannot find -lcryptominisat
I have absolutely no idea what to do now! Do I need to mv into some specific directory? Could something have gone wrong when I used make to compile Cryptominisat?
Got it compiling and running.
1.) Created directory /usr/include/cmsat/ and copied modified versions of the CryptoMiniSat header files into it. The modified versions replaced all
#include “cmsat/nameoffile.h”
with
#include
2.) There are two typos in the souce code: Replace
(S.model[var] != l_Undef)
with
(solver.model[var] != l_Undef)
and then replace
for (unsigned var = 0; var != solve.nVars(); var++)
with
for (unsigned var = 0; var != solver.nVars(); var++)
3.) I changed the command line used to compile, after finding a forum in which someone stated “The libraries have to go after the local translation units … It has to do with how unresolved symbols are looked up by the linker”. So it’s now:
g++ -fopenmp -o myprogram myprogram.cpp -lcryptominisat
(I’ve just rechecked and the original version of that line definitely doesn’t work.)
4.) Copied the following files into /usr/local/lib/
~/CryptoMiniSat/cmsat-2.9.5/build/cmsat/.libs/libcryptominisat.lai
~/CryptoMiniSat/cmsat-2.9.5/build/cmsat/.libs/libcryptominisat-2.9.5.so
(Didn’t copy ~/CryptoMiniSat/cmsat-2.9.5/build/cmsat/.libs/libcryptominisat.so, instead created a new symlink to /usr/local/lib/libcryptominisat-2.9.5.so with that name in /usr/local/lib)
~/CryptoMiniSat/cmsat-2.9.5/build/cmsat/.libs/libcryptominisat.a
~/CryptoMiniSat/cmsat-2.9.5/build/cmsat/libcryptominisat.la
This wasn’t quite enough – I was still getting “error while loading shared libraries: libcryptominisat-2.9.5.so: cannot open shared object file: No such file or directory”. I made another copy of libcryptominisat-2.9.5.so and put it in /usr/lib/
Program output is:
c N st 0 0 10 1 0 0 0 3 0 no data no data —
c Flit: 0 Blit: 0 bXBeca: 0 bXProp: 0 Bins: 0 BRemL: 0 BRemN: 0 P: 0.0M T: 0.00
c Finding binary XORs T: 0.00 s found: 0
c Finding non-binary XORs: 0.00 s (found: 0, avg size: -nan)
c calculated reachability. Time: 0.00
c Calc default polars – time: 0.00 s pos: 2 undec: 7 neg: 1
c =========================================================================================
c types(t): F = full restart, N = normal restart
c types(t): S = simplification begin/end, E = solution found
c restart types(rt): st = static, dy = dynamic
c t rt Rest Confl Vars NormCls XorCls BinCls Learnts ClLits LtLits LGlueHist SGlueHist
c B st 0 0 10 1 0 0 0 3 0 no data no data —
c E st 1 0 0 1 0 0 0 3 0 no data no data —
c Verified 1 clauses.
c Verified 1 clauses.
We have the solution, it’s here:
10
20
-30
-40
-50
-60
-70
-80
-90
100
After all that, could I ask a question? A lot of the header files #include the original C versions of certain header files – , , etc. – instead of the C++ versions (, , etc.) Is there any reason for this apart from avoiding having to type std:: before certain function names?
The “correct” way to do this is to:
1. Pass -I options to gcc, telling it where to search for include files. If you pass -Ifoo then #include “bar.h” will try to open foo/bar.h.
2. Pass -L options to gcc, telling it where to search for libraries. If you pass -Lfoo then -lbar will try to open (some variation of) foo/libbar.a
3. Set LD_LIBRARY_PATH, telling the program loader where to search for libraries. If you compiled the program with -lbar and run the program as:
LD_LIBRARY_PATH=”/path/to/foo:$LD_LIBRARY_PATH” program
then the program loader will try to open (some variation of) /path/to/foo/libbar.so.
This way you don’t have to mess around as root in your global filesystem hierarchy (/usr/include, /usr/lib, etc.).
The above comment was mangled – the sharp-bracket thingies in the #include line seem to have been parsed as HTML tags and so everything in them’s vanished. Mate Soos, if you’re reading this, could you edit the comment and fix this? Thanks!
Can you include an example with an xor clause?
I tried using solver.addXorClause, but I don’t understand what the second (bool) argument does. While playing with this I sometimes trigger the assert below – what does it mean?
Thanks.
test: ../../cmsat/VarReplacer.cpp:503: void CMSat::VarReplacer::extendModelPossible() const: Assertion `solver.assigns[i].getBool() == (solver.assigns[it->var()].getBool() ^ it->sign())’ failed.
Abort
Hi Micea!
Can you please send over to soos.mate@gmail.com your program so that I can debug the assertion? I think it’s a bug in CryptoMiniSat.
An example for adding an xor clause is: lits;
vec
lits.push(Lit(0, false));
lits.push(Lit(1, false));
lits.push(Lit(2, false));
solver.addXorClause(lits, true);
this will add the XOR:
var0 XOR var1 XOR var2 = false;
if you want to add this:
var0 XOR var1 XOR var2 = true;
you have to say:
solver.addXorClause(lits, false);
I hope I have helped!
Mate
Hi Mate,
With some tests using addXorClause() I have the same assert as Mircea (using the last version of CryptoMiniSat):
Assertion failed: solver.assigns[i].getBool() == (solver.assigns[it->var()].getBool() ^ it->sign()), file VarReplacer.cpp, line 503
Did you find the issue? If I can isolate a simple code sample, I will send it to you.
Furthermore I tried the following sample and I’m surprised by the result:
Solver solver;
solver.newVar();
solver.newVar();
solver.newVar();
vec XorClauseLiterals;
XorClauseLiterals.push( Lit(0, false) );
XorClauseLiterals.push( Lit(1, false) );
XorClauseLiterals.push( Lit(2, false) );
solver.addXorClause(XorClauseLiterals, false);
vec Assumptions;
Assumptions.push( Lit(0, false) );
Assumptions.push( Lit(1, false) );
if(solver.solve(Assumptions) == l_True) cout << "SAT" << endl;
else cout << "UNSAT" << endl;
The result is SAT, I would expect UNSAT with the XOR condition. What do you think ?
Thanks.
Didier.
[…] want to include cryptominisat as a library to my project using cmake for its compilation process. A blog article by msoos explains how to compile cryptominisat as a library to your C++ project, but as far as I am not […]
Hi. Is there a way to generate a table with occurrence frequencies of the variables, after calling “parse_DIMACS”??
(I don’t want to change cryptominisat code, just using native methods in Solver class.)
No, but writing such a parser in python should be trivial :) Try it, you will learn about both DIMACS and python!
Good luck,
Mate