OKlibrary  0.2.1.6
QuineMcCluskeySubsumptionHypergraph-n16.cpp
Go to the documentation of this file.
00001 // Matthew Gwynne, 5.10.2010 (Swansea)
00002 /* Copyright 2010, 2011 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00023 #include <fstream>
00024 #include <iostream>
00025 #include <string>
00026 #include <algorithm>
00027 
00028 #include <boost/filesystem/path.hpp>
00029 
00030 #include <OKlib/Satisfiability/Interfaces/InputOutput/Dimacs.hpp>
00031 #include <OKlib/Satisfiability/Interfaces/InputOutput/ClauseSetAdaptors.hpp>
00032 #include <OKlib/Satisfiability/FiniteFunctions/QuineMcCluskey.hpp>
00033 #include <OKlib/Structures/Sets/SetAlgorithms/SubsumptionHypergraph.hpp>
00034 
00035 namespace {
00036   
00037 #ifdef NUMBER_VARIABLES
00038   const int num_vars = NUMBER_VARIABLES;
00039 #else
00040   const int num_vars = 4;
00041 #endif
00042 
00043   enum {
00044     error_parameters = 1,
00045     error_openfile = 2
00046   };
00047 
00048   const std::string program = "QuineMcCluskeySubsumptionHypergraph";
00049   const std::string err = "ERROR[" + program + "]: ";
00050 
00051   const std::string version = "0.2.1";
00052 
00053 }
00054 
00055 int main(const int argc, const char* const argv[]) {
00056 
00057   if (argc != 2) {
00058     std::cerr << err << "Exactly one input is required,\n"
00059       " the name of the file with the clause-set in DIMACS-format.\n"
00060       "However, the actual number of input parameters was " << argc-1 << ".\n";
00061     return error_parameters;
00062   }
00063 
00064   const std::string shg_input_filepath = argv[1];
00065   std::ifstream shg_inputfile(shg_input_filepath.c_str());
00066   if (not shg_inputfile) {
00067     std::cerr << err << "Failure opening input file " << shg_input_filepath << ".\n";
00068     return error_openfile;
00069   }
00070 
00071   typedef OKlib::InputOutput::RawDimacsCLSAdaptor<> CLSAdaptor;
00072   CLSAdaptor cls_F;
00073   typedef OKlib::InputOutput::StandardDIMACSInput<CLSAdaptor> CLSInput;
00074   const CLSInput input_F(shg_inputfile, cls_F);
00075   shg_inputfile.close();
00076 
00077   // Compute the prime clauses:
00078   typedef OKlib::Satisfiability::FiniteFunctions::QuineMcCluskey<num_vars>::clause_set_type clause_set_type;
00079   const clause_set_type prime_imp_F = OKlib::Satisfiability::FiniteFunctions::quine_mccluskey<num_vars>(cls_F.clause_set);
00080 
00081   // Compute the subsumption hypergraph:
00082   typedef OKlib::SetAlgorithms::Subsumption_hypergraph<clause_set_type, CLSAdaptor::clause_set_type>::set_system_type subsumption_hg_type;
00083   subsumption_hg_type subsumption_hg = 
00084     OKlib::SetAlgorithms::subsumption_hypergraph(prime_imp_F, cls_F.clause_set);
00085   std::sort(subsumption_hg.begin(), subsumption_hg.end());
00086   subsumption_hg.erase(std::unique(subsumption_hg.begin(), subsumption_hg.end()), subsumption_hg.end());
00087 
00088   // Output:
00089   const std::string comment1("Subsumption hypergraph for the minimisation problem for " + shg_input_filepath);
00090   OKlib::InputOutput::List2DIMACSOutput(subsumption_hg,std::cout,comment1.c_str());
00091   // Output of prime clauses if needed:
00092   const std::string primes_output_filepath = boost::filesystem::path(shg_input_filepath).filename().string() + "_primes";
00093   std::ofstream outputfile(primes_output_filepath.c_str());
00094   if (not outputfile) {
00095     std::cerr << err << "Failure opening output file " << primes_output_filepath << ".\n";
00096     return error_openfile;
00097   }
00098   const std::string comment2("All prime implicates for " + shg_input_filepath);
00099   OKlib::InputOutput::List2DIMACSOutput(prime_imp_F,outputfile,comment2.c_str());
00100 }