/* -*- C++ -*-
 *
 * This file is a part of LEMON, a generic C++ optimization library
 *
 * Copyright (C) 2003-2007
 * 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;
}