How to use CryptoMiniSat 2.9 as a library

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":

vec clause;
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":

vec assumps;
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.

Posted

June 20, 2012

Development, SAT

msoos

Tags:

library, programming

Comments

0 responses to “How to use CryptoMiniSat 2.9 as a library”

Martin Albrecht

June 20, 2012

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?
1. msoos
  
  June 20, 2012
  
  Thanks, good point! I fixed it now, and I think it’s made the explanation clearer. Thanks again!
Daniel

June 21, 2012
Hi Mate,

Is there a way to feed CMS directly using Dimacs variables?
e.g.
```
vec clause;
clause.push(2);
clause.push(-5);
clause.push(10);
solver.addClause(clause);
```
Daniel
1. msoos
  
  June 22, 2012
  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:
  
  DimacsClause cl; cl.push(2); cl.push(-5); cl.push(10); solver.addClause(cl.getClause());
  
  Would this be OK?
  1. Vegard
    
    June 22, 2012
    
    If you enable C++11 support in your compiler (-std=c++0x with GCC), you can do really nice stuff like this:
    
    template static void args_to_vector(std::vector &v) { } template static void args_to_vector(std::vector &v, T x, Args... args) { v.push_back(x); return args_to_vector(v, args...); } template void addClause(Args... args) { std::vector c; args_to_vector(c, args...); addClause(c); }
    
    Now you can add clauses like this:
    
    addClause(2, -5, 10); addClause(2, 5, 10, 11);
    
    Yay for C++11! :-D
    1. msoos
      
      June 22, 2012
      
      Wow, this sounds absolutely unbelievable!
James McLaughlin

January 21, 2013

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?
1. James McLaughlin
  
  January 21, 2013
  
  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?
  1. Vegard
    
    January 22, 2013
    
    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.).
James McLaughlin

January 21, 2013

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!
Mircea Draghicescu

January 31, 2013

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
1. msoos
  
  February 4, 2013
  
  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:
  vec lits;
  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
Didier

March 20, 2013

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.
Include cryptominisat as library with cmake | Lukas' Weblog

April 5, 2013

[…] 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 […]
Marco Marino

November 10, 2013

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.)
1. msoos
  
  November 20, 2013
  
  No, but writing such a parser in python should be trivial :) Try it, you will learn about both DIMACS and python!
  
  Good luck,
  
  Mate