COIN-OR::LEMON - Graph Library

source: lemon-0.x/demo/sat.cc @ 2420:07c4f9bcb4d5

Last change on this file since 2420:07c4f9bcb4d5 was 2420:07c4f9bcb4d5, checked in by Balazs Dezso, 17 years ago

Demo program for SAT problems

File size: 2.9 KB
Line 
1/* -*- C++ -*-
2 *
3 * This file is a part of LEMON, a generic C++ optimization library
4 *
5 * Copyright (C) 2003-2007
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
43using namespace std;
44using namespace lemon;
45
46
47int 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}
Note: See TracBrowser for help on using the repository browser.