1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/demo/sat.cc	Wed Apr 18 16:34:40 2007 +0000
     1.3 @@ -0,0 +1,115 @@
     1.4 +/* -*- C++ -*-
     1.5 + *
     1.6 + * This file is a part of LEMON, a generic C++ optimization library
     1.7 + *
     1.8 + * Copyright (C) 2003-2007
     1.9 + * Egervary Jeno Kombinatorikus Optimalizalasi Kutatocsoport
    1.10 + * (Egervary Research Group on Combinatorial Optimization, EGRES).
    1.11 + *
    1.12 + * Permission to use, modify and distribute this software is granted
    1.13 + * provided that this copyright notice appears in all copies. For
    1.14 + * precise terms see the accompanying LICENSE file.
    1.15 + *
    1.16 + * This software is provided "AS IS" with no warranty of any kind,
    1.17 + * express or implied, and with no claim as to its suitability for any
    1.18 + * purpose.
    1.19 + *
    1.20 + */
    1.21 +
    1.22 +/// \ingroup demos
    1.23 +/// \file
    1.24 +/// \brief Solver for SAT problems.
    1.25 +///
    1.26 +/// This demo progam solves the SAT problem, i.e. the boolean
    1.27 +/// satisfiability problem. The problem in general case is
    1.28 +/// NP-complete.
    1.29 +///
    1.30 +/// The program uses an integer linear program solver. A <tt>{0,
    1.31 +/// 1}</tt> variable is assigned to each boolean variable. The
    1.32 +/// disjunctions are converted to linear inequalities as each negation
    1.33 +/// is replaced with a substraction from one and each disjunction is
    1.34 +/// converted to addition. The generated linear expression should be
    1.35 +/// at least one.
    1.36 +///
    1.37 +/// \include sat.cc
    1.38 +
    1.39 +#include <iostream>
    1.40 +#include <fstream>
    1.41 +#include <sstream>
    1.42 +#include <string>
    1.43 +
    1.44 +#include <lemon/lp.h>
    1.45 +
    1.46 +using namespace std;
    1.47 +using namespace lemon;
    1.48 +
    1.49 +
    1.50 +int main(int argc, const char *argv[]) {
    1.51 +  if (argc != 2) {
    1.52 +    std::cerr << "The SAT solver demo" << std::endl << std::endl;
    1.53 +    std::cerr << "The  parameter should be a filename" << std::endl;
    1.54 +    std::cerr << "Each line of the file should contain a bool expression:" 
    1.55 +              << std::endl;
    1.56 +    std::cerr << "  [not] <variable> [or [not] <variable>]..." << std::endl;
    1.57 +    std::cerr << "The program prints a feasible solution if it exists" 
    1.58 +              << std::endl;
    1.59 +    return -1;
    1.60 +  }
    1.61 +  ifstream is(argv[1]);
    1.62 +
    1.63 +  Mip mip;
    1.64 +  mip.max();
    1.65 +  mip.obj(0);
    1.66 +
    1.67 +  string line;
    1.68 +  while (getline(is, line)) {
    1.69 +    istringstream ls(line);
    1.70 +
    1.71 +    Mip::Expr expr;
    1.72 +
    1.73 +
    1.74 +    string op;
    1.75 +    do {
    1.76 +      string var;
    1.77 +      bool neg = false;
    1.78 +
    1.79 +      ls >> var;
    1.80 +      if (var == "not") {
    1.81 +        neg = true;
    1.82 +        ls >> var;
    1.83 +      }
    1.84 +
    1.85 +      Mip::Col col = mip.colByName(var);
    1.86 +
    1.87 +      if (col == INVALID) {
    1.88 +        col = mip.addCol();
    1.89 +        mip.colName(col, var);
    1.90 +        mip.colLowerBound(col, 0);
    1.91 +        mip.colUpperBound(col, 1);
    1.92 +        mip.integer(col, true);        
    1.93 +      }
    1.94 +      
    1.95 +      expr += (neg ? 1 - col : col);
    1.96 +
    1.97 +    } while (ls >> op && op == "or");
    1.98 +    if (ls) {
    1.99 +      std::cerr << "Wrong bool expression" << std::endl;
   1.100 +      return -1;
   1.101 +    }
   1.102 +    mip.addRow(expr >= 1);
   1.103 +  }
   1.104 +
   1.105 +  mip.solve();
   1.106 +
   1.107 +  if (mip.mipStatus() == Mip::OPTIMAL) {
   1.108 +    for (Mip::ColIt it(mip); it != INVALID; ++it) {
   1.109 +      std::cout << mip.colName(it) << " = " 
   1.110 +                << (mip.primal(it) == 1 ? "true" : "false")
   1.111 +                << std::endl;
   1.112 +    }
   1.113 +  } else {
   1.114 +    std::cout << "There is no feasible solution." << std::endl;
   1.115 +  }
   1.116 +  
   1.117 +  return 0;
   1.118 +}