|
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 |
|
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 } |