diff -r 6a567c0f1214 -r 07c4f9bcb4d5 demo/sat-2.cc
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/sat-2.cc	Wed Apr 18 16:34:40 2007 +0000
@@ -0,0 +1,157 @@
+/* -*- 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;
+}