Major improvements in NetworkSimplex.
Main changes:
- Use -potenital[] instead of potential[] to conform to the usual
terminology.
- Use function parameter instead of #define commands to select pivot rule.
- Use much faster implementation for the candidate list pivot rule.
It is about 5-20 times faster now.
- Add a new pivot rule called "Limited Search" that is a modified
version of "Block Search". It is about 25 percent faster on rather
sparse graphs.
- By default "Limited Search" is used for sparse graphs and
"Block Search" is used otherwise. This combined method is the most
efficient on every input class.
- Change the name of private members to start with "_".
- Change the name of function parameters not to start with "_".
- Remove unnecessary documentation for private members.
- Many doc improvements.
3 * This file is a part of LEMON, a generic C++ optimization library
5 * Copyright (C) 2003-2008
6 * Egervary Jeno Kombinatorikus Optimalizalasi Kutatocsoport
7 * (Egervary Research Group on Combinatorial Optimization, EGRES).
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.
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
21 /// \brief Solver for SAT-2 problems.
23 /// This demo progam solves the SAT-2 problem, i.e. the boolean
24 /// satisfiability problem where each disjuction consists at most 2
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.
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.
48 #include <lemon/smart_graph.h>
49 #include <lemon/topology.h>
52 using namespace lemon;
55 int main(int argc, const char *argv[]) {
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:"
61 std::cerr << " [not] <variable> [or [not] <variable>]" << std::endl;
62 std::cerr << "The program prints a feasible solution if it exists"
69 map<string, pair<SmartGraph::Node, SmartGraph::Node> > var;
72 while (getline(is, line)) {
73 istringstream ls(line);
74 string var1, var2, op;
75 bool neg1 = false, neg2 = false;
84 cerr << "Wrong bool expression" << std::endl;
94 cerr << "Wrong bool expression" << std::endl;
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;
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;
114 graph.addEdge(neg1 ? it1->second.first : it1->second.second,
115 neg2 ? it2->second.second : it2->second.first);
117 graph.addEdge(neg2 ? it2->second.first : it2->second.second,
118 neg1 ? it1->second.second : it1->second.first);
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;
128 graph.addEdge(neg1 ? it1->second.first : it1->second.second,
129 neg1 ? it1->second.second : it1->second.first);
135 SmartGraph::NodeMap<int> comp(graph);
137 stronglyConnectedComponents(graph, comp);
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;
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;
152 std::cout << it->first << " = true " << std::endl;