1.1 --- a/demo/Makefile.am Wed Apr 11 07:34:40 2007 +0000
1.2 +++ b/demo/Makefile.am Wed Apr 18 16:34:40 2007 +0000
1.3 @@ -13,7 +13,8 @@
1.4 demo/strongly_connected_orientation.lgf \
1.5 demo/sub_gad_input.lgf \
1.6 demo/u_components.lgf \
1.7 - demo/steiner.lgf
1.8 + demo/steiner.lgf \
1.9 + demo/sat-2.in
1.10
1.11 if WANT_DEMO
1.12
1.13 @@ -40,7 +41,9 @@
1.14 demo/simann_maxcut_demo \
1.15 demo/disjoint_paths_demo \
1.16 demo/strongly_connected_orientation \
1.17 - demo/steiner_demo
1.18 + demo/steiner_demo \
1.19 + demo/sat-2 \
1.20 + demo/sat
1.21
1.22 if HAVE_GLPK
1.23 noinst_PROGRAMS += demo/lp_demo demo/lp_maxflow_demo demo/mip_demo
1.24 @@ -107,4 +110,8 @@
1.25
1.26 demo_strongly_connected_orientation_SOURCES = demo/strongly_connected_orientation.cc
1.27
1.28 -demo_steiner_demo_SOURCES=demo/steiner_demo.cc
1.29 \ No newline at end of file
1.30 +demo_steiner_demo_SOURCES=demo/steiner_demo.cc
1.31 +
1.32 +demo_sat_2_SOURCES=demo/sat-2.cc
1.33 +
1.34 +demo_sat_SOURCES=demo/sat.cc
1.35 \ No newline at end of file
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/demo/sat-2.cc Wed Apr 18 16:34:40 2007 +0000
2.3 @@ -0,0 +1,157 @@
2.4 +/* -*- C++ -*-
2.5 + *
2.6 + * This file is a part of LEMON, a generic C++ optimization library
2.7 + *
2.8 + * Copyright (C) 2003-2007
2.9 + * Egervary Jeno Kombinatorikus Optimalizalasi Kutatocsoport
2.10 + * (Egervary Research Group on Combinatorial Optimization, EGRES).
2.11 + *
2.12 + * Permission to use, modify and distribute this software is granted
2.13 + * provided that this copyright notice appears in all copies. For
2.14 + * precise terms see the accompanying LICENSE file.
2.15 + *
2.16 + * This software is provided "AS IS" with no warranty of any kind,
2.17 + * express or implied, and with no claim as to its suitability for any
2.18 + * purpose.
2.19 + *
2.20 + */
2.21 +
2.22 +/// \ingroup demos
2.23 +/// \file
2.24 +/// \brief Solver for SAT-2 problems.
2.25 +///
2.26 +/// This demo progam solves the SAT-2 problem, i.e. the boolean
2.27 +/// satisfiability problem where each disjuction consists at most 2
2.28 +/// terms.
2.29 +///
2.30 +/// The program generates a graph from the boolean expression. Two
2.31 +/// nodes are assigned to each boolean variable, an <tt>x</tt> and a
2.32 +/// <tt>not x</tt> nodes. If there is an <tt>x or y</tt> disjunction
2.33 +/// in the formula, then the <tt>not x => y</tt> and the <tt>not y =>
2.34 +/// x</tt> edges are added to the graph. If there is a single
2.35 +/// <tt>x</tt> term disjunction in the formula then the <tt>not x
2.36 +/// =>x</tt> edge is added to the graph.
2.37 +///
2.38 +/// The boolean formula could be satified if and only if the
2.39 +/// <tt>x</tt> and <tt>not x</tt> nodes are in different strongly connected
2.40 +/// components. A feasible solution could be get from the current
2.41 +/// component numbering.
2.42 +///
2.43 +/// \include sat-2.cc
2.44 +
2.45 +#include <iostream>
2.46 +#include <fstream>
2.47 +#include <sstream>
2.48 +#include <string>
2.49 +#include <map>
2.50 +
2.51 +#include <lemon/smart_graph.h>
2.52 +#include <lemon/topology.h>
2.53 +
2.54 +using namespace std;
2.55 +using namespace lemon;
2.56 +
2.57 +
2.58 +int main(int argc, const char *argv[]) {
2.59 + if (argc != 2) {
2.60 + std::cerr << "The SAT-2 solver demo" << std::endl << std::endl;
2.61 + std::cerr << "The parameter should be a filename" << std::endl;
2.62 + std::cerr << "Each line of the file should contain a bool expression:"
2.63 + << std::endl;
2.64 + std::cerr << " [not] <variable> [or [not] <variable>]" << std::endl;
2.65 + std::cerr << "The program prints a feasible solution if it exists"
2.66 + << std::endl;
2.67 + return -1;
2.68 + }
2.69 + ifstream is(argv[1]);
2.70 +
2.71 + SmartGraph graph;
2.72 + map<string, pair<SmartGraph::Node, SmartGraph::Node> > var;
2.73 +
2.74 + string line;
2.75 + while (getline(is, line)) {
2.76 + istringstream ls(line);
2.77 + string var1, var2, op;
2.78 + bool neg1 = false, neg2 = false;
2.79 +
2.80 + ls >> var1;
2.81 + if (var1 == "not") {
2.82 + neg1 = true;
2.83 + ls >> var1;
2.84 + }
2.85 + if (ls >> op) {
2.86 + if (op != "or") {
2.87 + cerr << "Wrong bool expression" << std::endl;
2.88 + return -1;
2.89 + } else {
2.90 + ls >> var2;
2.91 + if (var2 == "not") {
2.92 + neg2 = true;
2.93 + ls >> var2;
2.94 + }
2.95 + }
2.96 + if (ls >> op) {
2.97 + cerr << "Wrong bool expression" << std::endl;
2.98 + return -1;
2.99 + }
2.100 +
2.101 + map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it1;
2.102 + map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it2;
2.103 + it1 = var.find(var1);
2.104 + if (it1 == var.end()) {
2.105 + SmartGraph::Node node = graph.addNode();
2.106 + SmartGraph::Node negNode = graph.addNode();
2.107 + it1 = var.insert(make_pair(var1, make_pair(node, negNode))).first;
2.108 + }
2.109 +
2.110 + it2 = var.find(var2);
2.111 + if (it2 == var.end()) {
2.112 + SmartGraph::Node node = graph.addNode();
2.113 + SmartGraph::Node negNode = graph.addNode();
2.114 + it2 = var.insert(make_pair(var2, make_pair(node, negNode))).first;
2.115 + }
2.116 +
2.117 + graph.addEdge(neg1 ? it1->second.first : it1->second.second,
2.118 + neg2 ? it2->second.second : it2->second.first);
2.119 +
2.120 + graph.addEdge(neg2 ? it2->second.first : it2->second.second,
2.121 + neg1 ? it1->second.second : it1->second.first);
2.122 + } else {
2.123 +
2.124 + map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it1;
2.125 + it1 = var.find(var1);
2.126 + if (it1 == var.end()) {
2.127 + SmartGraph::Node node = graph.addNode();
2.128 + SmartGraph::Node negNode = graph.addNode();
2.129 + it1 = var.insert(make_pair(var1, make_pair(node, negNode))).first;
2.130 + }
2.131 + graph.addEdge(neg1 ? it1->second.first : it1->second.second,
2.132 + neg1 ? it1->second.second : it1->second.first);
2.133 +
2.134 + }
2.135 +
2.136 + }
2.137 +
2.138 + SmartGraph::NodeMap<int> comp(graph);
2.139 +
2.140 + stronglyConnectedComponents(graph, comp);
2.141 +
2.142 + for (map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator
2.143 + it = var.begin(); it != var.end(); ++it) {
2.144 + if (comp[it->second.first] == comp[it->second.second]) {
2.145 + std::cout << "There is no feasible solution." << std::endl;
2.146 + return 0;
2.147 + }
2.148 + }
2.149 +
2.150 + for (map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator
2.151 + it = var.begin(); it != var.end(); ++it) {
2.152 + if (comp[it->second.first] < comp[it->second.second]) {
2.153 + std::cout << it->first << " = false " << std::endl;
2.154 + } else {
2.155 + std::cout << it->first << " = true " << std::endl;
2.156 + }
2.157 + }
2.158 +
2.159 + return 0;
2.160 +}
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/demo/sat.cc Wed Apr 18 16:34:40 2007 +0000
3.3 @@ -0,0 +1,115 @@
3.4 +/* -*- C++ -*-
3.5 + *
3.6 + * This file is a part of LEMON, a generic C++ optimization library
3.7 + *
3.8 + * Copyright (C) 2003-2007
3.9 + * Egervary Jeno Kombinatorikus Optimalizalasi Kutatocsoport
3.10 + * (Egervary Research Group on Combinatorial Optimization, EGRES).
3.11 + *
3.12 + * Permission to use, modify and distribute this software is granted
3.13 + * provided that this copyright notice appears in all copies. For
3.14 + * precise terms see the accompanying LICENSE file.
3.15 + *
3.16 + * This software is provided "AS IS" with no warranty of any kind,
3.17 + * express or implied, and with no claim as to its suitability for any
3.18 + * purpose.
3.19 + *
3.20 + */
3.21 +
3.22 +/// \ingroup demos
3.23 +/// \file
3.24 +/// \brief Solver for SAT problems.
3.25 +///
3.26 +/// This demo progam solves the SAT problem, i.e. the boolean
3.27 +/// satisfiability problem. The problem in general case is
3.28 +/// NP-complete.
3.29 +///
3.30 +/// The program uses an integer linear program solver. A <tt>{0,
3.31 +/// 1}</tt> variable is assigned to each boolean variable. The
3.32 +/// disjunctions are converted to linear inequalities as each negation
3.33 +/// is replaced with a substraction from one and each disjunction is
3.34 +/// converted to addition. The generated linear expression should be
3.35 +/// at least one.
3.36 +///
3.37 +/// \include sat.cc
3.38 +
3.39 +#include <iostream>
3.40 +#include <fstream>
3.41 +#include <sstream>
3.42 +#include <string>
3.43 +
3.44 +#include <lemon/lp.h>
3.45 +
3.46 +using namespace std;
3.47 +using namespace lemon;
3.48 +
3.49 +
3.50 +int main(int argc, const char *argv[]) {
3.51 + if (argc != 2) {
3.52 + std::cerr << "The SAT solver demo" << std::endl << std::endl;
3.53 + std::cerr << "The parameter should be a filename" << std::endl;
3.54 + std::cerr << "Each line of the file should contain a bool expression:"
3.55 + << std::endl;
3.56 + std::cerr << " [not] <variable> [or [not] <variable>]..." << std::endl;
3.57 + std::cerr << "The program prints a feasible solution if it exists"
3.58 + << std::endl;
3.59 + return -1;
3.60 + }
3.61 + ifstream is(argv[1]);
3.62 +
3.63 + Mip mip;
3.64 + mip.max();
3.65 + mip.obj(0);
3.66 +
3.67 + string line;
3.68 + while (getline(is, line)) {
3.69 + istringstream ls(line);
3.70 +
3.71 + Mip::Expr expr;
3.72 +
3.73 +
3.74 + string op;
3.75 + do {
3.76 + string var;
3.77 + bool neg = false;
3.78 +
3.79 + ls >> var;
3.80 + if (var == "not") {
3.81 + neg = true;
3.82 + ls >> var;
3.83 + }
3.84 +
3.85 + Mip::Col col = mip.colByName(var);
3.86 +
3.87 + if (col == INVALID) {
3.88 + col = mip.addCol();
3.89 + mip.colName(col, var);
3.90 + mip.colLowerBound(col, 0);
3.91 + mip.colUpperBound(col, 1);
3.92 + mip.integer(col, true);
3.93 + }
3.94 +
3.95 + expr += (neg ? 1 - col : col);
3.96 +
3.97 + } while (ls >> op && op == "or");
3.98 + if (ls) {
3.99 + std::cerr << "Wrong bool expression" << std::endl;
3.100 + return -1;
3.101 + }
3.102 + mip.addRow(expr >= 1);
3.103 + }
3.104 +
3.105 + mip.solve();
3.106 +
3.107 + if (mip.mipStatus() == Mip::OPTIMAL) {
3.108 + for (Mip::ColIt it(mip); it != INVALID; ++it) {
3.109 + std::cout << mip.colName(it) << " = "
3.110 + << (mip.primal(it) == 1 ? "true" : "false")
3.111 + << std::endl;
3.112 + }
3.113 + } else {
3.114 + std::cout << "There is no feasible solution." << std::endl;
3.115 + }
3.116 +
3.117 + return 0;
3.118 +}