OKlibrary  0.2.1.6
LexicographicalEvaluation.hpp
Go to the documentation of this file.
00001 // Oliver Kullmann, 25.10.2005 (Swansea)
00002 /* Copyright 2005 - 2007 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 
00018 #ifndef LEXICOGRAPHICALEVALUATION_9fsfs41917
00019 #define LEXICOGRAPHICALEVALUATION_9fsfs41917
00020 
00021 #include <map>
00022 #include <utility>
00023 #include <vector>
00024 #include <algorithm>
00025 #include <cassert>
00026 #include <ostream>
00027 #include <iterator>
00028 #include <string>
00029 #include <ios>
00030 #include <iomanip>
00031 
00032 #include <boost/functional.hpp>
00033 
00034 #include <OKlib/Structures/Sets/SetAlgorithms/BasicMapOperations.hpp>
00035 #include <OKlib/Programming/Utilities/OrderRelations/DerivedRelations.hpp>
00036 
00037 #include <OKlib/Experimentation/Competition/SingleResult.hpp>
00038 #include <OKlib/Experimentation/Competition/AnalysisTools.hpp>
00039 
00040 #include <OKlib/Experimentation/Competition/LexicographicalEvaluationPolicies.hpp>
00041 
00042 namespace OKlib {
00043   namespace SATCompetition {
00044 
00062     template <class IndexedDatabase, class SeriesPolicy = LexicographicalSeriesPolicy<Result>, typename NumberType = double>
00063     class LexicographicalEvaluation {
00064     public :
00065 
00066       typedef IndexedDatabase database_type;
00067       typedef NumberType number_type;
00068 
00069     private :
00070 
00071       typedef typename database_type::seq_solved_benchmarks seq_solved_benchmarks;
00072 
00073     public :
00074 
00075       typedef typename seq_solved_benchmarks::size_type size_type;
00076 
00077       struct numerics_solver_on_series_type {
00078         typedef size_type first_type;
00079         typedef number_type second_type;
00080         size_type first;
00081         number_type second;
00082         numerics_solver_on_series_type() : first(0), second(0) {}
00083         numerics_solver_on_series_type(const size_type first, const number_type second) : first(first), second(second) {}
00084       };
00085       friend bool operator ==(const numerics_solver_on_series_type& lhs, const numerics_solver_on_series_type& rhs) {
00086         return lhs.first == rhs.first and (lhs.first == 0 or lhs.second == rhs.second);
00087       }
00088       friend bool operator <(const numerics_solver_on_series_type& lhs, const numerics_solver_on_series_type& rhs) {
00089         return lhs.first > rhs.first or (lhs.first == rhs.first and lhs.first != 0 and lhs.second < rhs.second);
00090       }
00091       // a < b for a, b of type numerics_solver_on_series_type means "a is better than b"
00092       OKLIB_DERIVED_RELATIONS_FRIENDS(numerics_solver_on_series_type);
00093       friend std::ostream& operator <<(std::ostream& out, const numerics_solver_on_series_type& pair) {
00094         const std::streamsize field_width_count = 3;
00095         out.width(field_width_count);
00096         out << pair.first << ":";
00097         const std::streamsize field_width_time = 5;
00098         out.width(field_width_time);
00099         if (pair.first != 0) {
00100           const std::streamsize old_precision(out.precision());
00101           const std::streamsize new_precision_time = (pair.second < 10) ? 1 : 0;
00102           out.precision(new_precision_time);
00103           out << pair.second;
00104           out.precision(old_precision);
00105         }
00106         else
00107           out << "NaN";
00108         return out;
00109       }
00110 
00111       typedef typename SeriesPolicy::super_series_type super_series_type;
00112       typedef typename SeriesPolicy::series_type series_type;
00113       typedef std::map<series_type, numerics_solver_on_series_type> map_series_numerics_type;
00114       typedef std::map<super_series_type, map_series_numerics_type> map_solver_evaluation_type;
00115 
00116       const database_type& idb;
00117 
00118       LexicographicalEvaluation(const IndexedDatabase& idb) : idb(idb) {
00119 
00120         typedef typename database_type::map_solver_benchmarks map_solver_benchmarks;
00121         typedef typename map_solver_benchmarks::const_iterator iterator;
00122         const map_solver_benchmarks& solver_benchmarks(idb.solved_benchmarks());
00123         const iterator& end(solver_benchmarks.end());
00124         for (iterator i(solver_benchmarks.begin()); i != end; ++i) { // loop over all solvers
00125           const Solver& solver(i -> first);
00126           typedef typename database_type::seq_solved_benchmarks seq_solved_benchmarks;
00127           const seq_solved_benchmarks& solved_benchmarks(i -> second);
00128           map_solver_evaluation_type result_map;
00129 
00130           {
00131             typedef typename seq_solved_benchmarks::const_iterator iterator;
00132             const iterator& end(solved_benchmarks.end());
00133             for (iterator j(solved_benchmarks.begin()); j != end; ++j) { // loop over all solved benchs
00134               typedef typename database_type::SolvedBenchmark solved_benchmark_type;
00135               const solved_benchmark_type& solved_bench(*j);
00136               const super_series_type& super_series(SeriesPolicy::super_series(solved_bench));
00137               const series_type& series(SeriesPolicy::series(solved_bench));
00138               numerics_solver_on_series_type& ref(result_map[super_series][series]);
00139               ++ref.first;
00140               ref.second += solved_bench.node -> rb -> average().average();
00141             }
00142           }
00143           {
00144             typedef typename map_solver_evaluation_type::iterator iterator;
00145             const iterator& end(result_map.end());
00146             for (iterator j(result_map.begin()); j != end; ++j) {
00147               map_series_numerics_type& ref(j -> second);
00148               typedef typename map_series_numerics_type::iterator iterator2;
00149               const iterator2& end2(ref.end());
00150               for (iterator2 k(ref.begin()); k != end2; ++k) {
00151                 numerics_solver_on_series_type& ref2(k -> second);
00152                 assert(ref2.first > 0);
00153                 ref2.second /= ref2.first;
00154               }
00155             }
00156             map.insert(std::make_pair(solver, result_map));
00157           }
00158 
00159         }
00160       }
00161 
00162       const map_solver_evaluation_type& evaluation(const Solver& solver) const {
00163         return OKlib::SetAlgorithms::map_value(map, solver);
00164       }
00165 
00166     public : // ToDo: Design
00167 
00168       typedef std::map<Solver, map_solver_evaluation_type> map_solver_map_evaluation_type;
00169       map_solver_map_evaluation_type map;
00170       
00171     };
00172 
00173     // ###########################################################
00174 
00183     template <class IndexedDatabase, template <class solver_evaluation_pair_type> class SortingPolicy = LexicographicalSortingPolicy_unfolded_lexicographical, typename NumberType = double>
00184     class LexicographicalEvaluationRandom {
00185     public :
00186 
00187       typedef IndexedDatabase database_type;
00188       typedef NumberType number_type;
00189 
00190       typedef LexicographicalEvaluation<database_type, LexicographicalSeriesPolicy<ResultRandomSat>, number_type> lexicographical_evaluation_type;
00191       typedef typename lexicographical_evaluation_type::numerics_solver_on_series_type numerics_solver_on_series_type;
00192       typedef typename lexicographical_evaluation_type::size_type size_type;
00193 
00194       typedef std::vector<numerics_solver_on_series_type> evaluation_vector_type;
00195       typedef std::pair<Solver, evaluation_vector_type> solver_evaluation_pair_type;
00196 
00197       typedef typename SortingPolicy<solver_evaluation_pair_type>::comparison_type comparison_type;
00198       typedef std::set<solver_evaluation_pair_type, comparison_type> set_of_evaluations_type;
00199 
00200       const database_type& idb;
00201 
00202       LexicographicalEvaluationRandom(const IndexedDatabase& idb) : idb(idb) {
00203         lexicographical_evaluation_type eval(idb);
00204         typedef typename lexicographical_evaluation_type::map_solver_map_evaluation_type map_solver_map_evaluation_type;
00205         const map_solver_map_evaluation_type& map_solver(eval.map);
00206         typedef typename map_solver_map_evaluation_type::const_iterator iterator_solver;
00207         const iterator_solver& solver_end(map_solver.end());
00208 
00209         typedef typename database_type::map_superseries_series map_superseries_series;
00210         const map_superseries_series& map_superseries(idb.series_in_superseries());
00211         typedef typename map_superseries_series::const_iterator iterator;
00212         const iterator& end(map_superseries.end());
00213         for (iterator i = map_superseries.begin(); i != end; ++i) {
00214           const SuperSeries& super_series(i -> first);
00215           const RandomKSat& random_k_sat(get_derived_super_series(super_series));
00216           set_of_evaluations_type& set(map[random_k_sat]);
00217           
00218           typedef typename database_type::seq_series seq_series_type;
00219           const seq_series_type& seq_series(i -> second);
00220 
00221           typedef std::vector<RandomKSat_n> hash_map_type;
00222           hash_map_type hash_map;
00223           hash_map.reserve(seq_series.size());
00224           {
00225             typedef typename seq_series_type::const_iterator iterator;
00226             const iterator& end(seq_series.end());
00227             for (iterator i = seq_series.begin(); i != end; ++i)
00228               hash_map.push_back(get_derived_series(*i));
00229           }
00230           std::sort(hash_map.begin(), hash_map.end(), sort_by_n());
00231           assert(std::adjacent_find(hash_map.begin(), hash_map.end(), boost::not2(sort_by_n())) == hash_map.end());
00232 
00233           for (iterator_solver j(map_solver.begin()); j != solver_end; ++j) {
00234             const Solver& solver(j -> first);
00235             evaluation_vector_type evaluation_vector(hash_map.size());
00236             typedef typename lexicographical_evaluation_type::map_solver_evaluation_type map_solver_evaluation_type;
00237             const map_solver_evaluation_type map_solver_all_evaluations(j -> second);
00238             {
00239               typedef typename evaluation_vector_type::iterator iterator;
00240               const iterator& end(evaluation_vector.end());
00241               for (iterator i(evaluation_vector.begin()); i != end; ++i)
00242                 i -> first = 0;
00243             }
00244             {
00245               typedef typename map_solver_evaluation_type::const_iterator iterator_map_solver_evaluation;
00246               const iterator_map_solver_evaluation& aux(map_solver_all_evaluations.find(random_k_sat));
00247               if (aux == map_solver_all_evaluations.end()) continue;
00248               assert(aux != map_solver_all_evaluations.end());
00249               typedef typename lexicographical_evaluation_type::map_series_numerics_type map_series_numerics_type;
00250               const map_series_numerics_type& map_solver_evaluations(aux -> second);
00251               typedef typename map_series_numerics_type::const_iterator iterator_map_series_numerics;
00252               const iterator_map_series_numerics& end(map_solver_evaluations.end());
00253               for (iterator_map_series_numerics k(map_solver_evaluations.begin()); k != end; ++k) {
00254                 const RandomKSat_n& random_k_sat_n(k -> first);
00255                 {
00256                   const typename hash_map_type::iterator& found(std::lower_bound(hash_map.begin(), hash_map.end(), random_k_sat_n, sort_by_n()));
00257                   assert(found != hash_map.end());
00258                   const typename hash_map_type::iterator::difference_type& index(found - hash_map.begin());
00259                   assert(index >= 0);
00260                   assert((typename hash_map_type::size_type)index < hash_map.size());
00261                   evaluation_vector[index] = k -> second;
00262                   assert(*found == random_k_sat_n);
00263                 }
00264               }
00265             }
00266 
00267             set.insert(solver_evaluation_pair_type(solver, evaluation_vector));
00268           }
00269         }
00270       }
00271 
00272       const set_of_evaluations_type& evaluation(const SuperSeries& super_series) const {
00273         return OKlib::SetAlgorithms::map_value(map, super_series);
00274       }
00275 
00276     public : // ToDo: Design
00277 
00278       typedef std::map<RandomKSat, set_of_evaluations_type> map_super_series_to_evaluations_type;
00279       map_super_series_to_evaluations_type map;
00280 
00281       void print(std::ostream& out) const {
00282         const bool fixed = out.flags() & std::ios_base::fixed; // ToDo: RAII
00283         if (not fixed)
00284           out.setf(std::ios_base::fixed);
00285         typedef typename map_super_series_to_evaluations_type::const_iterator iterator;
00286         const iterator& end(map.end());
00287         for (iterator i = map.begin(); i != end; ++i) {
00288           print(out, *i);
00289           out << "\n";
00290         }
00291         if (not fixed)
00292           out.unsetf(std::ios_base::fixed);
00293       }
00294     private :
00295 
00296       typedef typename map_super_series_to_evaluations_type::value_type value_type;
00297 
00298       static void print(std::ostream& out, const value_type& pair) {
00299         out << pair.first << "\t:\n\n";
00300         print(out, pair.second);
00301         out << "\n";
00302       }
00303       static void print(std::ostream& out, const set_of_evaluations_type& set) {
00304         typedef typename set_of_evaluations_type::const_iterator iterator;
00305         const iterator& end(set.end());
00306         for (iterator i = set.begin(); i != end; ++i) {
00307           print(out, *i);
00308           out << "\n";
00309         }
00310       }
00311       static void print(std::ostream& out, const solver_evaluation_pair_type& pair) {
00312         const std::streamsize field_width_solvers(6 + 3);
00313         out.width(field_width_solvers);
00314         out << std::left << pair.first <<std::right << "\t:\t";
00315         print(out, pair.second);
00316         out << "\n";
00317       }
00318       static void print(std::ostream& out, const evaluation_vector_type& vec) {
00319         std::copy(vec.begin(), vec.end(), std::ostream_iterator<numerics_solver_on_series_type>(out, " | "));
00320       }
00321 
00322 
00323       RandomKSat get_derived_super_series(const SuperSeries& s) {
00324         return (static_cast<const ResultRandomSat*>((*OKlib::SetAlgorithms::map_value(idb.db.super_series(), s) -> begin()) -> rb)) -> super_series_random();
00325       }
00326       RandomKSat_n get_derived_series(const Series& s) {
00327         return (static_cast<const ResultRandomSat*>((*OKlib::SetAlgorithms::map_value(idb.db.series(), s) -> begin()) -> rb)) -> series_random();
00328       }
00329 
00330       struct sort_by_n : std::binary_function<const RandomKSat_n&, const RandomKSat_n&, bool> {
00331         bool operator() (const RandomKSat_n& lhs, const RandomKSat_n& rhs) const {
00332           return lhs.count_variables() > rhs.count_variables();
00333         }
00334       };
00335 
00336     };
00337 
00338     // ###########################################################
00339 
00340     template <template <typename CharT, typename ParseIterator> class ParserExtension = ParserEmpty>
00341     struct LexicographicalEvaluationRandom_from_file {
00342 
00343       typedef ResultRandomSat result_type;
00344       typedef Result_database_from_file<ParserResult, result_type, ParserExtension> result_database_from_file;
00345       typedef typename result_database_from_file::database_type database;
00346       typedef ElementaryAnalysis<database> indexed_database;
00347 
00348       typedef LexicographicalEvaluationRandom<indexed_database> lexicographical_evaluation_unfolded_type;
00349       typedef LexicographicalEvaluationRandom<indexed_database, LexicographicalSortingPolicy_induced_lexicographical> lexicographical_evaluation_induced_type;
00350 
00351       result_database_from_file rdb;
00352       database rdb_sat;
00353       database rdb_unsat;
00354 
00355       bool dummy;
00356 
00357       indexed_database idb_all, idb_sat, idb_unsat;
00358 
00359       lexicographical_evaluation_unfolded_type evaluation_unfolded_all;
00360       lexicographical_evaluation_unfolded_type evaluation_unfolded_sat;
00361       lexicographical_evaluation_unfolded_type evaluation_unfolded_unsat;
00362 
00363       lexicographical_evaluation_induced_type evaluation_induced_all;
00364       lexicographical_evaluation_induced_type evaluation_induced_sat;
00365       lexicographical_evaluation_induced_type evaluation_induced_unsat;
00366 
00367       LexicographicalEvaluationRandom_from_file(const std::string& file_name)  : rdb(file_name), rdb_sat(rdb.db), rdb_unsat(rdb.db), dummy(restrict_database()),  idb_all(rdb.db), idb_sat(rdb_sat), idb_unsat(rdb_unsat), evaluation_unfolded_all(idb_all),  evaluation_unfolded_sat(idb_sat), evaluation_unfolded_unsat(idb_unsat), evaluation_induced_all(idb_all),  evaluation_induced_sat(idb_sat), evaluation_induced_unsat(idb_unsat) {
00368         assert(dummy);
00369       }
00370 
00371     private :
00372 
00373       bool restrict_database() {
00374         rdb_sat.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb_sat.sat_status(), SATStatus(sat)));
00375         rdb_sat.intersection();
00376         rdb_sat.restrict();
00377         rdb_unsat.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb_unsat.sat_status(), SATStatus(unsat)));
00378         rdb_unsat.intersection();
00379         rdb_unsat.restrict();
00380         return true;
00381       }
00382 
00383     };
00384 
00385   }
00386 
00387 }
00388 
00389 #endif