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