maxsat.cc

#include<scil/scil.h>
#include<scil/core/boolfunction.h>
#include<iostream>

using namespace SCIL;
using namespace std;

void read_instance(char* infile, ILP_Problem &IP, vector<var>& vars, list<boolfunction*>& bf_list) {

   string path(infile);
   ifstream file(path.c_str());
   if(file.fail()) {
      cerr<<"no file with name "<< infile<<" found!"<< endl;
      exit(1);
   }
   char buf[1024];
   while(file.peek() != 'p')
      file.getline(buf, 1024);

   char c;
   string type;
   int nv,nc, v, weight =1;

   file>>c;
   file>>type;
   file>>nv;
   file>>nc;
   cout<<c<<" "<<type<<" "<<nv<<" "<<nc<<endl;
   vars.resize(nv+1); 
   for(int i=1; i<=nv; i++){
      vars[i] = IP.add_binary_variable(0);
   }
   for(int j=0; j<nc; j++){
      if(type == "wcnf")
        file >> weight;
      boolfunction* bf = NULL;
      file >> v;
      while(v != 0){
         if(bf){
            if(v < 0)
               bf->add(OR, vars[-v], true);
            else
               bf->add(OR, vars[v]);
         } else {
            if(v < 0)
               bf = new boolfunction(vars[-v], true);
            else
               bf = new boolfunction(vars[v]);
         }
         file >> v;
      }
      cout<<weight<<"   "<<j<<": "<<bf<<endl;
      bf_list.push_back(bf);
      IP.add_boolfunction(bf, weight);
   }

}

int main(int argc, char** argv) {
   
   vector<var> vars;
   list<boolfunction*> bf_list;
   ILP_Problem IP(Optsense_Max);
   
   read_instance(argv[1], IP,vars,bf_list);

   IP.optimize();

   solution s = IP.get_solution();
   cout<<"-----------Solution-----------"<<endl;
   for( int i = 1; i < vars.size(); i++)
      cout<<"x"<<i-1<<": "<<s.value(vars[i])<<endl;
   int num=0;
   for( list<boolfunction*>::iterator it = bf_list.begin(); it != bf_list.end(); it++)
      if (!((*it)->evaluate(s))){
         cout<<(*it)<<"  value: "<<(*it)->evaluate(s)<<endl;
         num++;
      }
   cout<<"O = "<<num<<endl;
}

---