[Lemon-commits] deba: r3256 - lemon/trunk/demo
Lemon SVN
svn at lemon.cs.elte.hu
Wed Apr 18 18:34:41 CEST 2007
Author: deba
Date: Wed Apr 18 18:34:40 2007
New Revision: 3256
Added:
lemon/trunk/demo/sat-2.cc
lemon/trunk/demo/sat.cc
Modified:
lemon/trunk/demo/Makefile.am
Log:
Demo program for SAT problems
Modified: lemon/trunk/demo/Makefile.am
==============================================================================
--- lemon/trunk/demo/Makefile.am (original)
+++ lemon/trunk/demo/Makefile.am Wed Apr 18 18:34:40 2007
@@ -13,7 +13,8 @@
demo/strongly_connected_orientation.lgf \
demo/sub_gad_input.lgf \
demo/u_components.lgf \
- demo/steiner.lgf
+ demo/steiner.lgf \
+ demo/sat-2.in
if WANT_DEMO
@@ -40,7 +41,9 @@
demo/simann_maxcut_demo \
demo/disjoint_paths_demo \
demo/strongly_connected_orientation \
- demo/steiner_demo
+ demo/steiner_demo \
+ demo/sat-2 \
+ demo/sat
if HAVE_GLPK
noinst_PROGRAMS += demo/lp_demo demo/lp_maxflow_demo demo/mip_demo
@@ -107,4 +110,8 @@
demo_strongly_connected_orientation_SOURCES = demo/strongly_connected_orientation.cc
-demo_steiner_demo_SOURCES=demo/steiner_demo.cc
\ No newline at end of file
+demo_steiner_demo_SOURCES=demo/steiner_demo.cc
+
+demo_sat_2_SOURCES=demo/sat-2.cc
+
+demo_sat_SOURCES=demo/sat.cc
\ No newline at end of file
Added: lemon/trunk/demo/sat-2.cc
==============================================================================
--- (empty file)
+++ lemon/trunk/demo/sat-2.cc Wed Apr 18 18:34:40 2007
@@ -0,0 +1,157 @@
+/* -*- C++ -*-
+ *
+ * This file is a part of LEMON, a generic C++ optimization library
+ *
+ * Copyright (C) 2003-2007
+ * Egervary Jeno Kombinatorikus Optimalizalasi Kutatocsoport
+ * (Egervary Research Group on Combinatorial Optimization, EGRES).
+ *
+ * Permission to use, modify and distribute this software is granted
+ * provided that this copyright notice appears in all copies. For
+ * precise terms see the accompanying LICENSE file.
+ *
+ * This software is provided "AS IS" with no warranty of any kind,
+ * express or implied, and with no claim as to its suitability for any
+ * purpose.
+ *
+ */
+
+/// \ingroup demos
+/// \file
+/// \brief Solver for SAT-2 problems.
+///
+/// This demo progam solves the SAT-2 problem, i.e. the boolean
+/// satisfiability problem where each disjuction consists at most 2
+/// terms.
+///
+/// The program generates a graph from the boolean expression. Two
+/// nodes are assigned to each boolean variable, an <tt>x</tt> and a
+/// <tt>not x</tt> nodes. If there is an <tt>x or y</tt> disjunction
+/// in the formula, then the <tt>not x => y</tt> and the <tt>not y =>
+/// x</tt> edges are added to the graph. If there is a single
+/// <tt>x</tt> term disjunction in the formula then the <tt>not x
+/// =>x</tt> edge is added to the graph.
+///
+/// The boolean formula could be satified if and only if the
+/// <tt>x</tt> and <tt>not x</tt> nodes are in different strongly connected
+/// components. A feasible solution could be get from the current
+/// component numbering.
+///
+/// \include sat-2.cc
+
+#include <iostream>
+#include <fstream>
+#include <sstream>
+#include <string>
+#include <map>
+
+#include <lemon/smart_graph.h>
+#include <lemon/topology.h>
+
+using namespace std;
+using namespace lemon;
+
+
+int main(int argc, const char *argv[]) {
+ if (argc != 2) {
+ std::cerr << "The SAT-2 solver demo" << std::endl << std::endl;
+ std::cerr << "The parameter should be a filename" << std::endl;
+ std::cerr << "Each line of the file should contain a bool expression:"
+ << std::endl;
+ std::cerr << " [not] <variable> [or [not] <variable>]" << std::endl;
+ std::cerr << "The program prints a feasible solution if it exists"
+ << std::endl;
+ return -1;
+ }
+ ifstream is(argv[1]);
+
+ SmartGraph graph;
+ map<string, pair<SmartGraph::Node, SmartGraph::Node> > var;
+
+ string line;
+ while (getline(is, line)) {
+ istringstream ls(line);
+ string var1, var2, op;
+ bool neg1 = false, neg2 = false;
+
+ ls >> var1;
+ if (var1 == "not") {
+ neg1 = true;
+ ls >> var1;
+ }
+ if (ls >> op) {
+ if (op != "or") {
+ cerr << "Wrong bool expression" << std::endl;
+ return -1;
+ } else {
+ ls >> var2;
+ if (var2 == "not") {
+ neg2 = true;
+ ls >> var2;
+ }
+ }
+ if (ls >> op) {
+ cerr << "Wrong bool expression" << std::endl;
+ return -1;
+ }
+
+ map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it1;
+ map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it2;
+ it1 = var.find(var1);
+ if (it1 == var.end()) {
+ SmartGraph::Node node = graph.addNode();
+ SmartGraph::Node negNode = graph.addNode();
+ it1 = var.insert(make_pair(var1, make_pair(node, negNode))).first;
+ }
+
+ it2 = var.find(var2);
+ if (it2 == var.end()) {
+ SmartGraph::Node node = graph.addNode();
+ SmartGraph::Node negNode = graph.addNode();
+ it2 = var.insert(make_pair(var2, make_pair(node, negNode))).first;
+ }
+
+ graph.addEdge(neg1 ? it1->second.first : it1->second.second,
+ neg2 ? it2->second.second : it2->second.first);
+
+ graph.addEdge(neg2 ? it2->second.first : it2->second.second,
+ neg1 ? it1->second.second : it1->second.first);
+ } else {
+
+ map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator it1;
+ it1 = var.find(var1);
+ if (it1 == var.end()) {
+ SmartGraph::Node node = graph.addNode();
+ SmartGraph::Node negNode = graph.addNode();
+ it1 = var.insert(make_pair(var1, make_pair(node, negNode))).first;
+ }
+ graph.addEdge(neg1 ? it1->second.first : it1->second.second,
+ neg1 ? it1->second.second : it1->second.first);
+
+ }
+
+ }
+
+ SmartGraph::NodeMap<int> comp(graph);
+
+ stronglyConnectedComponents(graph, comp);
+
+ for (map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator
+ it = var.begin(); it != var.end(); ++it) {
+ if (comp[it->second.first] == comp[it->second.second]) {
+ std::cout << "There is no feasible solution." << std::endl;
+ return 0;
+ }
+ }
+
+ for (map<string, pair<SmartGraph::Node, SmartGraph::Node> >::iterator
+ it = var.begin(); it != var.end(); ++it) {
+ if (comp[it->second.first] < comp[it->second.second]) {
+ std::cout << it->first << " = false " << std::endl;
+ } else {
+ std::cout << it->first << " = true " << std::endl;
+ }
+ }
+
+ return 0;
+}
Added: lemon/trunk/demo/sat.cc
==============================================================================
--- (empty file)
+++ lemon/trunk/demo/sat.cc Wed Apr 18 18:34:40 2007
@@ -0,0 +1,115 @@
+/* -*- C++ -*-
+ *
+ * This file is a part of LEMON, a generic C++ optimization library
+ *
+ * Copyright (C) 2003-2007
+ * Egervary Jeno Kombinatorikus Optimalizalasi Kutatocsoport
+ * (Egervary Research Group on Combinatorial Optimization, EGRES).
+ *
+ * Permission to use, modify and distribute this software is granted
+ * provided that this copyright notice appears in all copies. For
+ * precise terms see the accompanying LICENSE file.
+ *
+ * This software is provided "AS IS" with no warranty of any kind,
+ * express or implied, and with no claim as to its suitability for any
+ * purpose.
+ *
+ */
+
+/// \ingroup demos
+/// \file
+/// \brief Solver for SAT problems.
+///
+/// This demo progam solves the SAT problem, i.e. the boolean
+/// satisfiability problem. The problem in general case is
+/// NP-complete.
+///
+/// The program uses an integer linear program solver. A <tt>{0,
+/// 1}</tt> variable is assigned to each boolean variable. The
+/// disjunctions are converted to linear inequalities as each negation
+/// is replaced with a substraction from one and each disjunction is
+/// converted to addition. The generated linear expression should be
+/// at least one.
+///
+/// \include sat.cc
+
+#include <iostream>
+#include <fstream>
+#include <sstream>
+#include <string>
+
+#include <lemon/lp.h>
+
+using namespace std;
+using namespace lemon;
+
+
+int main(int argc, const char *argv[]) {
+ if (argc != 2) {
+ std::cerr << "The SAT solver demo" << std::endl << std::endl;
+ std::cerr << "The parameter should be a filename" << std::endl;
+ std::cerr << "Each line of the file should contain a bool expression:"
+ << std::endl;
+ std::cerr << " [not] <variable> [or [not] <variable>]..." << std::endl;
+ std::cerr << "The program prints a feasible solution if it exists"
+ << std::endl;
+ return -1;
+ }
+ ifstream is(argv[1]);
+
+ Mip mip;
+ mip.max();
+ mip.obj(0);
+
+ string line;
+ while (getline(is, line)) {
+ istringstream ls(line);
+
+ Mip::Expr expr;
+
+
+ string op;
+ do {
+ string var;
+ bool neg = false;
+
+ ls >> var;
+ if (var == "not") {
+ neg = true;
+ ls >> var;
+ }
+
+ Mip::Col col = mip.colByName(var);
+
+ if (col == INVALID) {
+ col = mip.addCol();
+ mip.colName(col, var);
+ mip.colLowerBound(col, 0);
+ mip.colUpperBound(col, 1);
+ mip.integer(col, true);
+ }
+
+ expr += (neg ? 1 - col : col);
+
+ } while (ls >> op && op == "or");
+ if (ls) {
+ std::cerr << "Wrong bool expression" << std::endl;
+ return -1;
+ }
+ mip.addRow(expr >= 1);
+ }
+
+ mip.solve();
+
+ if (mip.mipStatus() == Mip::OPTIMAL) {
+ for (Mip::ColIt it(mip); it != INVALID; ++it) {
+ std::cout << mip.colName(it) << " = "
+ << (mip.primal(it) == 1 ? "true" : "false")
+ << std::endl;
+ }
+ } else {
+ std::cout << "There is no feasible solution." << std::endl;
+ }
+
+ return 0;
+}
More information about the Lemon-commits
mailing list