1

我一直在尝试使用 minisat API 解决 SAT 实例，但由于某种原因，minisat 在打印结果时非常慢。我很确定我在 API 调用中做错了，因为我自己实现了 sat 求解器，并且 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我已经尝试删除松弛变量它仍然很慢

4

0 回答 0