MaxSat

This example shows how to solve a Max-Sat problem using boolfunctions.

First we set up an SCIL::ILP_Problem IP as a maximization problem. In the next step we read an instance in DIMACS format. Here we also support the wcnf type for weighted Max-Sat. All read clauses are added to the IP using IP.add_boolfunction.

We solve the model IP by the command IP.optimize(). This command starts the optimization process.

Finally we count the number of satisfied clauses and output them.

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;