/* -*- C++ -*-

  *

  * This file is a part of LEMON, a generic C++ optimization library

  *

  * Copyright (C) 2003-2008

  * Egervary Jeno Kombinatorikus Optimalizalasi Kutatocsoport

  * (Egervary Research Group on Combinatorial Optimization, EGRES).

  *

  * Permission to use, modify and distribute this software is granted

  * provided that this copyright notice appears in all copies. For

  * precise terms see the accompanying LICENSE file.

  *

  * This software is provided "AS IS" with no warranty of any kind,

  * express or implied, and with no claim as to its suitability for any

  * purpose.

  *

  */

 /// \ingroup demos

 /// \file

 /// \brief Solver for SAT problems.

 ///

 /// This demo progam solves the SAT problem, i.e. the boolean

 /// satisfiability problem. The problem in general case is

 /// NP-complete.

 ///

 /// The program uses an integer linear program solver. A <tt>{0,

 /// 1}</tt> variable is assigned to each boolean variable. The

 /// disjunctions are converted to linear inequalities as each negation

 /// is replaced with a substraction from one and each disjunction is

 /// converted to addition. The generated linear expression should be

 /// at least one.

 ///

 /// \include sat.cc

 #include <iostream>

 #include <fstream>

 #include <sstream>

 #include <string>

 #include <lemon/lp.h>

 using namespace std;

 using namespace lemon;

 int main(int argc, const char *argv[]) {

   if (argc != 2) {

     std::cerr << "The SAT solver demo" << std::endl << std::endl;

     std::cerr << "The  parameter should be a filename" << std::endl;

     std::cerr << "Each line of the file should contain a bool expression:" 

               << std::endl;

     std::cerr << "  [not] <variable> [or [not] <variable>]..." << std::endl;

     std::cerr << "The program prints a feasible solution if it exists" 

               << std::endl;

     return -1;

   }

   ifstream is(argv[1]);

   Mip mip;

   mip.max();

   mip.obj(0);

   string line;

   while (getline(is, line)) {

     istringstream ls(line);

     Mip::Expr expr;

     string op;

     do {

       string var;

       bool neg = false;

       ls >> var;

       if (var == "not") {

         neg = true;

         ls >> var;

       }

       Mip::Col col = mip.colByName(var);

       if (col == INVALID) {

         col = mip.addCol();

         mip.colName(col, var);

         mip.colLowerBound(col, 0);

         mip.colUpperBound(col, 1);

         mip.integer(col, true);        

       }

       expr += (neg ? 1 - col : col);

     } while (ls >> op && op == "or");

     if (ls) {

       std::cerr << "Wrong bool expression" << std::endl;

       return -1;

     }

     mip.addRow(expr >= 1);

   }

   mip.solve();

   if (mip.mipStatus() == Mip::OPTIMAL) {

     for (Mip::ColIt it(mip); it != INVALID; ++it) {

       std::cout << mip.colName(it) << " = " 

                 << (mip.primal(it) == 1 ? "true" : "false")

                 << std::endl;

     }

   } else {

     std::cout << "There is no feasible solution." << std::endl;

   }

   return 0;

 }