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