COIN-OR::LEMON - Graph Library

source: lemon-0.x/demo/sat-2.cc @ 2553:bfced05fa852

Last change on this file since 2553:bfced05fa852 was 2553:bfced05fa852, checked in by Alpar Juttner, 11 years ago

Happy New Year to LEMON (+ better update-copyright-header script)

File size: 4.9 KB
Line 
1/* -*- C++ -*-
2 *
3 * This file is a part of LEMON, a generic C++ optimization library
4 *
5 * Copyright (C) 2003-2008
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-2 problems.
22///
23/// This demo progam solves the SAT-2 problem, i.e. the boolean
24/// satisfiability problem where each disjuction consists at most 2
25/// terms.
26///
27/// The program generates a graph from the boolean expression. Two
28/// nodes are assigned to each boolean variable, an <tt>x</tt> and a
29/// <tt>not x</tt> nodes. If there is an <tt>x or y</tt> disjunction
30/// in the formula, then the <tt>not x => y</tt> and the <tt>not y =>
31/// x</tt> edges are added to the graph. If there is a single
32/// <tt>x</tt> term disjunction in the formula then the <tt>not x
33/// =>x</tt> edge is added to the graph.
34///
35/// The boolean formula could be satified if and only if the
36/// <tt>x</tt> and <tt>not x</tt> nodes are in different strongly connected
37/// components. A feasible solution could be get from the current
38/// component numbering.
39///
40/// \include sat-2.cc
41
42#include <iostream>
43#include <fstream>
44#include <sstream>
45#include <string>
46#include <map>
47
48#include <lemon/smart_graph.h>
49#include <lemon/topology.h>
50
51using namespace std;
52using namespace lemon;
53
54
55int main(int argc, const char *argv[]) {
56  if (argc != 2) {
57    std::cerr << "The SAT-2 solver demo" << std::endl << std::endl;
58    std::cerr << "The  parameter should be a filename" << std::endl;
59    std::cerr << "Each line of the file should contain a bool expression:"
60              << std::endl;
61    std::cerr << "  [not] <variable> [or [not] <variable>]" << std::endl;
62    std::cerr << "The program prints a feasible solution if it exists"
63              << std::endl;
64    return -1;
65  }
66  ifstream is(argv[1]);
67
68  SmartGraph graph;
69  map<string, pair<SmartGraph::Node, SmartGraph::Node> > var;
70
71  string line;
72  while (getline(is, line)) {
73    istringstream ls(line);
74    string var1, var2, op;
75    bool neg1 = false, neg2 = false;
76
77    ls >> var1;
78    if (var1 == "not") {
79      neg1 = true;
80      ls >> var1;
81    }
82    if (ls >> op) {
83      if (op != "or") {
84        cerr << "Wrong bool expression" << std::endl;
85        return -1;
86      } else {
87        ls >> var2;
88        if (var2 == "not") {
89          neg2 = true;
90          ls >> var2;
91        }
92      }
93      if (ls >> op) {
94        cerr << "Wrong bool expression" << std::endl;
95        return -1;
96      }
97
98      map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it1;
99      map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it2;   
100      it1 = var.find(var1);
101      if (it1 == var.end()) {
102        SmartGraph::Node node = graph.addNode();
103        SmartGraph::Node negNode = graph.addNode();
104        it1 = var.insert(make_pair(var1, make_pair(node, negNode))).first;
105      }
106
107      it2 = var.find(var2);
108      if (it2 == var.end()) {
109        SmartGraph::Node node = graph.addNode();
110        SmartGraph::Node negNode = graph.addNode();
111        it2 = var.insert(make_pair(var2, make_pair(node, negNode))).first;
112      }
113
114      graph.addEdge(neg1 ? it1->second.first : it1->second.second,
115                    neg2 ? it2->second.second : it2->second.first);
116
117      graph.addEdge(neg2 ? it2->second.first : it2->second.second,
118                    neg1 ? it1->second.second : it1->second.first);
119    } else {
120
121      map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it1;
122      it1 = var.find(var1);
123      if (it1 == var.end()) {
124        SmartGraph::Node node = graph.addNode();
125        SmartGraph::Node negNode = graph.addNode();
126        it1 = var.insert(make_pair(var1, make_pair(node, negNode))).first;
127      }
128      graph.addEdge(neg1 ? it1->second.first : it1->second.second,
129                    neg1 ? it1->second.second : it1->second.first);
130     
131    }
132   
133  }
134 
135  SmartGraph::NodeMap<int> comp(graph);
136
137  stronglyConnectedComponents(graph, comp);
138
139  for (map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator
140         it = var.begin(); it != var.end(); ++it) {
141    if (comp[it->second.first] == comp[it->second.second]) {
142      std::cout << "There is no feasible solution." << std::endl;
143      return 0;
144    }
145  }
146
147  for (map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator
148         it = var.begin(); it != var.end(); ++it) {
149    if (comp[it->second.first] < comp[it->second.second]) {
150      std::cout << it->first << " = false " << std::endl;
151    } else {
152      std::cout << it->first << " = true " << std::endl;
153    }
154  }
155 
156  return 0;
157}
Note: See TracBrowser for help on using the repository browser.