/* -*- 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-2 problems.

///

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

/// satisfiability problem where each disjuction consists at most 2

/// terms.

///

/// The program generates a graph from the boolean expression. Two

/// nodes are assigned to each boolean variable, an <tt>x</tt> and a

/// <tt>not x</tt> nodes. If there is an <tt>x or y</tt> disjunction

/// in the formula, then the <tt>not x => y</tt> and the <tt>not y =>

/// x</tt> edges are added to the graph. If there is a single

/// <tt>x</tt> term disjunction in the formula then the <tt>not x

/// =>x</tt> edge is added to the graph.

///

/// The boolean formula could be satified if and only if the

/// <tt>x</tt> and <tt>not x</tt> nodes are in different strongly connected

/// components. A feasible solution could be get from the current

/// component numbering.

///

/// \include sat-2.cc

#include <iostream>

#include <fstream>

#include <sstream>

#include <string>

#include <map>

#include <lemon/smart_graph.h>

#include <lemon/topology.h>

using namespace std;

using namespace lemon;

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

  if (argc != 2) {

    std::cerr << "The SAT-2 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]);

  SmartGraph graph;

  map<string, pair<SmartGraph::Node, SmartGraph::Node> > var;

  string line;

  while (getline(is, line)) {

    istringstream ls(line);

    string var1, var2, op;

    bool neg1 = false, neg2 = false;

    ls >> var1;

    if (var1 == "not") {

      neg1 = true;

      ls >> var1;

    }

    if (ls >> op) {

      if (op != "or") {

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

        return -1;

      } else {

        ls >> var2;

        if (var2 == "not") {

          neg2 = true;

          ls >> var2;

        }

      }

      if (ls >> op) {

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

        return -1;

      }

      map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it1;

      map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it2;    

      it1 = var.find(var1);

      if (it1 == var.end()) {

        SmartGraph::Node node = graph.addNode();

        SmartGraph::Node negNode = graph.addNode();

        it1 = var.insert(make_pair(var1, make_pair(node, negNode))).first;

      }

      it2 = var.find(var2);

      if (it2 == var.end()) {

        SmartGraph::Node node = graph.addNode();

        SmartGraph::Node negNode = graph.addNode();

        it2 = var.insert(make_pair(var2, make_pair(node, negNode))).first;

      }

      graph.addEdge(neg1 ? it1->second.first : it1->second.second, 

                    neg2 ? it2->second.second : it2->second.first);

      graph.addEdge(neg2 ? it2->second.first : it2->second.second, 

                    neg1 ? it1->second.second : it1->second.first);

    } else {

      map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it1;

      it1 = var.find(var1);

      if (it1 == var.end()) {

        SmartGraph::Node node = graph.addNode();

        SmartGraph::Node negNode = graph.addNode();

        it1 = var.insert(make_pair(var1, make_pair(node, negNode))).first;

      }

      graph.addEdge(neg1 ? it1->second.first : it1->second.second, 

                    neg1 ? it1->second.second : it1->second.first);

    }

  }

  SmartGraph::NodeMap<int> comp(graph);

  stronglyConnectedComponents(graph, comp); 

  for (map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator

         it = var.begin(); it != var.end(); ++it) {

    if (comp[it->second.first] == comp[it->second.second]) {

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

      return 0;

    }

  }

  for (map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator

         it = var.begin(); it != var.end(); ++it) {

    if (comp[it->second.first] < comp[it->second.second]) {

      std::cout << it->first << " = false " << std::endl;

    } else {

      std::cout << it->first << " = true " << std::endl;

    }

  }

  return 0;

}