1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/demo/sat-2.cc Wed Apr 18 16:34:40 2007 +0000
1.3 @@ -0,0 +1,157 @@
1.4 +/* -*- C++ -*-
1.5 + *
1.6 + * This file is a part of LEMON, a generic C++ optimization library
1.7 + *
1.8 + * Copyright (C) 2003-2007
1.9 + * Egervary Jeno Kombinatorikus Optimalizalasi Kutatocsoport
1.10 + * (Egervary Research Group on Combinatorial Optimization, EGRES).
1.11 + *
1.12 + * Permission to use, modify and distribute this software is granted
1.13 + * provided that this copyright notice appears in all copies. For
1.14 + * precise terms see the accompanying LICENSE file.
1.15 + *
1.16 + * This software is provided "AS IS" with no warranty of any kind,
1.17 + * express or implied, and with no claim as to its suitability for any
1.18 + * purpose.
1.19 + *
1.20 + */
1.21 +
1.22 +/// \ingroup demos
1.23 +/// \file
1.24 +/// \brief Solver for SAT-2 problems.
1.25 +///
1.26 +/// This demo progam solves the SAT-2 problem, i.e. the boolean
1.27 +/// satisfiability problem where each disjuction consists at most 2
1.28 +/// terms.
1.29 +///
1.30 +/// The program generates a graph from the boolean expression. Two
1.31 +/// nodes are assigned to each boolean variable, an <tt>x</tt> and a
1.32 +/// <tt>not x</tt> nodes. If there is an <tt>x or y</tt> disjunction
1.33 +/// in the formula, then the <tt>not x => y</tt> and the <tt>not y =>
1.34 +/// x</tt> edges are added to the graph. If there is a single
1.35 +/// <tt>x</tt> term disjunction in the formula then the <tt>not x
1.36 +/// =>x</tt> edge is added to the graph.
1.37 +///
1.38 +/// The boolean formula could be satified if and only if the
1.39 +/// <tt>x</tt> and <tt>not x</tt> nodes are in different strongly connected
1.40 +/// components. A feasible solution could be get from the current
1.41 +/// component numbering.
1.42 +///
1.43 +/// \include sat-2.cc
1.44 +
1.45 +#include <iostream>
1.46 +#include <fstream>
1.47 +#include <sstream>
1.48 +#include <string>
1.49 +#include <map>
1.50 +
1.51 +#include <lemon/smart_graph.h>
1.52 +#include <lemon/topology.h>
1.53 +
1.54 +using namespace std;
1.55 +using namespace lemon;
1.56 +
1.57 +
1.58 +int main(int argc, const char *argv[]) {
1.59 + if (argc != 2) {
1.60 + std::cerr << "The SAT-2 solver demo" << std::endl << std::endl;
1.61 + std::cerr << "The parameter should be a filename" << std::endl;
1.62 + std::cerr << "Each line of the file should contain a bool expression:"
1.63 + << std::endl;
1.64 + std::cerr << " [not] <variable> [or [not] <variable>]" << std::endl;
1.65 + std::cerr << "The program prints a feasible solution if it exists"
1.66 + << std::endl;
1.67 + return -1;
1.68 + }
1.69 + ifstream is(argv[1]);
1.70 +
1.71 + SmartGraph graph;
1.72 + map<string, pair<SmartGraph::Node, SmartGraph::Node> > var;
1.73 +
1.74 + string line;
1.75 + while (getline(is, line)) {
1.76 + istringstream ls(line);
1.77 + string var1, var2, op;
1.78 + bool neg1 = false, neg2 = false;
1.79 +
1.80 + ls >> var1;
1.81 + if (var1 == "not") {
1.82 + neg1 = true;
1.83 + ls >> var1;
1.84 + }
1.85 + if (ls >> op) {
1.86 + if (op != "or") {
1.87 + cerr << "Wrong bool expression" << std::endl;
1.88 + return -1;
1.89 + } else {
1.90 + ls >> var2;
1.91 + if (var2 == "not") {
1.92 + neg2 = true;
1.93 + ls >> var2;
1.94 + }
1.95 + }
1.96 + if (ls >> op) {
1.97 + cerr << "Wrong bool expression" << std::endl;
1.98 + return -1;
1.99 + }
1.100 +
1.101 + map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it1;
1.102 + map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it2;
1.103 + it1 = var.find(var1);
1.104 + if (it1 == var.end()) {
1.105 + SmartGraph::Node node = graph.addNode();
1.106 + SmartGraph::Node negNode = graph.addNode();
1.107 + it1 = var.insert(make_pair(var1, make_pair(node, negNode))).first;
1.108 + }
1.109 +
1.110 + it2 = var.find(var2);
1.111 + if (it2 == var.end()) {
1.112 + SmartGraph::Node node = graph.addNode();
1.113 + SmartGraph::Node negNode = graph.addNode();
1.114 + it2 = var.insert(make_pair(var2, make_pair(node, negNode))).first;
1.115 + }
1.116 +
1.117 + graph.addEdge(neg1 ? it1->second.first : it1->second.second,
1.118 + neg2 ? it2->second.second : it2->second.first);
1.119 +
1.120 + graph.addEdge(neg2 ? it2->second.first : it2->second.second,
1.121 + neg1 ? it1->second.second : it1->second.first);
1.122 + } else {
1.123 +
1.124 + map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it1;
1.125 + it1 = var.find(var1);
1.126 + if (it1 == var.end()) {
1.127 + SmartGraph::Node node = graph.addNode();
1.128 + SmartGraph::Node negNode = graph.addNode();
1.129 + it1 = var.insert(make_pair(var1, make_pair(node, negNode))).first;
1.130 + }
1.131 + graph.addEdge(neg1 ? it1->second.first : it1->second.second,
1.132 + neg1 ? it1->second.second : it1->second.first);
1.133 +
1.134 + }
1.135 +
1.136 + }
1.137 +
1.138 + SmartGraph::NodeMap<int> comp(graph);
1.139 +
1.140 + stronglyConnectedComponents(graph, comp);
1.141 +
1.142 + for (map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator
1.143 + it = var.begin(); it != var.end(); ++it) {
1.144 + if (comp[it->second.first] == comp[it->second.second]) {
1.145 + std::cout << "There is no feasible solution." << std::endl;
1.146 + return 0;
1.147 + }
1.148 + }
1.149 +
1.150 + for (map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator
1.151 + it = var.begin(); it != var.end(); ++it) {
1.152 + if (comp[it->second.first] < comp[it->second.second]) {
1.153 + std::cout << it->first << " = false " << std::endl;
1.154 + } else {
1.155 + std::cout << it->first << " = true " << std::endl;
1.156 + }
1.157 + }
1.158 +
1.159 + return 0;
1.160 +}