Решение проблем SAT с использованием минисата - PullRequest
Новая
       44

Решение проблем SAT с использованием минисата

1 голос
/ 14 марта 2020

Я пытался решить SAT-экземпляры, используя API-интерфейсы minisat, но по какой-то причине minisat работает очень медленно, когда нужно распечатать результат. Я почти уверен, что я делаю что-то не так в вызовах API, так как я сам реализовал спутниковые решатели, и minisat не должен быть таким медленным в проверяемых мной экземплярах (мои собственные реализованные выходные данные решателя в течение 4 секунд)

ниже приведен код, который я написал. 

#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();
}

PS Я пытался удалить переменные релаксации, это все еще медленно

...