OKlibrary  0.2.1.6
Scoring.hpp
Go to the documentation of this file.
00001 // Oliver Kullmann, 17.6.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 
00013 #ifndef SCORING_567UyTr
00014 #define SCORING_567UyTr
00015 
00016 #include <algorithm>
00017 #include <cassert>
00018 #include <vector>
00019 #include <string>
00020 #include <ostream>
00021 #include <functional>
00022 
00023 #include <boost/format.hpp>
00024 
00025 #include <OKlib/General/IteratorHandling.hpp>
00026 
00027 #include <OKlib/Structures/Sets/SetAlgorithms/BasicMapOperations.hpp>
00028 #include <OKlib/Programming/Utilities/OrderRelations/DerivedRelations.hpp>
00029 
00030 #include <OKlib/Experimentation/Competition/SingleResult.hpp>
00031 #include <OKlib/Experimentation/Competition/ParsingSingleResult.hpp>
00032 #include <OKlib/Experimentation/Competition/ParsingResultSequences.hpp>
00033 #include <OKlib/Experimentation/Competition/ResultProcessing.hpp>
00034 #include <OKlib/Experimentation/Competition/AnalysisTools.hpp>
00035 
00036 namespace OKlib {
00037   namespace SATCompetition {
00038 
00043     struct ConstantSeriesPurse {
00044       template <typename Number, typename Int>
00045       static Number purse(const Number initial_purse, const Int count) {
00046         return initial_purse;
00047       }
00048     };
00054     struct SAT2005SeriesPurse {
00055       template <typename Number, typename Int>
00056       static Number purse(const Number initial_purse, const Int count) {
00057         const Int count_threshold = 5;
00058         if (count >= count_threshold)
00059           return initial_purse;
00060         else {
00061           const Number weight = Number(1) / Number(3);
00062           return weight * initial_purse;
00063         }
00064       }
00065     };
00066 
00067     // ###############
00068 
00076     template <class IndexedDatabase, class SeriesPursePolicy = SAT2005SeriesPurse, typename NumberType = double>
00077     class PurseScoring {
00078 
00079     public :
00080 
00081       const IndexedDatabase& idb;
00082 
00083       typedef NumberType number_type;
00084       typedef IndexedDatabase database_type;
00085       typedef SeriesPursePolicy series_policy_type;
00086 
00087       const number_type standard_problem_purse;
00088       const number_type standard_speed_factor;
00089       const number_type standard_series_factor;
00090 
00091       const number_type standard_speed_purse;
00092       const number_type standard_series_purse;
00093 
00094       PurseScoring(const IndexedDatabase& idb, const number_type standard_problem_purse = 1000, const number_type standard_speed_factor = 1, const number_type standard_series_factor = 3) :
00095         idb(idb), standard_problem_purse(standard_problem_purse), standard_speed_factor(standard_speed_factor), standard_series_factor(standard_series_factor), standard_speed_purse(standard_speed_factor * standard_problem_purse), standard_series_purse(standard_series_factor * standard_problem_purse) {}
00096 
00097       virtual ~PurseScoring() {}
00098       
00099       bool solved(const Solver& solver, const Benchmark& bench) const {
00100         return solved_(solver, bench);
00101       }
00102 
00103       bool solved(const Solver& solver, const SpecSeries& series) const {
00104         return solved_(solver, series);
00105       }
00106 
00107     private :
00108 
00109       typedef typename database_type::seq_solvers seq_solvers;
00110 
00111     public :
00112 
00113       typedef typename seq_solvers::size_type size_type_solvers;
00114 
00115       size_type_solvers solved(const Benchmark& bench) const {
00116         return solved_(bench);
00117       }
00118 
00119       size_type_solvers solved(const SpecSeries& series) const {
00120         return solved_(series);
00121       }
00122 
00123       number_type problem_purse(const Solver& solver, const Benchmark& bench) const {
00124         return problem_purse_(solver, bench);
00125       }
00126       number_type problem_purse(const Solver& solver) const {
00127         return problem_purse_(solver);
00128       }
00129 
00130       number_type speed_factor(const Solver& solver, const Benchmark& bench) const {
00131         return speed_factor_(solver, bench);
00132       }
00133       number_type speed_factor(const Benchmark& bench) const {
00134         return speed_factor_(bench);
00135       }
00136 
00137       number_type total_time(const Benchmark& bench) const {
00138         return total_time_(bench);
00139       }
00140       
00141       number_type speed_award(const Solver& solver, const Benchmark& bench) const {
00142         return speed_award_(solver, bench);
00143       }
00144       number_type speed_award(const Solver& solver) const {
00145         return speed_award_(solver);
00146       }
00147 
00148       number_type series_purse(const SpecSeries& series) const {
00149         return series_purse_(series);
00150       }
00151       number_type series_purse(const Solver& solver, const SpecSeries& series) const {
00152         return series_purse_(solver, series);
00153       }
00154       number_type series_purse(const Solver& solver) const {
00155         return series_purse_(solver);
00156       }
00157 
00158       number_type score(const Solver& solver) const {
00159         return score_(solver);
00160       }
00161 
00162     private :
00163 
00164       typedef typename database_type::seq_solved_benchmarks seq_solved_benchmarks;
00165       typedef typename seq_solved_benchmarks::size_type size_type_solved_benchmarks;
00166       typedef typename database_type::seq_benchmarks seq_benchmarks;
00167       typedef typename seq_benchmarks::size_type size_type_benchmarks;
00168 
00169 
00170       typedef typename database_type::seq_spec_series seq_spec_series;
00171 
00172       typedef typename database_type::SolvedBenchmark SolvedBenchmark;
00173 
00174       // --------------------------------------------------------------
00175 
00176       virtual bool solved_(const Solver& solver, const Benchmark& bench) const {
00177         const seq_solvers& seq(OKlib::SetAlgorithms::map_value(idb.succesful_solvers(), bench));
00178         return std::binary_search(seq.begin(), seq.end(), solver);
00179       }
00180 
00181       virtual bool solved_(const Solver& solver, const SpecSeries& series) const {
00182         const seq_spec_series& seq(OKlib::SetAlgorithms::map_value(idb.solved_series(), solver));
00183         return std::binary_search(seq.begin(), seq.end(), series);
00184       }
00185 
00186       virtual size_type_solvers solved_(const Benchmark& bench) const {
00187         const seq_solvers& seq(OKlib::SetAlgorithms::map_value(idb.succesful_solvers(), bench));
00188         const size_type_solvers& count(seq.size());
00189         return count;
00190       }
00191 
00192       virtual size_type_solvers solved_(const SpecSeries& series) const {
00193         size_type_solvers count = 0;
00194         typedef typename database_type::map_solver_benchmarks map_solver_benchmarks;
00195         typedef typename IteratorHandling::IteratorFirst<typename map_solver_benchmarks::const_iterator>::type iterator;
00196         const map_solver_benchmarks& map(idb.solved_benchmarks());
00197         const iterator end(map.end());
00198         for (iterator i(map.begin()); i != end; ++i) { // loop over all solvers
00199           const Solver& solver(*i);
00200             count += solved(solver, series);
00201           }
00202         return count;
00203       }
00204 
00205       // --------------------------------------------------------------
00206 
00207       virtual number_type problem_purse_(const Solver& solver, const Benchmark& bench) const {
00208         if (solved(solver, bench)) {
00209           const size_type_solvers& count(solved(bench));
00210           assert(count > 0);
00211           return standard_problem_purse / count;
00212         }
00213         else
00214           return 0;
00215       }
00216 
00217       virtual number_type problem_purse_(const Solver& solver) const {
00218         const seq_solved_benchmarks& seq(OKlib::SetAlgorithms::map_value(idb.solved_benchmarks(), solver));
00219         number_type sum = 0;
00220         typedef typename seq_solved_benchmarks::const_iterator iterator;
00221         const iterator end(seq.end());
00222         for (iterator i = seq.begin(); i != end; ++i) { // loop over all benchmarks the solver solved
00223           const Benchmark& bench(*i);
00224           sum += problem_purse(solver, bench);
00225         }
00226         return sum;
00227       }
00228 
00229       // --------------------------------------------------------------
00230 
00231       virtual number_type speed_factor_(const Solver& solver, const Benchmark& bench) const {
00232         if (solved(solver, bench)) {
00233           const seq_solved_benchmarks& seq(OKlib::SetAlgorithms::map_value(idb.solved_benchmarks(), solver));
00234           typedef typename seq_solved_benchmarks::const_iterator iterator;
00235           const iterator& solution_it(std::lower_bound(seq.begin(), seq.end(), SolvedBenchmark(bench)));
00236           assert(solution_it != seq.end());
00237           const SolvedBenchmark& solution(*solution_it);
00238           assert(solution.bench == bench);
00239           typedef ResultElement::floating_point_type floating_point_type;
00240           const floating_point_type& time_needed(solution.node -> rb -> average().average());
00241           typedef ResultElement::natural_number_type natural_number_type;
00242           const natural_number_type& time_out(solution.node -> rb -> time_out().time_out());
00243           return time_out / (1 + time_needed);
00244         }
00245         else
00246           return 0;
00247       }
00248 
00249       virtual number_type speed_factor_(const Benchmark& bench) const {
00250         const seq_solvers& seq(OKlib::SetAlgorithms::map_value(idb.succesful_solvers(), bench));
00251         typedef typename seq_solvers::const_iterator iterator;
00252         const iterator& end(seq.end());
00253         number_type sum = 0;
00254         for (iterator i = seq.begin(); i != end; ++i) {
00255           const Solver& solver(*i);
00256           sum += speed_factor(solver, bench); // ToDo: Here the first test in speed_factor(solver, bench) is not necessary
00257         }
00258         return sum;
00259       }
00260 
00261       virtual number_type total_time_(const Benchmark& bench) const {
00262         const seq_solvers& seq(OKlib::SetAlgorithms::map_value(idb.succesful_solvers(), bench));
00263         typedef typename seq_solvers::const_iterator iterator;
00264         const iterator& end(seq.end());
00265         number_type sum = 0;
00266         for (iterator i = seq.begin(); i != end; ++i) {
00267           const Solver& solver(*i);
00268           const seq_solved_benchmarks& seq(OKlib::SetAlgorithms::map_value(idb.solved_benchmarks(), solver));
00269           typedef typename seq_solved_benchmarks::const_iterator iterator;
00270           const iterator& solution_it(std::lower_bound(seq.begin(), seq.end(), SolvedBenchmark(bench)));
00271           assert(solution_it != seq.end());
00272           const SolvedBenchmark& solution(*solution_it);
00273           assert(solution.bench == bench);
00274           typedef ResultElement::floating_point_type floating_point_type;
00275           const floating_point_type& time_needed(solution.node -> rb -> average().average());
00276           sum += time_needed;
00277         }
00278         return sum;
00279       }
00280 
00281       virtual number_type speed_award_(const Solver& solver, const Benchmark& bench) const {
00282         if (solved(solver, bench))
00283           return standard_speed_purse * speed_factor(solver, bench) / speed_factor(bench);
00284         else
00285           return 0;
00286       }
00287 
00288       virtual number_type speed_award_(const Solver& solver) const {
00289         const seq_solved_benchmarks& seq(OKlib::SetAlgorithms::map_value(idb.solved_benchmarks(), solver));
00290         number_type sum = 0;
00291         typedef typename seq_solved_benchmarks::const_iterator iterator;
00292         const iterator end(seq.end());
00293         for (iterator i = seq.begin(); i != end; ++i) {
00294           const Benchmark& bench(*i);
00295           sum += speed_award(solver, bench);
00296         }
00297         return sum;
00298       }
00299      
00300       // --------------------------------------------------------------
00301 
00302       virtual number_type series_purse_(const SpecSeries& series) const {
00303         const seq_benchmarks& seq(OKlib::SetAlgorithms::map_value(idb.benchmarks_in_series(), series));
00304         const size_type_benchmarks& size(seq.size());
00305         return series_policy_type::purse(standard_series_purse, size);
00306       }
00307 
00308       virtual number_type series_purse_(const Solver& solver, const SpecSeries& series) const {
00309         if (solved(solver, series)) {
00310           const number_type count = solved(series);
00311           assert(count >= 1);
00312           return series_purse(series) / count;
00313         }
00314         else
00315           return 0;
00316       }
00317 
00318       virtual number_type series_purse_(const Solver& solver) const {
00319         const seq_spec_series& seq(OKlib::SetAlgorithms::map_value(idb.solved_series(), solver));
00320         number_type sum = 0;
00321         typedef typename seq_spec_series::const_iterator iterator;
00322         const iterator end(seq.end());
00323         for (iterator i = seq.begin(); i != end; ++i) { // loop over all series' the solver solved
00324           const SpecSeries& series(*i);
00325           sum += series_purse(solver, series);
00326         }
00327         return sum;
00328       }
00329 
00330       // --------------------------------------------------------------
00331 
00332       virtual number_type score_(const Solver& solver) const {
00333         return problem_purse(solver) + speed_award(solver) + series_purse(solver);
00334       }
00335 
00336     };
00337 
00338     // #######################################################
00339 
00352     template <template <typename CharT, typename ParseIterator> class ParserExtension = ParserEmpty, class ResultClass = Result, class SeriesPursePolicy = SAT2005SeriesPurse>
00353     struct Scoring_from_file {
00354       typedef Result_database_from_file<ParserResult, ResultClass, ParserExtension> result_database_from_file;
00355       typedef typename result_database_from_file::database_type database;
00356       typedef ElementaryAnalysis<database> indexed_database;
00357       typedef PurseScoring<indexed_database, SeriesPursePolicy> purse_scoring_type;
00358 
00359       result_database_from_file rdb;
00360       indexed_database idb;
00361 
00362       typedef typename purse_scoring_type::number_type number_type;
00363 
00364       struct series_info {
00365         SpecSeries series;
00366         number_type total_series_purse;
00367         number_type solver_series_purse;
00368         series_info (const SpecSeries& series, const number_type total_series_purse, const number_type solver_series_purse) : series(series), total_series_purse(total_series_purse), solver_series_purse(solver_series_purse) {}
00369         bool solved() const { return solver_series_purse != 0; }
00370         friend bool operator <(const series_info& lhs, const series_info& rhs) {
00371           return lhs.solver_series_purse < rhs.solver_series_purse;
00372         }
00373         friend bool operator ==(const series_info& lhs, const series_info& rhs) {
00374           return lhs.solver_series_purse == rhs.solver_series_purse;
00375         }
00376         OKLIB_DERIVED_RELATIONS_FRIENDS(series_info);
00377         friend std::ostream& operator <<(std::ostream& out, const series_info& s) {
00378           if (s.solved()) {
00379             out << boost::format("  %-60s : %10.1f %10.1f") % s.series % s.solver_series_purse % s.total_series_purse;
00380             return out << "\n";
00381           }
00382           else
00383             return out;
00384         }
00385       };
00386 
00387       struct solved_series : std::unary_function<const series_info&, bool> {
00388         bool operator() (const series_info& si) const {
00389           return si.solved();
00390         }
00391       };
00392 
00399       struct scoring {
00400         Solver solver;
00401         number_type score;
00402         number_type problem_purse;
00403         number_type speed_award;
00404         number_type series_purse;
00405 
00406         typedef std::vector<series_info> vector_type;
00407         vector_type series_info_vector;
00408 
00409         typedef unsigned int natural_number_type;
00410         natural_number_type instances_solved;
00411         //ToDo: Finer: number sat/unsat solved.
00412 
00413         scoring(const Solver& solver, const number_type score, const number_type problem_purse, const number_type speed_award, const number_type series_purse, const natural_number_type instances_solved) : solver(solver), score(score), problem_purse(problem_purse), speed_award(speed_award), series_purse(series_purse), instances_solved(instances_solved) {}
00414         friend bool operator <(const scoring& lhs, const scoring& rhs) {
00415           return lhs.score < rhs.score;
00416         }
00417         friend bool operator ==(const scoring& lhs, const scoring& rhs) {
00418           return lhs.score == rhs.score;
00419         }
00420         OKLIB_DERIVED_RELATIONS_FRIENDS(scoring);
00421         friend std::ostream& operator <<(std::ostream& out, const scoring& s) {
00422           out << boost::format("%-8s : %10.1f %10.1f %10.1f %10.1f\n") % s.solver % s.score % s.problem_purse % s.speed_award % s.series_purse;
00423           out << boost::format("Number of instances solved: %5u\n") % s.instances_solved;
00424           out << boost::format("Number of series solved: %4u\n") % std::count_if(s.series_info_vector.begin(), s.series_info_vector.end(), solved_series());
00425           out << "Composition of series purse:\n";
00426           std::copy(s.series_info_vector.begin(), s.series_info_vector.end(), std::ostream_iterator<series_info>(out, ""));
00427           return out;
00428         }
00429       };
00430 
00431       typedef std::vector<scoring> scoring_vector;
00432       scoring_vector scores_all;
00433       scoring_vector scores_sat;
00434       scoring_vector scores_unsat;
00435 
00436       const number_type standard_problem_purse;
00437       const number_type standard_speed_factor;
00438       const number_type standard_series_factor;
00439 
00440       Scoring_from_file(const std::string file_name, const number_type standard_problem_purse = 1000, const number_type standard_speed_factor = 1, const number_type standard_series_factor = 3) : rdb(file_name), idb(rdb.db), standard_problem_purse(standard_problem_purse), standard_speed_factor(standard_speed_factor), standard_series_factor(standard_series_factor) {
00441 
00442         {
00443           purse_scoring_type purse_scoring_all(idb, standard_problem_purse, standard_speed_factor, standard_series_factor);
00444           fill_scoring_vectors(scores_all, purse_scoring_all);
00445         }
00446         {
00447           database rdb_sat = rdb.db;
00448           rdb_sat.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb_sat.sat_status(), SATStatus(sat)));
00449           rdb_sat.intersection();
00450           rdb_sat.restrict();
00451           indexed_database idb_sat(rdb_sat);
00452           purse_scoring_type purse_scoring_sat(idb_sat, standard_problem_purse, standard_speed_factor, standard_series_factor);
00453           fill_scoring_vectors(scores_sat, purse_scoring_sat);
00454         }
00455         {
00456           database rdb_unsat = rdb.db;
00457           rdb_unsat.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb_unsat.sat_status(), SATStatus(unsat)));
00458           rdb_unsat.intersection();
00459           rdb_unsat.restrict();
00460           indexed_database idb_unsat(rdb_unsat);
00461           purse_scoring_type purse_scoring_unsat(idb_unsat, standard_problem_purse, standard_speed_factor, standard_series_factor);
00462           fill_scoring_vectors(scores_unsat, purse_scoring_unsat);
00463         }
00464       }
00465 
00466     private :
00467 
00468       void fill_scoring_vectors(scoring_vector& vector, purse_scoring_type& purse_scoring) {
00469         typedef typename indexed_database::map_solver_benchmarks map_solver;
00470         const map_solver& solvers(purse_scoring.idb.solved_benchmarks());
00471         vector.reserve(solvers.size());
00472         typedef typename map_solver::const_iterator iterator_solver;
00473         const iterator_solver& end_solvers(solvers.end());
00474         for (iterator_solver i = solvers.begin(); i != end_solvers; ++i) {
00475           const Solver& solver(i -> first);
00476           vector.push_back(scoring(solver, purse_scoring.score(solver), purse_scoring.problem_purse(solver), purse_scoring.speed_award(solver), purse_scoring.series_purse(solver), i -> second.size()));
00477           scoring& current(vector.back());
00478           typedef typename indexed_database::map_series_benchmarks map_series;
00479           const map_series& all_series(purse_scoring.idb.benchmarks_in_series());
00480           current.series_info_vector.reserve(all_series.size());
00481           typedef typename map_series::const_iterator iterator_series;
00482           const iterator_series& end_series(all_series.end());
00483           for (iterator_series j = all_series.begin(); j != end_series; ++j) {
00484             const SpecSeries& series(j -> first);
00485             current.series_info_vector.push_back(series_info(series,  purse_scoring.series_purse(series), purse_scoring.series_purse(solver, series)));
00486           }
00487           std::sort(current.series_info_vector.begin(), current.series_info_vector.end());
00488         }
00489         std::sort(vector.begin(), vector.end());
00490       }
00491 
00492     };
00493 
00494   }
00495 
00496 }
00497 
00498 #endif