demo/sat.cc
author kpeter
Thu, 28 Feb 2008 02:54:27 +0000
changeset 2581 054566ac0934
parent 2420 07c4f9bcb4d5
permissions -rw-r--r--
Query improvements in the min cost flow algorithms.

- External flow and potential maps can be used.
- New query functions: flow() and potential().
- CycleCanceling also provides dual solution (node potentials).
- Doc improvements.
     1 /* -*- C++ -*-
     2  *
     3  * This file is a part of LEMON, a generic C++ optimization library
     4  *
     5  * Copyright (C) 2003-2008
     6  * Egervary Jeno Kombinatorikus Optimalizalasi Kutatocsoport
     7  * (Egervary Research Group on Combinatorial Optimization, EGRES).
     8  *
     9  * Permission to use, modify and distribute this software is granted
    10  * provided that this copyright notice appears in all copies. For
    11  * precise terms see the accompanying LICENSE file.
    12  *
    13  * This software is provided "AS IS" with no warranty of any kind,
    14  * express or implied, and with no claim as to its suitability for any
    15  * purpose.
    16  *
    17  */
    18 
    19 /// \ingroup demos
    20 /// \file
    21 /// \brief Solver for SAT problems.
    22 ///
    23 /// This demo progam solves the SAT problem, i.e. the boolean
    24 /// satisfiability problem. The problem in general case is
    25 /// NP-complete.
    26 ///
    27 /// The program uses an integer linear program solver. A <tt>{0,
    28 /// 1}</tt> variable is assigned to each boolean variable. The
    29 /// disjunctions are converted to linear inequalities as each negation
    30 /// is replaced with a substraction from one and each disjunction is
    31 /// converted to addition. The generated linear expression should be
    32 /// at least one.
    33 ///
    34 /// \include sat.cc
    35 
    36 #include <iostream>
    37 #include <fstream>
    38 #include <sstream>
    39 #include <string>
    40 
    41 #include <lemon/lp.h>
    42 
    43 using namespace std;
    44 using namespace lemon;
    45 
    46 
    47 int main(int argc, const char *argv[]) {
    48   if (argc != 2) {
    49     std::cerr << "The SAT solver demo" << std::endl << std::endl;
    50     std::cerr << "The  parameter should be a filename" << std::endl;
    51     std::cerr << "Each line of the file should contain a bool expression:" 
    52               << std::endl;
    53     std::cerr << "  [not] <variable> [or [not] <variable>]..." << std::endl;
    54     std::cerr << "The program prints a feasible solution if it exists" 
    55               << std::endl;
    56     return -1;
    57   }
    58   ifstream is(argv[1]);
    59 
    60   Mip mip;
    61   mip.max();
    62   mip.obj(0);
    63 
    64   string line;
    65   while (getline(is, line)) {
    66     istringstream ls(line);
    67 
    68     Mip::Expr expr;
    69 
    70 
    71     string op;
    72     do {
    73       string var;
    74       bool neg = false;
    75 
    76       ls >> var;
    77       if (var == "not") {
    78         neg = true;
    79         ls >> var;
    80       }
    81 
    82       Mip::Col col = mip.colByName(var);
    83 
    84       if (col == INVALID) {
    85         col = mip.addCol();
    86         mip.colName(col, var);
    87         mip.colLowerBound(col, 0);
    88         mip.colUpperBound(col, 1);
    89         mip.integer(col, true);        
    90       }
    91       
    92       expr += (neg ? 1 - col : col);
    93 
    94     } while (ls >> op && op == "or");
    95     if (ls) {
    96       std::cerr << "Wrong bool expression" << std::endl;
    97       return -1;
    98     }
    99     mip.addRow(expr >= 1);
   100   }
   101 
   102   mip.solve();
   103 
   104   if (mip.mipStatus() == Mip::OPTIMAL) {
   105     for (Mip::ColIt it(mip); it != INVALID; ++it) {
   106       std::cout << mip.colName(it) << " = " 
   107                 << (mip.primal(it) == 1 ? "true" : "false")
   108                 << std::endl;
   109     }
   110   } else {
   111     std::cout << "There is no feasible solution." << std::endl;
   112   }
   113   
   114   return 0;
   115 }