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

 }