1

I've been trying to solve SAT instances using minisat APIs but for some reason minisat is very slow when it comes to printing out the result. I am pretty sure that I am doing something wrong in the API calls as I've implemented sat solvers myself and minisat is not supposed to be that slow on the instances I am checking (my own implemented solver outputs within 4 secs)

below is the code that I wrote.

#include "core/Solver.h"
#include <algorithm>
#include <cmath>
#include <cstdio>
#include <iostream>
#include <string>
#include <vector>

using namespace Minisat;

Solver s1;
int no_clauses;
int no_variables;
vec<Var> vars;
vec<Var> relax_vars;


void read_clause(){
  char c;
  int lits;
  std::string temp; 
  std::cin>>c;
  while(c=='c'){
    getline(std::cin,temp);
    std::cin>>c; 
  }
  std::cin>>c>>temp;
  std::cin>>no_variables;
  std::cin>>no_clauses;

  vars.growTo(no_variables);
  relax_vars.growTo(no_clauses);

  for(int i=0;i<no_variables;i++)
    vars[i]=s1.newVar();

  for(int i=0;i<no_clauses;i++)
     relax_vars[i]=s1.newVar();

  for(int i=0;i<no_clauses;i++){
    vec<Lit> cl_list;
      while(1){
          std::cin>>lits;
          if(lits==0)
            break;
          if(lits>0)
           cl_list.push(mkLit(vars[lits-1],false));         
          else 
            cl_list.push(~mkLit(vars[-lits-1],false));
    }
    cl_list.push(mkLit(relax_vars[i],false));
    s1.addClause(cl_list);
  }
}




int main(){
   read_clause();
   std::cout<<s1.solve();
}

P.S I've tried removing the relaxation variables it is still slow

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
lava_07
  • 83
  • 1
  • 7
  • The question is somewhat unclear. Is the call to `s1.solve()` taking long, or the model-printing functionality of MiniSAT? What makes you believe that MiniSAT is not supposed to be *that slow* on the instances you are solving? Furthermore, the question is incomplete without at least one such instance. – Patrick Trentin Mar 15 '20 at 11:54
  • The model printing I meant.. I know it isn't supposed to be that slow as I tested the instance on crypto-minisat online and it gave an output within 2 secs – lava_07 Mar 15 '20 at 12:30
  • Are you saying that if you replace `std::cout< – Patrick Trentin Mar 15 '20 at 12:38
  • Yes! I have also noticed wrapping the Solver object in a class has the same effect. P.S I had no idea crypto-minisat was different I am pretty new to this! – lava_07 Mar 15 '20 at 12:42
  • 2
    I see. I don't have the source code in front of me, but one possible explanation is that the `std::ostream& operator<<(std::ostream& os, const Solver& obj)` implementation in the MiniSAT library appends `std::endl` rather than `'\n'` at the end of each line.. [this causes the output stream to be flushed and can significantly slow down the execution](https://stackoverflow.com/questions/213907/c-stdendl-vs-n). Therefore, you may want to try implementing your own model-printing routine. – Patrick Trentin Mar 15 '20 at 12:50
  • Thanks a ton! will try! – lava_07 Mar 15 '20 at 14:16

0 Answers0