Solving SAT problems using minisat

332 Views Asked by At

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

0

There are 0 best solutions below