/* -*- 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;

}