deba@2420: /* -*- C++ -*- deba@2420: * deba@2420: * This file is a part of LEMON, a generic C++ optimization library deba@2420: * deba@2420: * Copyright (C) 2003-2007 deba@2420: * Egervary Jeno Kombinatorikus Optimalizalasi Kutatocsoport deba@2420: * (Egervary Research Group on Combinatorial Optimization, EGRES). deba@2420: * deba@2420: * Permission to use, modify and distribute this software is granted deba@2420: * provided that this copyright notice appears in all copies. For deba@2420: * precise terms see the accompanying LICENSE file. deba@2420: * deba@2420: * This software is provided "AS IS" with no warranty of any kind, deba@2420: * express or implied, and with no claim as to its suitability for any deba@2420: * purpose. deba@2420: * deba@2420: */ deba@2420: deba@2420: /// \ingroup demos deba@2420: /// \file deba@2420: /// \brief Solver for SAT-2 problems. deba@2420: /// deba@2420: /// This demo progam solves the SAT-2 problem, i.e. the boolean deba@2420: /// satisfiability problem where each disjuction consists at most 2 deba@2420: /// terms. deba@2420: /// deba@2420: /// The program generates a graph from the boolean expression. Two deba@2420: /// nodes are assigned to each boolean variable, an x and a deba@2420: /// not x nodes. If there is an x or y disjunction deba@2420: /// in the formula, then the not x => y and the not y => deba@2420: /// x edges are added to the graph. If there is a single deba@2420: /// x term disjunction in the formula then the not x deba@2420: /// =>x edge is added to the graph. deba@2420: /// deba@2420: /// The boolean formula could be satified if and only if the deba@2420: /// x and not x nodes are in different strongly connected deba@2420: /// components. A feasible solution could be get from the current deba@2420: /// component numbering. deba@2420: /// deba@2420: /// \include sat-2.cc deba@2420: deba@2420: #include deba@2420: #include deba@2420: #include deba@2420: #include deba@2420: #include deba@2420: deba@2420: #include deba@2420: #include deba@2420: deba@2420: using namespace std; deba@2420: using namespace lemon; deba@2420: deba@2420: deba@2420: int main(int argc, const char *argv[]) { deba@2420: if (argc != 2) { deba@2420: std::cerr << "The SAT-2 solver demo" << std::endl << std::endl; deba@2420: std::cerr << "The parameter should be a filename" << std::endl; deba@2420: std::cerr << "Each line of the file should contain a bool expression:" deba@2420: << std::endl; deba@2420: std::cerr << " [not] [or [not] ]" << std::endl; deba@2420: std::cerr << "The program prints a feasible solution if it exists" deba@2420: << std::endl; deba@2420: return -1; deba@2420: } deba@2420: ifstream is(argv[1]); deba@2420: deba@2420: SmartGraph graph; deba@2420: map > var; deba@2420: deba@2420: string line; deba@2420: while (getline(is, line)) { deba@2420: istringstream ls(line); deba@2420: string var1, var2, op; deba@2420: bool neg1 = false, neg2 = false; deba@2420: deba@2420: ls >> var1; deba@2420: if (var1 == "not") { deba@2420: neg1 = true; deba@2420: ls >> var1; deba@2420: } deba@2420: if (ls >> op) { deba@2420: if (op != "or") { deba@2420: cerr << "Wrong bool expression" << std::endl; deba@2420: return -1; deba@2420: } else { deba@2420: ls >> var2; deba@2420: if (var2 == "not") { deba@2420: neg2 = true; deba@2420: ls >> var2; deba@2420: } deba@2420: } deba@2420: if (ls >> op) { deba@2420: cerr << "Wrong bool expression" << std::endl; deba@2420: return -1; deba@2420: } deba@2420: deba@2420: map >::iterator it1; deba@2420: map >::iterator it2; deba@2420: it1 = var.find(var1); deba@2420: if (it1 == var.end()) { deba@2420: SmartGraph::Node node = graph.addNode(); deba@2420: SmartGraph::Node negNode = graph.addNode(); deba@2420: it1 = var.insert(make_pair(var1, make_pair(node, negNode))).first; deba@2420: } deba@2420: deba@2420: it2 = var.find(var2); deba@2420: if (it2 == var.end()) { deba@2420: SmartGraph::Node node = graph.addNode(); deba@2420: SmartGraph::Node negNode = graph.addNode(); deba@2420: it2 = var.insert(make_pair(var2, make_pair(node, negNode))).first; deba@2420: } deba@2420: deba@2420: graph.addEdge(neg1 ? it1->second.first : it1->second.second, deba@2420: neg2 ? it2->second.second : it2->second.first); deba@2420: deba@2420: graph.addEdge(neg2 ? it2->second.first : it2->second.second, deba@2420: neg1 ? it1->second.second : it1->second.first); deba@2420: } else { deba@2420: deba@2420: map >::iterator it1; deba@2420: it1 = var.find(var1); deba@2420: if (it1 == var.end()) { deba@2420: SmartGraph::Node node = graph.addNode(); deba@2420: SmartGraph::Node negNode = graph.addNode(); deba@2420: it1 = var.insert(make_pair(var1, make_pair(node, negNode))).first; deba@2420: } deba@2420: graph.addEdge(neg1 ? it1->second.first : it1->second.second, deba@2420: neg1 ? it1->second.second : it1->second.first); deba@2420: deba@2420: } deba@2420: deba@2420: } deba@2420: deba@2420: SmartGraph::NodeMap comp(graph); deba@2420: deba@2420: stronglyConnectedComponents(graph, comp); deba@2420: deba@2420: for (map >::iterator deba@2420: it = var.begin(); it != var.end(); ++it) { deba@2420: if (comp[it->second.first] == comp[it->second.second]) { deba@2420: std::cout << "There is no feasible solution." << std::endl; deba@2420: return 0; deba@2420: } deba@2420: } deba@2420: deba@2420: for (map >::iterator deba@2420: it = var.begin(); it != var.end(); ++it) { deba@2420: if (comp[it->second.first] < comp[it->second.second]) { deba@2420: std::cout << it->first << " = false " << std::endl; deba@2420: } else { deba@2420: std::cout << it->first << " = true " << std::endl; deba@2420: } deba@2420: } deba@2420: deba@2420: return 0; deba@2420: }