sat-2.cc File Reference

---

Detailed Description

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 x and a not x nodes. If there is an x or y disjunction in the formula, then the not x => y and the not y => x edges are added to the graph. If there is a single x term disjunction in the formula then the not x =>x edge is added to the graph.

The boolean formula could be satified if and only if the x and not x nodes are in different strongly connected components. A feasible solution could be get from the current component numbering.

/* -*- C++ -*-
 *
 * This file is a part of LEMON, a generic C++ optimization library
 *
 * Copyright (C) 2003-2008
 * 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.
 *
 */


#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;
}

#include <iostream>
#include <fstream>
#include <sstream>
#include <string>
#include <map>
#include <lemon/smart_graph.h>
#include <lemon/topology.h>