deba@2420: /* -*- C++ -*-
deba@2420:  *
deba@2420:  * This file is a part of LEMON, a generic C++ optimization library
deba@2420:  *
deba@2420:  * Copyright (C) 2003-2007
deba@2420:  * Egervary Jeno Kombinatorikus Optimalizalasi Kutatocsoport
deba@2420:  * (Egervary Research Group on Combinatorial Optimization, EGRES).
deba@2420:  *
deba@2420:  * Permission to use, modify and distribute this software is granted
deba@2420:  * provided that this copyright notice appears in all copies. For
deba@2420:  * precise terms see the accompanying LICENSE file.
deba@2420:  *
deba@2420:  * This software is provided "AS IS" with no warranty of any kind,
deba@2420:  * express or implied, and with no claim as to its suitability for any
deba@2420:  * purpose.
deba@2420:  *
deba@2420:  */
deba@2420: 
deba@2420: /// \ingroup demos
deba@2420: /// \file
deba@2420: /// \brief Solver for SAT-2 problems.
deba@2420: ///
deba@2420: /// This demo progam solves the SAT-2 problem, i.e. the boolean
deba@2420: /// satisfiability problem where each disjuction consists at most 2
deba@2420: /// terms.
deba@2420: ///
deba@2420: /// The program generates a graph from the boolean expression. Two
deba@2420: /// nodes are assigned to each boolean variable, an <tt>x</tt> and a
deba@2420: /// <tt>not x</tt> nodes. If there is an <tt>x or y</tt> disjunction
deba@2420: /// in the formula, then the <tt>not x => y</tt> and the <tt>not y =>
deba@2420: /// x</tt> edges are added to the graph. If there is a single
deba@2420: /// <tt>x</tt> term disjunction in the formula then the <tt>not x
deba@2420: /// =>x</tt> edge is added to the graph.
deba@2420: ///
deba@2420: /// The boolean formula could be satified if and only if the
deba@2420: /// <tt>x</tt> and <tt>not x</tt> nodes are in different strongly connected
deba@2420: /// components. A feasible solution could be get from the current
deba@2420: /// component numbering.
deba@2420: ///
deba@2420: /// \include sat-2.cc
deba@2420: 
deba@2420: #include <iostream>
deba@2420: #include <fstream>
deba@2420: #include <sstream>
deba@2420: #include <string>
deba@2420: #include <map>
deba@2420: 
deba@2420: #include <lemon/smart_graph.h>
deba@2420: #include <lemon/topology.h>
deba@2420: 
deba@2420: using namespace std;
deba@2420: using namespace lemon;
deba@2420: 
deba@2420: 
deba@2420: int main(int argc, const char *argv[]) {
deba@2420:   if (argc != 2) {
deba@2420:     std::cerr << "The SAT-2 solver demo" << std::endl << std::endl;
deba@2420:     std::cerr << "The  parameter should be a filename" << std::endl;
deba@2420:     std::cerr << "Each line of the file should contain a bool expression:" 
deba@2420:               << std::endl;
deba@2420:     std::cerr << "  [not] <variable> [or [not] <variable>]" << std::endl;
deba@2420:     std::cerr << "The program prints a feasible solution if it exists" 
deba@2420:               << std::endl;
deba@2420:     return -1;
deba@2420:   }
deba@2420:   ifstream is(argv[1]);
deba@2420: 
deba@2420:   SmartGraph graph;
deba@2420:   map<string, pair<SmartGraph::Node, SmartGraph::Node> > var;
deba@2420: 
deba@2420:   string line;
deba@2420:   while (getline(is, line)) {
deba@2420:     istringstream ls(line);
deba@2420:     string var1, var2, op;
deba@2420:     bool neg1 = false, neg2 = false;
deba@2420: 
deba@2420:     ls >> var1;
deba@2420:     if (var1 == "not") {
deba@2420:       neg1 = true;
deba@2420:       ls >> var1;
deba@2420:     }
deba@2420:     if (ls >> op) {
deba@2420:       if (op != "or") {
deba@2420:         cerr << "Wrong bool expression" << std::endl;
deba@2420:         return -1;
deba@2420:       } else {
deba@2420:         ls >> var2;
deba@2420:         if (var2 == "not") {
deba@2420:           neg2 = true;
deba@2420:           ls >> var2;
deba@2420:         }
deba@2420:       }
deba@2420:       if (ls >> op) {
deba@2420:         cerr << "Wrong bool expression" << std::endl;
deba@2420:         return -1;
deba@2420:       }
deba@2420: 
deba@2420:       map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it1;
deba@2420:       map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it2;    
deba@2420:       it1 = var.find(var1);
deba@2420:       if (it1 == var.end()) {
deba@2420:         SmartGraph::Node node = graph.addNode();
deba@2420:         SmartGraph::Node negNode = graph.addNode();
deba@2420:         it1 = var.insert(make_pair(var1, make_pair(node, negNode))).first;
deba@2420:       }
deba@2420: 
deba@2420:       it2 = var.find(var2);
deba@2420:       if (it2 == var.end()) {
deba@2420:         SmartGraph::Node node = graph.addNode();
deba@2420:         SmartGraph::Node negNode = graph.addNode();
deba@2420:         it2 = var.insert(make_pair(var2, make_pair(node, negNode))).first;
deba@2420:       }
deba@2420: 
deba@2420:       graph.addEdge(neg1 ? it1->second.first : it1->second.second, 
deba@2420:                     neg2 ? it2->second.second : it2->second.first);
deba@2420: 
deba@2420:       graph.addEdge(neg2 ? it2->second.first : it2->second.second, 
deba@2420:                     neg1 ? it1->second.second : it1->second.first);
deba@2420:     } else {
deba@2420: 
deba@2420:       map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it1;
deba@2420:       it1 = var.find(var1);
deba@2420:       if (it1 == var.end()) {
deba@2420:         SmartGraph::Node node = graph.addNode();
deba@2420:         SmartGraph::Node negNode = graph.addNode();
deba@2420:         it1 = var.insert(make_pair(var1, make_pair(node, negNode))).first;
deba@2420:       }
deba@2420:       graph.addEdge(neg1 ? it1->second.first : it1->second.second, 
deba@2420:                     neg1 ? it1->second.second : it1->second.first);
deba@2420:       
deba@2420:     }
deba@2420:     
deba@2420:   }
deba@2420:   
deba@2420:   SmartGraph::NodeMap<int> comp(graph);
deba@2420: 
deba@2420:   stronglyConnectedComponents(graph, comp); 
deba@2420: 
deba@2420:   for (map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator
deba@2420:          it = var.begin(); it != var.end(); ++it) {
deba@2420:     if (comp[it->second.first] == comp[it->second.second]) {
deba@2420:       std::cout << "There is no feasible solution." << std::endl;
deba@2420:       return 0;
deba@2420:     }
deba@2420:   }
deba@2420: 
deba@2420:   for (map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator
deba@2420:          it = var.begin(); it != var.end(); ++it) {
deba@2420:     if (comp[it->second.first] < comp[it->second.second]) {
deba@2420:       std::cout << it->first << " = false " << std::endl;
deba@2420:     } else {
deba@2420:       std::cout << it->first << " = true " << std::endl;
deba@2420:     }
deba@2420:   }
deba@2420:   
deba@2420:   return 0;
deba@2420: }