sample.bib

@article{wager2014confidence,
  title={{Confidence intervals for random forests: The jackknife and the infinitesimal jackknife}},
  author={Wager, Stefan and Hastie, Trevor and Efron, Bradley},
  journal={The Journal of Machine Learning Research},
  volume={15},
  number={1},
  pages={1625--1651},
  year={2014},
  publisher={JMLR. org}
}

@book{Bischl2024,
    title = {{Applied Machine Learning Using {m}lr3 in {R}}},
    editor = {Bernd Bischl and Raphael Sonabend and Lars Kotthoff and Michel Lang},
    url = {https://mlr3book.mlr-org.com},
    year = {2024},
    isbn = {9781032507545},
    publisher = {CRC Press}
}

@InProceedings{10.1007/978-3-319-27436-2_21,
author="Amadini, Roberto
and Gabbrielli, Maurizio
and Mauro, Jacopo",
editor="Falaschi, Moreno",
title="{Why CP Portfolio Solvers Are (under)Utilized? Issues and Challenges}",
booktitle="Logic-Based Program Synthesis and Transformation",
year="2015",
publisher="Springer International Publishing",
address="Cham",
pages="349--364",
abstract="It is well recognized that a single, arbitrarily efficient solver can be significantly outperformed by a portfolio solver exploiting a combination of possibly slower on-average different solvers. Despite the success of portfolio solvers within the context of solving competitions, they are rarely used in practice. In this paper we give an overview of the main limitations that hinder the practical adoption and development of portfolio solvers within the Constraint Programming (CP) paradigm, discussing also possible ways to overcome them and potential extensions outside the CP field.",
isbn="978-3-319-27436-2"
}


@book{bishop2006pattern,
  title={Pattern recognition and machine learning},
  author={Bishop, Christopher M and Nasrabadi, Nasser M},
  volume={4},
  number={4},
  year={2006},
  publisher={Springer}
}

@inbook{HOOS2005257,
title = {Propositional Satisfiability and Constraint Satisfaction},
booktitle = {Stochastic Local Search},
publisher = {Morgan Kaufmann},
address = {San Francisco},
pages = {257-312},
year = {2005},
series = {The Morgan Kaufmann Series in Artificial Intelligence},
isbn = {978-1-55860-872-6},
doi = {https://doi.org/10.1016/B978-155860872-6/50023-8},
url = {https://www.sciencedirect.com/science/article/pii/B9781558608726500238},
author = {Holger H. Hoos and Thomas Stützle}
}

@article{KL,
 ISSN = {00034851},
 URL = {http://www.jstor.org/stable/2236703},
 author = {S. Kullback and R. A. Leibler},
 journal = {The Annals of Mathematical Statistics},
 number = {1},
 pages = {79--86},
 publisher = {Institute of Mathematical Statistics},
 title = {{On Information and Sufficiency}},
 urldate = {2024-11-02},
 volume = {22},
 year = {1951}
}

@article{randomforest,
  title={Random forests},
  author={Breiman, Leo},
  journal={Machine learning},
  volume={45},
  pages={5--32},
  year={2001},
  publisher={Springer}
}

@Article{ranger,
  title = {{ranger}: A Fast Implementation of Random Forests for High Dimensional Data in {C++} and {R}},
  author = {Marvin N. Wright and Andreas Ziegler},
  journal = {Journal of Statistical Software},
  year = {2017},
  volume = {77},
  number = {1},
  pages = {1--17},
  doi = {10.18637/jss.v077.i01},
}

@INPROCEEDINGS{968634,
  author={Lintao Zhang and Madigan, C.F. and Moskewicz, M.H. and Malik, S.},
  booktitle={IEEE/ACM International Conference on Computer Aided Design. ICCAD 2001. IEEE/ACM Digest of Technical Papers (Cat. No.01CH37281)}, 
  title={{Efficient conflict driven learning in a Boolean satisfiability solver}}, 
  year={2001},
  volume={},
  number={},
  pages={279-285},
  keywords={NP-complete problem;Electronic design automation and methodology;Formal verification;Automatic test pattern generation;Polynomials;Data mining;Databases},
  doi={10.1109/ICCAD.2001.968634}}


@article{biere2009conflict,
  title={Conflict-driven clause learning sat solvers},
  author={Biere, Armin and Heule, Marijn and van Maaren, Hans and Walsh, Toby},
  journal={Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications},
  pages={131--153},
  year={2009}
}

@inproceedings{conf/sat/AignerBKNP13,
  author       = {Martin Aigner and
                  Armin Biere and
                  Christoph M. Kirsch and
                  Aina Niemetz and
                  Mathias Preiner},
  editor       = {Daniel Le Berre},
  title        = {Analysis of Portfolio-Style Parallel {SAT} Solving on Current Multi-Core
                  Architectures},
  booktitle    = {{POS-13.} Fourth Pragmatics of {SAT} workshop, a workshop of the {SAT}
                  2013 conference, July 7, 2013, Helsinki, Finland},
  series       = {EPiC Series in Computing},
  volume       = {29},
  pages        = {28--40},
  publisher    = {EasyChair},
  year         = {2013},
  url          = {https://doi.org/10.29007/73n4},
  doi          = {10.29007/73N4},
  timestamp    = {Thu, 23 Sep 2021 11:48:26 +0200},
  biburl       = {https://dblp.org/rec/conf/sat/AignerBKNP13.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{10.1145/368273.368557,
author = {Davis, Martin and Logemann, George and Loveland, Donald},
title = {A machine program for theorem-proving},
year = {1962},
issue_date = {July 1962},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {5},
number = {7},
issn = {0001-0782},
url = {https://doi.org/10.1145/368273.368557},
doi = {10.1145/368273.368557},
abstract = {The programming of a proof procedure is discussed in connection with trial runs and possible improvements.},
journal = {Commun. ACM},
month = {jul},
pages = {394–397},
numpages = {4}
}

@book{10.5555/525,
author = {Pearl, Judea},
title = {Heuristics:  intelligent search strategies for computer problem solving},
year = {1984},
isbn = {0201055945},
publisher = {Addison-Wesley Longman Publishing Co., Inc.},
address = {USA}
}

@article{cenamor2014ibacop,
  title={{IBACOP and IBACOP2 planner}},
  author={Cenamor, Isabel and de la Rosa, Tom{\'a}s and Fern{\'a}ndez, Fernando and others},
  journal={IPC 2014 planner abstracts},
  pages={35--38},
  year={2014}
}

@book{books/daglib/0030297,
  added-at = {2013-01-09T00:00:00.000+0100},
  author = {Williamson, David P. and Shmoys, David B.},
  biburl = {https://www.bibsonomy.org/bibtex/221e625e4d68828727b30c5488bc2cd3b/dblp},
  ee = {http://www.cambridge.org/de/knowledge/isbn/item5759340/?site_locale=de_DE},
  interhash = {3413e8a66855af1121837c6af2cbbea3},
  intrahash = {21e625e4d68828727b30c5488bc2cd3b},
  isbn = {978-0-521-19527-0},
  keywords = {dblp},
  pages = {I-XI, 1-504},
  publisher = {Cambridge University Press},
  timestamp = {2013-01-10T11:39:33.000+0100},
  title = {The Design of Approximation Algorithms.},
  year = 2011
}


@incollection{gerhard_j__woeginger_2002,
        title={ Exact algorithms for {NP-hard} problems: a survey },
        author={ Gerhard J. Woeginger },
        year={ 2002 },
        publisher={ Springer, Berlin, Heidelberg },       
        pages={ 185-207 },
        doi={ 10.1007/3-540-36478-1_17 },  
      }

@InProceedings{10.1007/3-540-44614-1_50,
author="Redekopp, M.
and Dandalis, A.",
editor="Hartenstein, Reiner W.
and Gr{\"u}nbacher, Herbert",
title="{A Parallel Pipelined SAT Solver for FPGA's}",
booktitle="Field-Programmable Logic and Applications: The Roadmap to Reconfigurable Computing",
year="2000",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="462--468",
abstract="Solving Boolean satisfiability problems in reconfigurable hardware is an area of great research interest. Originally, reconfigurable hardware was used to map each problem instance and thus exploit maximum parallelism in evaluation of variable assignments. However, techniques to greatly reduce the search space require dynamic reconfiguration, and make regular mappings more desirable. Unfortunately, using a regular mapping constrains the parallelism in assignment evaluation. The architectures that have emerged choose either custom mapping and maximum parallelism or regular mapping and the promise of significant decreases in the search space. We propose a framework that can exploit both. Our framework uses a regular mapping while introducing a scalable parallel architecture. Using our approach, speedups of up to one order of magnitude over current state-of-the-art reconfigurable hardware solvers have been obtained.",
isbn="978-3-540-44614-9"
}

@conference{11390_1234673,
 abstract = {Modern SAT solvers employ a number of smart techniques and strategies to achieve maximum efficiency in solving the Boolean Satisfiability problem. Among all components of a solver, the branching heuristics plays a crucial role in affecting the performance of the entire solver. Traditionally, the main branching heuristics that have appeared in the literature have been classified as look-back heuristics or look-ahead heuristics. As SAT technology has evolved, the former have become more and more preferable, for their demand for less computational effort. Graphics Processor Units (GPUs) are massively parallel devices that have spread enormously over the past few decades and offer great computing power at a relatively low cost. We describe how to exploit such computational power to efficiently implement look-ahead heuristics. Our aim is to “rehabilitate” these heuristics, by showing their effectiveness in the contest of a parallel SAT solver.},
 author = {Collevati, M. and Dovier, Agostino and Formisano, A.},
 booktitle = {CEUR Workshop Proceedings},
 keywords = {Branching Heuristics; GPU parallelism; SAT Solving},
 pages = {17--31},
 publisher = {CEUR-WS},
 title = {{GPU Parallelism for SAT Solving Heuristics}},
 volume = {3204},
 year = {2022}
}

@incollection{kadioglu2010isac,
  title={ISAC--instance-specific algorithm configuration},
  author={Kadioglu, Serdar and Malitsky, Yuri and Sellmann, Meinolf and Tierney, Kevin},
  booktitle={ECAI 2010},
  pages={751--756},
  year={2010},
  publisher={IOS Press}
}

@InProceedings{10.1007/978-3-030-72016-2_8,
author="Osama, Muhammad
and Wijs, Anton
and Biere, Armin",
editor="Groote, Jan Friso
and Larsen, Kim Guldstrand",
title="{SAT Solving with GPU Accelerated Inprocessing}",
booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="133--151",
abstract="Since 2013, the leading SAT solvers in the SAT competition all use inprocessing, which unlike preprocessing, interleaves search with simplifications. However, applying inprocessing frequently can still be a bottle neck, i.e., for hard or large formulas. In this work, we introduce the first attempt to parallelize inprocessing on GPU architectures. As memory is a scarce resource in GPUs, we present new space-efficient data structures and devise a data-parallel garbage collector. It runs in parallel on the GPU to reduce memory consumption and improves memory access locality. Our new parallel variable elimination algorithm is twice as fast as previous work. In experiments our new solver ParaFROST solves many benchmarks faster on the GPU than its sequential counterparts.",
isbn="978-3-030-72016-2"
}


@INPROCEEDINGS{5547116,
  author={Meyer, Quirin and Schönfeld, Fabian and Stamminger, Marc and Wanka, Rolf},
  booktitle={2010 International Conference on High Performance Computing \& Simulation}, 
  title={{3-SAT on CUDA: Towards a massively parallel SAT solver}}, 
  year={2010},
  volume={},
  number={},
  pages={306-313},
  keywords={Graphics processing unit;Memory management;Pipelines;Program processors;Multicore processing;GPGPU;thread level parallelism;load balancing and sharing;random 3-SAT},
  doi={10.1109/HPCS.2010.5547116}}


@article{10.1007/s10703-023-00432-z,
author = {Osama, Muhammad and Wijs, Anton and Biere, Armin},
title = {{Certified SAT solving with GPU accelerated inprocessing}},
year = {2023},
issue_date = {Jun 2024},
publisher = {Kluwer Academic Publishers},
address = {USA},
volume = {62},
number = {1–3},
issn = {0925-9856},
url = {https://doi.org/10.1007/s10703-023-00432-z},
doi = {10.1007/s10703-023-00432-z},
abstract = {Since 2013, the leading SAT solvers in SAT competitions all use inprocessing, which, unlike preprocessing, interleaves search with simplifications. However, inprocessing is typically a performance bottleneck, in particular for hard or large formulas. In this work, we introduce the first attempt to parallelize inprocessing on GPU architectures. As one of the main challenges in GPU programming is memory locality, we present new compact data structures and devise a data-parallel garbage collector. It runs in parallel on the GPU to reduce memory consumption and improve memory locality. Our new parallel variable elimination algorithm is roughly twice as fast as previous work. Moreover, we augment the variable elimination with the first parallel algorithm for functional dependency extraction in an attempt to find more logical gates to eliminate that cannot be found with syntactic approaches. We present a novel algorithm to generate clausal proofs in parallel to validate all simplifications running on the GPU besides the CDCL search, giving high credibility to our solver and its use in critical applications such as model checkers. In experiments, our new solver ParaFROST solves numerous benchmarks faster on the GPU than its sequential counterparts. With functional dependency extraction, inprocessing in ParaFROST was more effective in reducing the solving time. Last but not least, all proofs generated by ParaFROST were successfully verified.},
journal = {Form. Methods Syst. Des.},
month = {aug},
pages = {79–118},
numpages = {40},
keywords = {SAT solving, Inprocessing, GPUs, Clausal proofs, Functional dependency extraction}
}

@article{10.1145/1497561.1497576,
author = {Gulati, Kanupriya and Paul, Suganth and Khatri, Sunil P. and Patil, Srinivas and Jas, Abhijit},
title = {{FPGA-based hardware acceleration for Boolean satisfiability}},
year = {2009},
issue_date = {March 2009},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {14},
number = {2},
issn = {1084-4309},
url = {https://doi.org/10.1145/1497561.1497576},
doi = {10.1145/1497561.1497576},
abstract = {We present an FPGA-based hardware solution to the Boolean satisfiability (SAT) problem, with the main goals of scalability and speedup. In our approach the traversal of the implication graph as well as conflict clause generation are performed in hardware, in parallel. The experimental results and their analysis, along with the performance models are discussed. We show that an order of magnitude improvement in runtime can be obtained over MiniSAT (the best-in-class software based approach) by using a Virtex-4 (XC4VFX140) FPGA device. The resulting system can handle instances with as many as 10K variables and 280K clauses.},
journal = {ACM Trans. Des. Autom. Electron. Syst.},
month = {apr},
articleno = {33},
numpages = {11},
keywords = {Boolean satisfiabilty (SAT), FPGA, boolean constant propagation (BCP), conflict induced clauses, non-chronological backtrack}
}
@INPROCEEDINGS{4555925,
  author={Davis, John D. and Zhangxi Tan and Fang Yu and Lintao Zhang},
  booktitle={2008 45th ACM/IEEE Design Automation Conference}, 
  title={A practical reconfigurable hardware accelerator for boolean satisfiability solvers}, 
  year={2008},
  volume={},
  number={},
  pages={780-785},
  keywords={Hardware;Field programmable gate arrays;Business continuity;Acceleration;Computer architecture;Signal synthesis;Wires;Pipeline processing;Signal design;Clocks;SAT solver;reconfigurable;BCP;co-processor;FPGA},
  doi={10.1145/1391469.1391669}}

@INPROCEEDINGS{707896,
  author={Peixin Zhong and Martonosi, M. and Ashar, P. and Malik, S.},
  booktitle={{Proceedings. IEEE Symposium on FPGAs for Custom Computing Machines (Cat. No.98TB100251)}}, 
  title={{Accelerating Boolean satisfiability with configurable hardware}}, 
  year={1998},
  volume={},
  number={},
  pages={186-195},
  keywords={Acceleration;Hardware;Field programmable gate arrays;Application specific integrated circuits;Logic design;Artificial intelligence;Application software;Computer applications;National electric code;Boolean functions},
  doi={10.1109/FPGA.1998.707896}}

@InProceedings{10.1007/11752578_46,
author="Singer, Daniel
and Vagner, Alain",
editor="Wyrzykowski, Roman
and Dongarra, Jack
and Meyer, Norbert
and Wa{\'{s}}niewski, Jerzy",
title="{Parallel Resolution of the Satisfiability Problem (SAT) with OpenMP and MPI}",
booktitle="Parallel Processing and Applied Mathematics",
year="2006",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="380--388",
abstract="The past few years have seen enormous progress in the performance of propositional satisfiability (SAT) solving, and consequently SAT solvers are widely used in industry for many applications. In spite of this progress, there is strong demand for higher SAT algorithms efficiency to solve harder and larger problems. Unfortunately, most modern solvers are sequential and fewer are parallel.",
isbn="978-3-540-34142-0"
}


@InProceedings{10.1007/978-3-540-85110-3_11,
author="Hyv{\"a}rinen, Antti E. J.
and Junttila, Tommi
and Niemel{\"a}, Ilkka",
editor="Autexier, Serge
and Campbell, John
and Rubio, Julio
and Sorge, Volker
and Suzuki, Masakazu
and Wiedijk, Freek",
title="Strategies for Solving {SAT} in Grids by Randomized Search",
booktitle="Intelligent Computer Mathematics",
year="2008",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="125--140",
abstract="Grid computing offers a promising approach to solving challenging computational problems in an environment consisting of a large number of easily accessible resources. In this paper we develop strategies for solving collections of hard instances of the propositional satisfiability problem (SAT) with a randomized SAT solver run in a Grid. We study alternative strategies by using a simulation framework which is composed of (i) a grid model capturing the communication and management delays, and (ii) run-time distributions of a randomized solver, obtained by running a state-of-the-art SAT solver on a collection of hard instances. The results are experimentally validated in a production level Grid. When solving a single hard SAT instance, the results show that in practice only a relatively small amount of parallelism can be efficiently used; the speedup obtained by increasing parallelism thereafter is negligible. This observation leads to a novel strategy of using grid to solve collections of hard instances. Instead of solving instances one-by-one, the strategy aims at decreasing the overall solution time by applying an alternating distribution schedule.",
isbn="978-3-540-85110-3"
}


@article{journals/jsat/GilFS09,
  author       = {Lu{\'{\i}}s Gil and
                  Paulo F. Flores and
                  Lu{\'{\i}}s Miguel Silveira},
  title        = {{PMSat: a parallel version of MiniSAT}},
  journal      = {J. Satisf. Boolean Model. Comput.},
  volume       = {6},
  number       = {1-3},
  pages        = {71--98},
  year         = {2009},
  url          = {https://doi.org/10.3233/sat190063},
  doi          = {10.3233/SAT190063},
  timestamp    = {Mon, 17 Aug 2020 18:32:39 +0200},
  biburl       = {https://dblp.org/rec/journals/jsat/GilFS09.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}


@article{holldobler_short_2011,
	title = {{A short overview on modern parallel {SAT}-solvers}},
	abstract = {This paper surveys modern parallel SAT-solvers. It focusses on recent successful techniques and points out weaknesses that have to be overcome to exploit the full power of modern multi-core processors. © 2011 Universitas Indonesia.},
	number = {January},
	journal = {ICACSIS 2011 - 2011 International Conference on Advanced Computer Science and Information Systems, Proceedings},
	author = {Hölldobler, Steffen and Manthey, Norbert and {Van Hau Nguyen} and Stecklina, Julian and Steinke, Peter},
	year = {2011},
	note = {ISBN: 9789791421119},
	pages = {201--206},
	file = {PDF:/home/hkashgar/Zotero/storage/A38AIQ6I/A_short_overview_on_modern_parallel_SAT-solvers.pdf:application/pdf},
}

@InProceedings{10.1007/978-3-642-16242-8_37,
author="H{\"o}lldobler, Steffen
and Manthey, Norbert
and Saptawijaya, Ari",
editor="Ferm{\"u}ller, Christian G.
and Voronkov, Andrei",
title="{Improving Resource-Unaware SAT Solvers}",
booktitle="Logic for Programming, Artificial Intelligence, and Reasoning",
year="2010",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="519--534",
abstract="The paper discusses cache utilization in state-of-the-art SAT solvers. The aim of the study is to show how a resource-unaware SAT solver can be improved by utilizing the cache sensibly. The analysis is performed on a CDCL-based SAT solver using a subset of the industrial SAT Competition 2009 benchmark. For the analysis, the total cycles, the resource stall cycles, the L2 cache hits and the L2 cache misses are traced using sample based profiling. Based on the analysis, several techniques -- some of which have not been used in SAT solvers so far -- are proposed resulting in a combined speedup up to 83{\%} without affecting the search path of the solver. The average speedup on the benchmark is 60{\%}. The new techniques are also applied to MiniSAT2.0 improving its runtime by 20{\%} on average.",
isbn="978-3-642-16242-8"
}

@book{sat2023,
  title = {Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions},
  editor = {Tomas Balyo and Marijn Heule and Markus Iser and Matti Järvisalo and Martin Suda},
  year = {2023},
  publisher = {Department of Computer Science, Helsinki Institute for Information Technology, Constraint Reasoning and Optimization research group / Matti Järvisalo},
  type = {Anthology or special issue},
  note = {Research output: Book/Report},
}

@article{YUEN2016654,
title = {{Which algorithm should I choose: An evolutionary algorithm portfolio approach}},
journal = {Applied Soft Computing},
volume = {40},
pages = {654-673},
year = {2016},
issn = {1568-4946},
doi = {https://doi.org/10.1016/j.asoc.2015.12.021},
url = {https://www.sciencedirect.com/science/article/pii/S1568494615008005},
author = {Shiu Yin Yuen and Chi Kin Chow and Xin Zhang and Yang Lou},
keywords = {Multi-method search, Algorithm portfolio, Performance prediction, Synergy, Scalability, Real world application},
abstract = {Many good evolutionary algorithms have been proposed in the past. However, frequently, the question arises that given a problem, one is at a loss of which algorithm to choose. In this paper, we propose a novel algorithm portfolio approach to address the above problem for single objective optimization. A portfolio of evolutionary algorithms is first formed. Covariance Matrix Adaptation Evolution Strategy (CMA-ES), History driven Evolutionary Algorithm (HdEA), Particle Swarm Optimization (PSO2011) and Self adaptive Differential Evolution (SaDE) are chosen as component algorithms. Each algorithm runs independently with no information exchange. At any point in time, the algorithm with the best predicted performance is run for one generation, after which the performance is predicted again. The best algorithm runs for the next generation, and the process goes on. In this way, algorithms switch automatically as a function of the computational budget. This novel algorithm is named Multiple Evolutionary Algorithm (MultiEA). The predictor we introduced has the nice property of being parameter-less, and algorithms switch automatically as a function of budget. The following contributions are made: (1) experimental results on 24 benchmark functions show that MultiEA outperforms (i) Multialgorithm Genetically Adaptive Method for Single Objective Optimization (AMALGAM-SO); (ii) Population-based Algorithm Portfolio (PAP); (iii) a multiple algorithm approach which chooses an algorithm randomly (RandEA); and (iv) a multiple algorithm approach which divides the computational budget evenly and execute all algorithms in parallel (ExhEA). This shows that it outperforms existing portfolio approaches and the predictor is functioning well. (2) Moreover, a neck to neck comparison of MultiEA with CMA-ES, HdEA, PSO2011, and SaDE is also made. Experimental results show that the performance of MultiEA is very competitive. In particular, MultiEA, being a portfolio algorithm, is sometimes even better than all its individual algorithms, and has more robust performance. (3) Furthermore, a positive synergic effect is discovered, namely, MultiEA can sometimes perform better than the sum of its individual EAs. This gives interesting insights into why an algorithm portfolio is a good approach. (4) It is found that MultiEA scales as well as the best algorithm in the portfolio. This suggests that MultiEA scales up nicely, which is a desirable algorithmic feature. (5) Finally, the performance of MultiEA is investigated on a real world problem. It is found that MultiEA can select the most suitable algorithm for the problem and is much better than choosing algorithms randomly.}
}

@book{sat2021,
  title = {Proceedings of SAT Competition 2021: Solver and Benchmark Descriptions},
  editor = {Tomas Balyo and Nils Froleyks and Marijn Heule and Markus Iser and Matti Järvisalo and Martin Suda},
  year = {2021},
  publisher = {Department of Computer Science Report Series B},
  pages = {71},
  url = {http://hdl.handle.net/10138/333647},
  note = {Non peer reviewed, Access rights unspecified},
  keywords = {Computer and information sciences},
  series = {Department of Computer Science Report Series B},
  type = {Anthology or special issue},
}

@article{10.5555/3013589.3013607,
author = {Cenamor, Isabel and De La Rosa, Tom\'{a}s and Fern\'{a}ndez, Fernando},
title = {{The IBaCoP planning system: instance-based configured portfolios}},
year = {2016},
issue_date = {May 2016},
publisher = {AI Access Foundation},
address = {El Segundo, CA, USA},
volume = {56},
number = {1},
issn = {1076-9757},
abstract = {Sequential planning portfolios are very powerful in exploiting the complementary strength of different automated planners. The main challenge of a portfolio planner is to define which base planners to run, to assign the running time for each planner and to decide in what order they should be carried out to optimize a planning metric. Portfolio configurations are usually derived empirically from training benchmarks and remain fixed for an evaluation phase. In this work, we create a per-instance configurable portfolio, which is able to adapt itself to every planning task. The proposed system pre-selects a group of candidate planners using a Pareto-dominance filtering approach and then it decides which planners to include and the time assigned according to predictive models. These models estimate whether a base planner will be able to solve the given problem and, if so, how long it will take. We define different portfolio strategies to combine the knowledge generated by the models. The experimental evaluation shows that the resulting portfolios provide an improvement when compared with non-informed strategies. One of the proposed portfolios was the winner of the Sequential Satisficing Track of the International Planning Competition held in 2014.},
journal = {J. Artif. Int. Res.},
month = may,
pages = {657–691},
numpages = {35}
}

@inproceedings{10.5555/3007337.3007474,
author = {Valenzano, Richard and Nakhost, Hootan and M\"{u}ller, Martin and Schaeffer, Jonathan and Sturtevant, Nathan},
title = {ArvandHerd: parallel planning with a portfolio},
year = {2012},
isbn = {9781614990970},
publisher = {IOS Press},
address = {NLD},
abstract = {ArvandHerd is a parallel planner that won the multi-core sequential satisficing track of the 2011 International Planning Competition (IPC 2011). It assigns processors to run different members of an algorithm portfolio which contains several configurations of each of two different planners: LAMA-2008 and Arvand. In this paper, we demonstrate that simple techniques for using different planner configurations can significantly improve the coverage of both of these planners. We then show that these two planners, when using multiple configurations, can be combined to construct a high performance parallel planner. In particular, we will show that ArvandHerd can solve more IPC benchmark problems than even a perfect parallelization of LAMA-2011, which won the satisficing track at IPC 2011. We will also show that the coverage of ArvandHerd can be further improved if LAMA-2008 is replaced by LAMA-2011 in the portfolio.},
booktitle = {Proceedings of the 20th European Conference on Artificial Intelligence},
pages = {786–791},
numpages = {6},
location = {Montpellier, France},
series = {ECAI'12}
}

@book{series/faia/336,
  editor       = {Armin Biere and
                  Marijn Heule and
                  Hans van Maaren and
                  Toby Walsh},
  title        = {Handbook of Satisfiability - Second Edition},
  series       = {Frontiers in Artificial Intelligence and Applications},
  volume       = {336},
  publisher    = {{IOS} Press},
  year         = {2021},
  url          = {https://doi.org/10.3233/FAIA336},
  doi          = {10.3233/FAIA336},
  isbn         = {978-1-64368-160-3},
  timestamp    = {Fri, 06 May 2022 08:03:54 +0200},
  biburl       = {https://dblp.org/rec/series/faia/336.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@misc{hoos2014claspfolio2advancesalgorithm,
      title={claspfolio 2: Advances in Algorithm Selection for Answer Set Programming}, 
      author={Holger Hoos and Marius Lindauer and Torsten Schaub},
      year={2014},
      eprint={1405.1520},
      archivePrefix={arXiv},
      primaryClass={cs.AI},
      url={https://arxiv.org/abs/1405.1520}, 
}

@article{Lissovoi_Oliveto_Warwicker_2019, title={{On the Time Complexity of Algorithm Selection Hyper-Heuristics for Multimodal Optimisation}}, volume={33}, url={https://ojs.aaai.org/index.php/AAAI/article/view/4071}, DOI={10.1609/aaai.v33i01.33012322}, abstractNote={<p>Selection hyper-heuristics are automated algorithm selection methodologies that choose between different heuristics during the optimisation process. Recently selection hyperheuristics choosing between a collection of elitist randomised local search heuristics with different neighbourhood sizes have been shown to optimise a standard unimodal benchmark function from evolutionary computation in the optimal expected runtime achievable with the available low-level heuristics. In this paper we extend our understanding to the domain of multimodal optimisation by considering a hyper-heuristic from the literature that can switch between elitist and nonelitist heuristics during the run. We first identify the range of parameters that allow the hyper-heuristic to hillclimb efficiently and prove that it can optimise a standard hillclimbing benchmark function in the best expected asymptotic time achievable by unbiased mutation-based randomised search heuristics. Afterwards, we use standard multimodal benchmark functions to highlight function characteristics where the hyper-heuristic is efficient by swiftly escaping local optima and ones where it is not. For a function class called C<sc>LIFF</sc><sub><em>d</em></sub> where a new gradient of increasing fitness can be identified after escaping local optima, the hyper-heuristic is extremely efficient while a wide range of established elitist and non-elitist algorithms are not, including the well-studied Metropolis algorithm. We complete the picture with an analysis of another standard benchmark function called J<sc>UMP</sc><sub><em>d</em></sub> as an example to highlight problem characteristics where the hyper-heuristic is inefficient. Yet, it still outperforms the wellestablished non-elitist Metropolis algorithm.</p>}, number={01}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Lissovoi, Andrei and Oliveto, Pietro S. and Warwicker, John Alasdair}, year={2019}, month={Jul.}, pages={2322-2329} }

@inproceedings{yuri_malitsky__2014,
        title={{A Portfolio Approach to Enumerating Minimal Correction Subsets for Satisfiability Problems}},
        author={ Yuri Malitsky and Barry O'Sullivan and Alessandro Previti and Joao Marques-Silva },
        year={ 2014 },
        publisher={ Springer, Cham },
        pages={ 368-376 },
        doi={ 10.1007/978-3-319-07046-9_26 }
}

@article{osti_2223030,
title = {{A Probabilistic Approach To Selecting Build Configurations in Package Managers}},
author = {Nichols, Daniel and Menon, Harshitha and Gamblin, Todd and Bhatele, Abhinav},
abstractNote = {In the past decade software has grown significantly in complexity and scale. Likewise the number of dependencies for most software has increased with typical software packages depending on tens to hundreds of other packages. Such large numbers of dependencies place a significant burden on package managers to correctly maintain dependency lists and constraints between them. Due to this package managers have incorporated sophisticated tooling such as SAT solvers into their dependency management mechanisms. Despite these tools package managers still rely on many human annotated constraints for dependency and version selection. These are error-prone and require a significant amount of labor to constantly update and test. In this paper we propose a methodology to make use of historical build results in selecting the version for package dependencies. Our method utilizes the flexibility of the Spack package manager’s heavily parameterized package configurations to incorporate a machine learning model trained to predict the probability of build outcomes. This work is able to build and install packages with a 13% higher success rate than the default version selection mechanism in Spack.},
doi = {10.2172/2223030},
url = {https://www.osti.gov/biblio/2223030}, journal = {},
place = {United States},
year = {2023},
month = {11}
}

@article{manthey2011parallel,
  title={{Parallel SAT solving-using more cores}},
  author={Manthey, Norbert},
  journal={Pragmatics of SAT (POS’11)},
  year={2011}
}

@InProceedings{10.1007/978-3-540-30201-8_33,
author="Nudelman, Eugene
and Leyton-Brown, Kevin
and Hoos, Holger H.
and Devkar, Alex
and Shoham, Yoav",
editor="Wallace, Mark",
title="Understanding Random {SAT}: Beyond the Clauses-to-Variables Ratio",
booktitle="Principles and Practice of Constraint Programming -- CP 2004",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="438--452",
abstract="It is well known that the ratio of the number of clauses to the number of variables in a random k-SAT instance is highly correlated with the instance's empirical hardness. We consider the problem of identifying such features of random SAT instances automatically using machine learning. We describe and analyze models for three SAT solvers -- kcnfs, oksolver and satz -- and for two different distributions of instances: uniform random 3-SAT with varying ratio of clauses-to-variables, and uniform random 3-SAT with fixed ratio of clauses-to-variables. We show that surprisingly accurate models can be built in all cases. Furthermore, we analyze these models to determine which features are most useful in predicting whether an instance will be hard to solve. Finally we discuss the use of our models to build SATzilla, an algorithm portfolio for SAT.",
isbn="978-3-540-30201-8"
}


@article{PULINA2019224,
title = {The 2016 and 2017 {QBF} solvers evaluations ({QBFEVAL'16} and {QBFEVAL'17})},
journal = {Artificial Intelligence},
volume = {274},
pages = {224-248},
year = {2019},
issn = {0004-3702},
doi = {https://doi.org/10.1016/j.artint.2019.04.002},
url = {https://www.sciencedirect.com/science/article/pii/S0004370218301450},
author = {Luca Pulina and Martina Seidl},
keywords = {Quantified Boolean formulas, QBF competition, QBF solving},
abstract = {After a break of about five years, in 2016 the classical QBFEVAL has been revived. QBFEVAL is a competitive evaluation of solvers for quantified Boolean formulas (QBF), the extension of propositional formulas with existential and universal quantifiers over the propositional variables. Due to the enormous interest in QBFEVAL'16, more recently, QBFEVAL'17 was organized. Both competitions were affiliated to the respective editions of the International Conference on Theory and Applications of Satisfiability Testing (SAT'16 and SAT'17), the major conference in research on SAT and related areas. In this paper we report about the 2016 and 2017 competitive evaluations of QBF solvers (QBFEVAL'16 and QBFEVAL'17), the two most recent events in a series of competitions established with the aim of assessing the advancements in reasoning about QBFs. This report gives an overview of the setup of these two events, on their participants and on the results of the experiments that were performed for evaluating the participating systems.}
}

@inproceedings{9ae8443ad82b4056bccf7102c0056152,  title     = "{Which algorithm should I choose at any point of the search: An evolutionary portfolio approach}", 
author    = "Yuen, {Shiu Yin} and Chow, {Chi Kin} and Xin Zhang",  
year      = "2013", 
doi       = "10.1145/2463372.2463435",  language  = "English", 
isbn      = "9781450319638", 
pages     = "567--574",  
booktitle = "GECCO 2013 - Proceedings of the 2013 Genetic and Evolutionary Computation Conference" }

@article{10.1162/evco_a_00242,
    author = {Kerschke, Pascal and Hoos, Holger H. and Neumann, Frank and Trautmann, Heike},
    title = "{Automated Algorithm Selection: Survey and Perspectives}",
    journal = {Evolutionary Computation},
    volume = {27},
    number = {1},
    pages = {3-45},
    year = {2019},
    issn = {1063-6560},
    doi = {10.1162/evco_a_00242},
    url = {https://doi.org/10.1162/evco\_a\_00242},
    eprint = {https://direct.mit.edu/evco/article-pdf/27/1/3/1552398/evco\_a\_00242.pdf},
}

@techreport{gerevini2005plan,
  title={{Plan constraints and preferences in PDDL3}},
  author={Gerevini, Alfonso and Long, Derek},
  year={2005},
  institution={Technical Report 2005-08-07, Department of Electronics for Automation~…}
}

@Inbook{Maturana2012,
author={Maturana, Jorge
and Fialho, {\'A}lvaro
and Saubion, Fr{\'e}d{\'e}ric
and Schoenauer, Marc
and Lardeux, Fr{\'e}d{\'e}ric
and Sebag, Mich{\`e}le},
title={Adaptive Operator Selection and Management in Evolutionary Algorithms},
bookTitle={Autonomous Search},
year={2012},
publisher={Springer},
pages={161--189},
isbn={978-3-642-21434-9},
doi={10.1007/978-3-642-21434-9_7},
url={https://doi.org/10.1007/978-3-642-21434-9_7}
}


@article{HUTTER201479,
title = {Algorithm runtime prediction: Methods \& evaluation},
journal = {Artificial Intelligence},
volume = {206},
pages = {79-111},
year = {2014},
issn = {0004-3702},
doi = {https://doi.org/10.1016/j.artint.2013.10.003},
url = {https://www.sciencedirect.com/science/article/pii/S0004370213001082},
author = {Frank Hutter and Lin Xu and Holger H. Hoos and Kevin Leyton-Brown},
keywords = {Supervised machine learning, Performance prediction, Empirical performance models, Response surface models, Highly parameterized algorithms, Propositional satisfiability, Mixed integer programming, Travelling salesperson problem}
}

@article{HU201268,
title = {An intelligent augmentation of particle swarm optimization with multiple adaptive methods},
journal = {Information Sciences},
volume = {213},
pages = {68-83},
year = {2012},
issn = {0020-0255},
doi = {https://doi.org/10.1016/j.ins.2012.05.020},
url = {https://www.sciencedirect.com/science/article/pii/S0020025512003799},
author = {Mengqi Hu and Teresa Wu and Jeffery D. Weir},
keywords = {Particle swarm optimization, Adaptive multi-method, Sub-gradient, Non-uniform mutation, Cauchy mutation},

}
@Article{mlr,
  title = {{mlr: Machine Learning in R}},
  author = {Bernd Bischl and Michel Lang and Lars Kotthoff and Julia Schiffner and Jakob Richter and Erich Studerus and Giuseppe Casalicchio and Zachary M. Jones},
  journal = {Journal of Machine Learning Research},
  year = {2016},
  volume = {17},
  number = {170},
  pages = {1-5},
  url = {https://jmlr.org/papers/v17/15-066.html},
}

@InProceedings{pmlr-v140-kashgarani21a,
  title = 	 {{Is Algorithm Selection Worth It? Comparing Selecting Single Algorithms and Parallel Execution}},
  author =       {Kashgarani, Haniye and Kotthoff, Lars},
  booktitle = 	 {AAAI Workshop on Meta-Learning and MetaDL Challenge},
  pages = 	 {58--64},
  year = 	 {2021},
  volume = 	 {140},
  series = 	 {Proceedings of Machine Learning Research},
  publisher =    {PMLR},
  pdf = 	 {http://proceedings.mlr.press/v140/kashgarani21a/kashgarani21a.pdf},
  url = 	 {https://proceedings.mlr.press/v140/kashgarani21a.html}
}

@article{yuen2019selecting,
  title={Selecting evolutionary algorithms for black box design optimization problems},
  author={Yuen, Shiu Yin and Lou, Yang and Zhang, Xin},
  journal={Soft Computing},
  volume={23},
  number={15},
  pages={6511--6531},
  year={2019},
  publisher={Springer}
}

@article{maratea2014multi,
  title={A multi-engine approach to answer-set programming},
  author={Maratea, Marco and Pulina, Luca and Ricca, Francesco},
  journal={Theory and Practice of Logic Programming},
  volume={14},
  number={6},
  pages={841--868},
  year={2014},
  publisher={Cambridge University Press}
}

@InProceedings{pmlr-v79-lindauer17a,
  title = 	 {Open Algorithm Selection Challenge 2017: Setup and Scenarios},
  author = 	 {Lindauer, Marius and van Rijn, Jan N. and Kotthoff, Lars},
  booktitle = 	 {Proceedings of the Open Algorithm Selection Challenge},
  pages = 	 {1--7},
  year = 	 {2017},
  volume = 	 {79},
  publisher =    {PMLR},
  pdf = 	 {http://proceedings.mlr.press/v79/lindauer17a/lindauer17a.pdf},
  url = 	 {https://proceedings.mlr.press/v79/lindauer17a.html}
}

@article{LLAMA,
  author    = {Lars Kotthoff},
  title     = {{LLAMA: Leveraging Learning to Automatically Manage Algorithms}},
  journal   = {CoRR},
  volume    = {abs/1306.1031},
  year      = {2013},
  url       = {http://arxiv.org/abs/1306.1031},
  archivePrefix = {arXiv},
  eprint    = {1306.1031},
  numpages = {36},
  timestamp = {Mon, 13 Aug 2018 16:48:04 +0200},
  biburl    = {https://dblp.org/rec/journals/corr/Kotthoff13.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{GOMES200143,
author = {Gomes, Carla and Selman, Bart},
year = {2001},
pages = {43-62},
title = {Algorithm portfolios},
volume = {126},
journal = {Artificial Intelligence}
}

@article{Carchrae2005APPLYINGML,
  title={{Applying Machine Learning to Low-Knowledge Control of Optimization Algorithms}},
  author={Tom Carchrae and J. Christopher Beck},
  journal={Computational Intelligence},
  year={2005},
  volume={21},
  url={https://api.semanticscholar.org/CorpusID:7953876}
}

@INPROCEEDINGS{10194439,
  author={Lukac, Martin and Kameyama, Michitaka},
  booktitle={2023 International Conference on Information and Digital Technologies (IDT)}, 
  title={{Verification Based Algorithm Selection}}, 
  year={2023},
  volume={},
  number={},
  pages={25-30},
  keywords={Metalearning;Image segmentation;Semantics;Merging;Information processing;Cognition;Resource management;algorithm selection;semantic verification;relational graphs},
  doi={10.1109/IDT59031.2023.10194439}}


@InProceedings{10.1007/978-3-319-32034-2_25,
author="C{\'a}rdenas-Montes, Miguel",
editor="Mart{\'i}nez-{\'A}lvarez, Francisco
and Troncoso, Alicia
and Quinti{\'a}n, H{\'e}ctor
and Corchado, Emilio",
title="{Evaluating the Difficulty of Instances of the Travelling Salesman Problem in the Nearby of the Optimal Solution Based on Random Walk Exploration}",
booktitle="Hybrid Artificial Intelligent Systems",
year="2016",
publisher="Springer International Publishing",
address="Cham",
pages="299--310",
abstract="Combinatorial optimization is one of the main research areas in Evolutionary Computing and Operational Research, and the Travelling Salesman Problem one of their most popular problems. The never ending quest of researchers for new and more difficult combinatorial problems to stress their evolutionary algorithms leads to investigate how to measure the difficulty of Travelling Salesman Problem instances. By developing methodologies for separating ease from difficult instances, researchers will be confident about the performance of their algorithms. In this proof-of-concept, a methodology for evaluating the difficulty of instances of the Travelling Salesman Problem in the nearby of the optimal solution is proposed. This methodology is based on the use of Random Walk to explore the closeness area of the optimal solution. Instances with a more pronounced gradient towards the optimal solution might be considered easier than instances exhibiting almost a null gradient. The exploration of this gradient is done by starting from the optimal tour and later modifying it with a Random Walk process. The aim is to propose a methodology to evaluate the difficulty of instances of Travelling Salesman Problem, which can be applied to other combinatorial-problems instances. As a consequence of this work, a methodology to evaluate the difficulty of Travelling Salesman Problem instances is proposed and confronted to a wide set of instances, and finally a rank of their difficulty is stated.",
isbn="978-3-319-32034-2"
}

@phdthesis{lefrioux,
  TITLE = {{Towards more efficient parallel SAT solving}},
  AUTHOR = {Le Frioux, Ludovic},
  URL = {https://theses.hal.science/tel-03030122},
  NUMBER = {2019SORUS209},
  SCHOOL = {{Sorbonne Universit{\'e}}},
  YEAR = {2019},
  MONTH = Jul,
  KEYWORDS = {Parallelisation ; Boolean satisfiability ; Portfolio ; Divide-and-conquer ; Clause sharing ; Satisfaisabilit{\'e} bool{\'e}enne ; Parall{\'e}lisation ; Portfolio ; Diviser pour r{\'e}gner ; {\'E}change de clauses ; Outil},
  TYPE = {Theses},
  PDF = {https://theses.hal.science/tel-03030122v1/file/2019SORUS209.pdf},
  HAL_ID = {tel-03030122},
  HAL_VERSION = {v1},
}

@article{SMITHMILES2012875,
title = {Measuring instance difficulty for combinatorial optimization problems},
journal = {Computers \& Operations Research},
volume = {39},
number = {5},
pages = {875-889},
year = {2012},
issn = {0305-0548},
doi = {https://doi.org/10.1016/j.cor.2011.07.006},
url = {https://www.sciencedirect.com/science/article/pii/S0305054811001997},
author = {Kate Smith-Miles and Leo Lopes},
keywords = {Algorithm selection, Combinatorial optimization, Hardness prediction, Instance difficulty, Landscape analysis, Phase transition, Traveling salesman problem, Assignment problem, Knapsack problem, Bin-packing, Graph coloring, Timetabling},
abstract = {Discovering the conditions under which an optimization algorithm or search heuristic will succeed or fail is critical for understanding the strengths and weaknesses of different algorithms, and for automated algorithm selection. Large scale experimental studies – studying the performance of a variety of optimization algorithms across a large collection of diverse problem instances – provide the resources to derive these conditions. Data mining techniques can be used to learn the relationships between the critical features of the instances and the performance of algorithms. This paper discusses how we can adequately characterize the features of a problem instance that have impact on difficulty in terms of algorithmic performance, and how such features can be defined and measured for various optimization problems. We provide a comprehensive survey of the research field with a focus on six combinatorial optimization problems: assignment, traveling salesman, and knapsack problems, bin-packing, graph coloring, and timetabling. For these problems – which are important abstractions of many real-world problems – we review hardness-revealing features as developed over decades of research, and we discuss the suitability of more problem-independent landscape metrics. We discuss how the features developed for one problem may be transferred to study related problems exhibiting similar structures.}
}
@article{Gomes1997AlgorithmPD,
  title={Algorithm Portfolio Design: Theory vs. Practice},
  author={Carla Pedro Gomes and Bart Selman},
  journal={ArXiv},
  year={1997},
  volume={abs/1302.1541},
  url={https://api.semanticscholar.org/CorpusID:8512615}
}

@article{Huberman1997,
author = {Huberman, Bernardo A. and Lukose, Rajan M. and Hogg, Tad},
doi = {10.1126/science.275.5296.51},
issn = {00368075},
journal = {Science},
number = {5296},
pages = {51--54},
title = {{An economics approach to hard computational problems}},
volume = {275},
year = {1997}
}

@article{Kotthoff2014,
author = {Kotthoff, Lars},
journal = {AI Magazine},
title = {{Algorithm selection for combinatorial search problems: A survey}},
year = {2014},
volume={35},
pages = {48-69}, 
number = {3}
}  

@InProceedings{shavit_et_al,
  author =	{Shavit, Hadar and Hoos, Holger H.},
  title =	{{Revisiting SATZilla Features in 2024}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{27:1--27:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.27},
  URN =		{urn:nbn:de:0030-drops-205496},
  doi =		{10.4230/LIPIcs.SAT.2024.27},
  annote =	{Keywords: Satisfiability, feature extraction, running time prediction, satisfiability prediction}
}

@inproceedings{Yun,
author = {Yun, Xi and Epstein, Susan L.},
title = {Learning Algorithm Portfolios for Parallel Execution},
year = {2012},
isbn = {9783642344121},
publisher = {Springer-Verlag},
booktitle = {Revised Selected Papers of the 6th International Conference on Learning and Intelligent Optimization - Volume 7219},
pages = {323–338},
numpages = {16},
keywords = {parallel processing, algorithm portfolio, constraint satisfaction, machine learning},
location = {Paris, France},
series = {LION 6}
}

@article{satzilla,
author = {Xu, Lin and Hutter, Frank and Hoos, Holger H. and Leyton-Brown, Kevin},
title = {{SATzilla}: Portfolio-Based Algorithm Selection for {SAT}},
year = {2008},
issue_date = {May 2008},
publisher = {AI Access Foundation},
volume = {32},
number = {1},
issn = {1076-9757},
journal = {J. Artif. Int. Res.},
pages = {565–606},
numpages = {42}
}

@article{10.1162/evco_a_00215,
    author = {Kerschke, Pascal and Kotthoff, Lars and Bossek, Jakob and Hoos, Holger H. and Trautmann, Heike},
    title = "{Leveraging TSP Solver Complementarity through Machine Learning}",
    journal = {Evolutionary Computation},
    volume = {26},
    number = {4},
    pages = {597-620},
    year = {2018},
    issn = {1063-6560},
    doi = {10.1162/evco_a_00215},
    url = {https://doi.org/10.1162/evco\_a\_00215},
    eprint = {https://direct.mit.edu/evco/article-pdf/26/4/597/1552098/evco\_a\_00215.pdf},
}

@inproceedings{pmlr-v188-pulatov22a,
  title = {{Opening the Black Box: Automated Software Analysis for Algorithm Selection}},
  author = {Pulatov, Damir and Anastacio, Marie and Kotthoff, Lars and Hoos, Holger},
  booktitle = {Proceedings of the First International Conference on Automated Machine Learning},
  pages = {6/1--18},
  year={2022},
  publisher = {PMLR},
  volume = {188},
  pdf = {https://proceedings.mlr.press/v188/pulatov22a/pulatov22a.pdf},
  url = {https://proceedings.mlr.press/v188/pulatov22a.html}
}

@article{ppfolio,
  title={Description of ppfolio (2011)},
  author={Roussel, Olivier},
  journal={Proc. SAT Challenge},
  pages={46},
  year={2012}
}

@inproceedings{howe2000exploiting,
  title={Exploiting competitive planner performance},
  author={Howe, Adele E and Dahlman, Eric and Hansen, Christopher and Scheetz, Michael and Von Mayrhauser, Anneliese},
  booktitle={Recent Advances in AI Planning: 5th European Conference on Planning, ECP’99, Durham, UK, September 8-10, 1999. Proceedings 5},
  pages={62--72},
  year={2000},
  organization={Springer}
}

@inproceedings{roberts2008makes,
  title={{What Makes Planners Predictable?}},
  author={Roberts, Mark and Howe, Adele E and Wilson, Brandon and Marie desJardins},
  booktitle={ICAPS},
  pages={288--295},
  year={2008}
}

@inproceedings{p3s,
author = {Malitsky, Yuri and Sabharwal, Ashish and Samulowitz, Horst and Sellmann, Meinolf},
title = {{Parallel SAT Solver Selection and Scheduling}},
year = {2012},
isbn = {9783642335570},
publisher = {Springer-Verlag},
booktitle = {Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming - Volume 7514},
pages = {512–526},
numpages = {15}
}

@article{brighton2002advances,
  title={Advances in instance selection for instance-based learning algorithms},
  author={Brighton, Henry and Mellish, Chris},
  journal={Data mining and knowledge discovery},
  volume={6},
  pages={153--172},
  year={2002},
  publisher={Springer}
}
@article{ali2006learning,
  title={On learning algorithm selection for classification},
  author={Ali, Shawkat and Smith, Kate A},
  journal={Applied Soft Computing},
  volume={6},
  number={2},
  pages={119--138},
  year={2006},
  publisher={Elsevier}
}

@inproceedings{cenamor2013learning,
  title={Learning predictive models to configure planning portfolios},
  author={Cenamor, Isabel and De La Rosa, Tom{\'a}s and Fern{\'a}ndez, Fernando},
  booktitle={Proceedings of the 4th workshop on Planning and Learning (ICAPS-PAL 2013)},
  pages={14--22},
  year={2013},
  organization={Citeseer}
}

@article{Fawcett_Vallati_Hutter_Hoffmann_Hoos_Leyton-Brown_2014, 
title={{Improved Features for Runtime Prediction of Domain-Independent Planners}}, 
volume={24}, 
url={https://ojs.aaai.org/index.php/ICAPS/article/view/13680}, 
DOI={10.1609/icaps.v24i1.13680}, 
number={1}, 
journal={Proceedings of the International Conference on Automated Planning and Scheduling}, author={Fawcett, Chris and Vallati, Mauro and Hutter, Frank and Hoffmann, Jörg and Hoos, Holger and Leyton-Brown, Kevin}, 
year={2014}, 
pages={355-359} }

@inproceedings{flexfolio,
  title={An empirical study of per-instance algorithm scheduling},
  author={Lindauer, Marius and Bergdoll, Rolf-David and Hutter, Frank},
  booktitle={Proceedings
of the Tenth International Conference on Learning and Intelligent Optimization, LION’16, in: Lecture Notes in Computer Science},
  pages={253--259},
  year={2016},
  organization={Springer},
  publisher={Springer}
}

@inproceedings{10.1145/3411564.3411646,
author = {Batista dos Santos, V\^{a}nia and Merschmann, Luiz Henrique de Campos},
title = {Metalearning Applied to Multi-label Text Classification},
year = {2020},
isbn = {9781450388733},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3411564.3411646},
doi = {10.1145/3411564.3411646},
abstract = {Data Mining and Machine Learning fields have many techniques that can support data analysts in the text classification task. However, finding the most adequate techniques require advanced technical knowledge, exhaustive computational experiments and, consequently, time. To address this issue, researchers have proposed different approaches for selecting such techniques to be employed in classification tasks and the dynamic selection of classifiers is one of them. Therefore, this work proposes an approach that uses metalearning to automate the process of selecting the best classifier for each instance of a given multi-label textual dataset. Experiments were performed with multi-label text datasets and showed that the proposed approach is promising.},
booktitle = {Proceedings of the XVI Brazilian Symposium on Information Systems},
articleno = {36},
numpages = {8},
keywords = {dynamic algorithm selection, metalearning, multi-label classification, text classification},
location = {S\~{a}o Bernardo do Campo, Brazil},
series = {SBSI '20}
}

@article{10.1145/3637225,
author = {Leeson, Will and Dwyer, Matthew B.},
title = {{Algorithm Selection for Software Verification Using Graph Neural Networks}},
year = {2024},
issue_date = {March 2024},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {33},
number = {3},
issn = {1049-331X},
url = {https://doi.org/10.1145/3637225},
doi = {10.1145/3637225},
abstract = {The field of software verification has produced a wide array of algorithmic techniques that can prove a variety of properties of a given program. It has been demonstrated that the performance of these techniques can vary up to 4 orders of magnitude on the same verification problem. Even for verification experts, it is difficult to decide which tool will perform best on a given problem. For general users, deciding the best tool for their verification problem is effectively impossible. In this work, we present Graves, a selection strategy based on graph neural networks (GNNs). Graves generates a graph representation of a program from which a GNN predicts a score for a verifier that indicates its performance on the program. We evaluate Graves on a set of 10 verification tools and over 8,000 verification problems and find that it improves the state-of-the-art in verification algorithm selection by 12\%, or 8 percentage points. Further, it is able to verify 9\% more problems than any existing verifier on our test set. Through a qualitative study on model interpretability, we find strong evidence that the Graves model learns to base its predictions on factors that relate to the unique features of the algorithmic techniques.},
journal = {ACM Trans. Softw. Eng. Methodol.},
month = {mar},
articleno = {76},
numpages = {36},
keywords = {Algorithm selection, graph neural networks}
}

@INPROCEEDINGS{9463528,
  author={Wang, Qiang and Jiang, Jiawei and Zhao, Yongxin and Cao, Weipeng and Wang, Chunjiang and Li, Shengdong},
  booktitle={2021 7th IEEE Intl Conference on Big Data Security on Cloud (BigDataSecurity), IEEE Intl Conference on High Performance and Smart Computing, (HPSC) and IEEE Intl Conference on Intelligent Data and Security (IDS)}, 
  title={{Algorithm selection for software verification based on adversarial LSTM}}, 
  year={2021},
  volume={},
  number={},
  pages={87-92},
  keywords={Conferences;Software algorithms;Tools;Big Data;Prediction algorithms;Software;Security;software verification;Algorithm Selection;Machine Learning},
  doi={10.1109/BigDataSecurityHPSCIDS52275.2021.00026}}

@article{10.1007/s10515-020-00270-x,
author = {Richter, Cedric and H\"{u}llermeier, Eyke and Jakobs, Marie-Christine and Wehrheim, Heike},
title = {Algorithm selection for software validation based on graph kernels},
year = {2020},
issue_date = {Jun 2020},
publisher = {Kluwer Academic Publishers},
address = {USA},
volume = {27},
number = {1–2},
issn = {0928-8910},
url = {https://doi.org/10.1007/s10515-020-00270-x},
doi = {10.1007/s10515-020-00270-x},
abstract = {Algorithm selection is the task of choosing an algorithm from a given set of candidate algorithms when faced with a particular problem instance. Algorithm selection via machine learning (ML) has recently been successfully applied for various problem classes, including computationally hard problems such as SAT. In this paper, we study algorithm selection for software validation, i.e., the task of choosing a software validation tool for a given validation instance. A validation instance consists of a program plus properties to be checked on it. The application of machine learning techniques to this task first of all requires an appropriate representation of software. To this end,
we propose a dedicated kernel function, which compares two programs in terms of their similarity, thus making the algorithm selection task amenable to kernel-based machine learning methods. Our kernel operates on a graph representation of source code mixing elements of control-flow and program-dependence graphs with abstract syntax trees.
Thus, given two such representations as input, the kernel function yields a real-valued score that can be interpreted as a degree of similarity. We experimentally evaluate our kernel in two learning scenarios, namely a classification and a ranking problem: (1) selecting between a verification and a testing tool for bug finding (i.e., property violation), and (2) ranking several verification tools,
from presumably best to worst, for property proving. The evaluation, which is based on data sets from the annual software verification competition SV-COMP, demonstrates our kernel to generalize well and to achieve rather high prediction accuracy, both for the classification and the ranking task.},
journal = {Automated Software Engg.},
month = {jun},
pages = {153–186},
numpages = {34},
keywords = {Algorithm selection, Software validation, Machine learning, Graph kernels, Verification, Testing}
}

@INPROCEEDINGS{10.4108/ICST.SIMUTOOLS2009.5659,
    author={Roland  Ewald and Adelinde M.  Uhrmacher and Kaustav  Saha},
    title={Data mining for simulation algorithm selection},
    proceedings={2nd International ICST Conference on Simulation Tools and Techniques},
    publisher={ICST},
    proceedings_a={SIMUTOOLS},
    year={2010},
    month={5},
    keywords={Algorithm Selection Data Mining Simulation Performance Analysis},
    doi={10.4108/ICST.SIMUTOOLS2009.5659}
}
@InProceedings{GCP,
author="Musliu, Nysret
and Schwengerer, Martin",
editor="Nicosia, Giuseppe
and Pardalos, Panos",
title="{Algorithm Selection for the Graph Coloring Problem}",
booktitle="Learning and Intelligent Optimization",
year="2013",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="389--403",
abstract="We present an automated algorithm selection method based on machine learning for the graph coloring problem (GCP). For this purpose, we identify {\$}{\$}78{\$}{\$}78features for this problem and evaluate the performance of six state-of-the-art (meta) heuristics for the GCP. We use the obtained data to train several classification algorithms that are applied to predict on a new instance the algorithm with the highest expected performance. To achieve better performance for the machine learning algorithms, we investigate the impact of parameters, and evaluate different data discretization and feature selection methods. Finally, we evaluate our approach, which exploits the existing GCP techniques and the automated algorithm selection, and compare it with existing heuristic algorithms. Experimental results show that the GCP solver based on machine learning outperforms previous methods on benchmark instances.",
isbn="978-3-642-44973-4"
}

@article{KOCAMAZ201394,
title = {Increasing the efficiency of quicksort using a neural network based algorithm selection model},
journal = {Information Sciences},
volume = {229},
pages = {94-105},
year = {2013},
issn = {0020-0255},
doi = {https://doi.org/10.1016/j.ins.2012.11.014},
url = {https://www.sciencedirect.com/science/article/pii/S0020025512007670},
author = {Uğur Erkin Kocamaz},
keywords = {Neural algorithm selection, Sorting algorithm selection, Quicksort, Sorting, Algorithm selection, Neural networks},
abstract = {Quicksort is one of the most popular sorting algorithms, it is based on a divide-and-conquer technique and has a wide acceptance as the fastest general-purpose sorting technique. Though it is successful in separating large partitions into small ones, quicksort runs slowly when it processes its small partitions, for which completing the sorting through using a different sorting algorithm is much plausible solution. This variant minimizes the overall execution time but it switches to a constant sorting algorithm at a constant cut-off point. To cope with this constancy problem, it has been suggested that a dynamic model which can choose the fastest sorting algorithm for the small partitions. The model includes continuation with quicksort so that the cut-off point is also more flexible. To implement this with an intelligent algorithm selection model, artificial neural networks are preferred due to their non-comparison, constant-time and low-cost architecture features. In spite of the fact that finding the best sorting algorithm by using a neural network causes some extra computational time, the gain in overall execution time is greater. As a result, a faster variant of quicksort has been implemented by using artificial neural network based algorithm selection approach. Experimental results of the proposed algorithm and the several other fast sorting algorithms have been presented, compared and discussed.}
}

@article{ 10.5120/ijca2016910726,
author = { Somshubra Majumdar, Ishaan Jain, Kunal Kukreja },
title = {{AdaSort: Adaptive Sorting using Machine Learning}},
journal = { International Journal of Computer Applications },
issue_date = { Jul 2016 },
volume = { 145 },
number = { 12 },
month = { Jul },
year = { 2016 },
issn = { 0975-8887 },
pages = { 12-17 },
numpages = {9},
url = { https://ijcaonline.org/archives/volume145/number12/25328-2016910726/ },
doi = { 10.5120/ijca2016910726 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
}

@inproceedings{10.1109/CEC55065.2022.9870417,
author = {Sitaru, Ioana and Raschip, Madalina},
title = {{Algorithm Selection for Combinatorial Packing Problems}},
year = {2022},
publisher = {IEEE Press},
url = {https://doi.org/10.1109/CEC55065.2022.9870417},
doi = {10.1109/CEC55065.2022.9870417},
abstract = {This paper describes a way of building an algorithm selection system for the two-dimensional rectangle packing problem. A list of features was defined, and five heuristics and metaheuristics were selected as solvers. The first step involves the extraction of features from the input problem instances. Using those computed features, machine learning regressors will predict the performance of each solver on the instance and, therefore, find the most fitted algorithm for it. Both the predicted execution time and the expected quality of the solution were used as performance metrics for the selection step. The experimental results showed that the built system has a high accuracy in predicting the best algorithm based on the runtime execution and the solution quality. Moreover, the system achieves these results with much lower computational resources than running the actual solvers of the problem.},
booktitle = {2022 IEEE Congress on Evolutionary Computation (CEC)},
pages = {1–8},
numpages = {8},
location = {Padua, Italy}
}

@inproceedings{NIPS2014_7fb8ceb3,
 author = {Lieder, Falk and Plunkett, Dillon and Hamrick, Jessica B and Russell, Stuart J and Hay, Nicholas and Griffiths, Tom},
 booktitle = {Advances in Neural Information Processing Systems},
 editor = {Z. Ghahramani and M. Welling and C. Cortes and N. Lawrence and K.Q. Weinberger},
 pages = {},
 publisher = {Curran Associates, Inc.},
 title = {Algorithm selection by rational metareasoning as a model of human strategy selection},
 url = {https://proceedings.neurips.cc/paper_files/paper/2014/file/7fb8ceb3bd59c7956b1df66729296a4c-Paper.pdf},
 volume = {27},
 year = {2014}
}

@techreport{hyvarinen2012approaches,
author = {Hyvarinen, Antti E. J. and Wintersteiger, Christoph M.},
title = {{Approaches for Multi-Core Propagation in Clause Learning Satisfiability Solvers}},
year = {2012},
month = {May},
abstract = {Parallelization of unit propagation in SAT solvers is a compelling way of obtaining an efficient parallel decision procedure for the propositional satisfiability problem. However, due to the P-completeness of unit propagation, it is challenging to achieve good efficiency in practice. In this article, we present two methods for unit propagation on multi-core systems and their implementation. We throughly evaluate these techniques by comparison to a simulation that estimates a baseline efficiency and by experimental evaluation of an implementation on competition benchmarks. We thereby demonstrate that achieving a speed-up linear in the number of cores is indeed challenging in practice, but also that unit propagation on multi-core systems is feasible in practice.},
url = {https://www.microsoft.com/en-us/research/publication/approaches-for-multi-core-propagation-in-clause-learning-satisfiability-solvers/},
number = {MSR-TR-2012-47},
}

@inproceedings{Biere2013LingelingPA,
  title={{Lingeling, Plingeling and Treengeling Entering the SAT Competition 2013}},
  author={Armin Biere},
  year={2013},
  url={https://api.semanticscholar.org/CorpusID:972178}
}

@article{plingeling,
author = {Biere, Armin},
year = {2012},
month = {01},
pages = {33-34},
title = {{Lingeling and friends entering the SAT challenge 2012}},
journal = {Department of Computer Science Series of Publications B}
}

@phdthesis{sotingAS,
author = {Guo, Haipeng and Hsu, William H.},
title = {Algorithm selection for sorting and probabilistic inference: a machine learning-based approach},
year = {2003},
publisher = {Kansas State University},
address = {USA},
abstract = {The  algorithm selection problem  aims at selecting the best algorithm for a given computational problem instance according to some characteristics of the instance. In this dissertation, we first introduce some results from theoretical investigation of the algorithm selection problem. We show, by Rice's theorem, the nonexistence of an automatic algorithm selection program based only on the description of the input instance and the competing hardness and algorithm performance based on Kolmogorov complexity to show that algorithm selection for search is also incomputable. Driven by the theoretical results, we propose a machine learning-based inductive approach using experimental algorithmic methods and machine learning techniques to solve the algorithm selection problem. Experimentally, we have applied the proposed methodology to algorithm selection for sorting and the MPE problem. In sorting, instances with an existing order are easier for some algorithms. We have studied different presortedness measures, designed algorithms to generate permutations with a specified existing order uniformly at random, and applied various learning algorithms to induce sorting algorithm selection models from runtime experimental results. In the MPE problem, the instance characteristics we have studied include size and topological type of the network, network connectedness, skewness of the distributions in Conditional Probability Tables (CPTs), and the proportion and distribution of evidence variables. The MPE algorithms considered include an exact algorithm (clique-tree propagation), two stochastic sampling algorithms (MCMC Gibbs sampling and importance forward sampling), two search-based algorithms (multi-restart hill-climbing and tabu search), and one hybrid algorithm combining both sampling and search (ant colony optimization). Another major contribution of this dissertation is the discovery of multifractal properties of the joint probability distributions of Bayesian networks. With sufficient asymmetry in individual prior and conditional probability distributions, the joint distribution is not only highly skewed, but it also has clusters of high-probability instantiations at all scales. We present a two phase hybrid random sampling and search algorithm to solve the MPE problem exploiting this clustering property. Since the MPE problem (decision version) is  NP -complete, the multifractal meta-heuristic can be applied to solve other  NP -hard combinatorial optimization problems as well.},
note = {AAI3100557}
}

@inproceedings{10.1145/2487575.2487629,
author = {Thornton, Chris and Hutter, Frank and Hoos, Holger H. and Leyton-Brown, Kevin},
title = {{Auto-WEKA: combined selection and hyperparameter optimization of classification algorithms}},
year = {2013},
isbn = {9781450321747},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2487575.2487629},
doi = {10.1145/2487575.2487629},
abstract = {Many different machine learning algorithms exist; taking into account each algorithm's hyperparameters, there is a staggeringly large number of possible alternatives overall. We consider the problem of simultaneously selecting a learning algorithm and setting its hyperparameters, going beyond previous work that attacks these issues separately. We show that this problem can be addressed by a fully automated approach, leveraging recent innovations in Bayesian optimization. Specifically, we consider a wide range of feature selection techniques (combining 3 search and 8 evaluator methods) and all classification approaches implemented in WEKA's standard distribution, spanning 2 ensemble methods, 10 meta-methods, 27 base classifiers, and hyperparameter settings for each classifier. On each of 21 popular datasets from the UCI repository, the KDD Cup 09, variants of the MNIST dataset and CIFAR-10, we show classification performance often much better than using standard selection and hyperparameter optimization methods. We hope that our approach will help non-expert users to more effectively identify machine learning algorithms and hyperparameter settings appropriate to their applications, and hence to achieve improved performance.},
booktitle = {Proceedings of the 19th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining},
pages = {847–855},
numpages = {9},
keywords = {weka, model selection, hyperparameter optimization},
location = {Chicago, Illinois, USA},
series = {KDD '13}
}

@InProceedings{explainability,
author="Visentin, Andrea
and Gallch{\'o}ir, Aodh {\'O}
and K{\"a}rcher, Jens
and Meyr, Herbert",
editor="Dilkina, Bistra",
title="{Explainable Algorithm Selection for the Capacitated Lot Sizing Problem}",
booktitle="Integration of Constraint Programming, Artificial Intelligence, and Operations Research",
year="2024",
publisher="Springer Nature Switzerland",
address="Cham",
pages="243--252",
abstract="Algorithm selection is a class of meta-algorithms that has emerged as a crucial approach for solving complex combinatorial optimization problems. Successful algorithm selection involves navigating a diverse landscape of solvers, each designed with distinct heuristics and search strategies. It is a classification problem in which statistical features of a problem instance are used to select the algorithm that should tackle it most efficiently. However, minimal attention has been given to investigating algorithm selection decisions. This work presents a framework for iterative feature selection and explainable multi-class classification in Algorithm Selection for the Capacitated Lot Sizing Problem (CLSP). The CLSP is a combinatorial optimization problem widely studied with important industrial applications. The framework reduces the features considered by the machine learning approach and uses SHAP analysis to investigate their contribution to the selection. The analysis shows which instance type characteristics positively affect the relative performance of a heuristic. The approach can be used to improve the algorithm selection's transparency and inform the developer of an algorithm's weak and strong points. The experimental analysis shows that the framework selector provides valuable insights with a narrow optimality gap close to a parallel deployment of the heuristic set that generalises well to instances considerably bigger than the training ones.",
isbn="978-3-031-60599-4"
}


@INPROCEEDINGS{FlorinaOpneMP,
  author={Ciorba, Florina M. and Mohammed, Ali and Korndörfer, Jonas H. Müller and Eleliemy, Ahmed},
  booktitle={2023 22nd International Symposium on Parallel and Distributed Computing (ISPDC)}, 
  title={{Automated Scheduling Algorithm Selection in OpenMP}}, 
  year={2023},
  volume={},
  number={},
  pages={106-109},
  keywords={Scheduling algorithms;Runtime library;High performance computing;Memory management;Diversity reception;Oral communication;Manuals;algorithm selection;self-scheduling;dynamic load balancing;OpenMP;multithreaded programming;shared-memory systems;runtime library;automated selection;expert methods;machine learning;reinforcement learning},
  doi={10.1109/ISPDC59212.2023.00025}}


@Inbook{Vanschoren2019,
author="Vanschoren, Joaquin",
editor="Hutter, Frank
and Kotthoff, Lars
and Vanschoren, Joaquin",
title="Meta-Learning",
bookTitle="Automated Machine Learning: Methods, Systems, Challenges",
year="2019",
publisher="Springer International Publishing",
address="Cham",
pages="35--61",
abstract="Meta-learning, or learning to learn, is the science of systematically observing how different machine learning approaches perform on a wide range of learning tasks, and then learning from this experience, or meta-data, to learn new tasks much faster than otherwise possible. Not only does this dramatically speed up and improve the design of machine learning pipelines or neural architectures, it also allows us to replace hand-engineered algorithms with novel approaches learned in a data-driven way. In this chapter, we provide an overview of the state of the art in this fascinating and continuously evolving field.",
isbn="978-3-030-05318-5",
doi="10.1007/978-3-030-05318-5_2",
url="https://doi.org/10.1007/978-3-030-05318-5_2"
}


@book{hutter2019automated,
title = {Automated Machine Learning - Methods, Systems, Challenges},
editor = {Frank Hutter and Lars Kotthoff and Joaquin Vanschoren},
year = {2019},
publisher = {Springer},
keywords = {}
} 

@book{brazdil2022metalearning,
  title={Metalearning: Applications to Automated Machine Learning and Data Mining},
  author={Brazdil, P. and van Rijn, J.N. and Soares, C. and Vanschoren, J.},
  isbn={9783030670238},
  series={Cognitive Technologies},
  url={https://books.google.com/books?id=zDcOzgEACAAJ},
  year={2022},
  publisher={Springer International Publishing}
}

@misc{erdem_ku__2024,
        title={{Frugal Algorithm Selection}},
        author={ Erdem Kuş and Özgür Akgün and Nguyen Dang and Ian Miguel },
        year={ 2024 },
        publisher={ Cornell University },
        doi={ 10.48550/arxiv.2405.11059 },  
      }
@article{sunnycp, 
title={SUNNY-CP and the MiniZinc challenge}, 
volume={18}, DOI={10.1017/S1471068417000205}, 
number={1}, 
journal={Theory and Practice of Logic Programming}, 
publisher={Cambridge University Press}, 
author={Amadini, Roberto and Gabbrielli, Maurizio and Mauro, Jacopo}, 
year={2018}, 
pages={81–96}
}

@inproceedings{sunnycp2,
author = {Amadini, Roberto and Gabbrielli, Maurizio and Mauro, Jacopo},
title = {{A Multicore Tool for Constraint Solving}},
year = {2015},
isbn = {9781577357384},
booktitle = {Proceedings of the 24th International Conference on Artificial Intelligence},
pages = {232–238},
numpages = {7}
}

@article{sunny,
  author    = {Roberto Amadini and
               Maurizio Gabbrielli and
               Jacopo Mauro},
  title     = {{SUNNY:} a Lazy Portfolio Approach for Constraint Solving},
  journal   = {Theory Pract. Log. Program.},
  volume    = {14},
  number    = {4-5},
  pages     = {509--524},
  year      = {2014},
  url       = {https://doi.org/10.1017/S1471068414000179},
  doi       = {10.1017/S1471068414000179},
  timestamp = {Sat, 09 Apr 2022 12:21:06 +0200},
  biburl    = {https://dblp.org/rec/journals/tplp/AmadiniGM14.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{biere,
  title={{Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures}},
  author={Aigner, Martin and Biere, Armin and Kirsch, Christoph M and Niemetz, Aina and Preiner, Mathias},
  journal={POS@ SAT},
  volume={29},
  pages={28--40},
  year={2013}
}

@article{lindauer2015autofolio,
  title={Autofolio: An automatically configured algorithm selector},
  author={Lindauer, Marius and Hoos, Holger H and Hutter, Frank and Schaub, Torsten},
  journal={Journal of Artificial Intelligence Research},
  volume={53},
  pages={745--778},
  year={2015}
}

@inproceedings{10.5555/2898607.2898641,
author = {Xu, Lin and Hoos, Holger H. and Leyton-Brown, Kevin},
title = {{Hydra: Automatically Configuring Algorithms for Portfolio-Based Selection}},
year = {2010},
publisher = {AAAI Press},
booktitle = {Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence},
pages = {210–216},
number={1},
numpages = {7},
series = {AAAI'10}
}

@inproceedings{XuEtAl11,
  title={{Hydra-MIP: Automated algorithm configuration and selection for mixed integer programming}},
  author={Xu, Lin and Hutter, Frank and Hoos, Holger H and Leyton-Brown, Kevin},
  pages={16--30},
  year={2011}, 
  booktitle={Proceedings of the 18th RCRA workshop}
}

@article{aspeed,
  title = {{aspeed: Solver scheduling via answer set programming}},
  author = {Hoos, Holger H. and Kaminski, Roland and Lindauer, Marius Thomas and Schaub, Torsten},
  journal = {{TPLP}},
  number = {1},
  pages = {117--142},
  volume = {15},
  year = {2015}
}

@inproceedings{cphydra,
  title={Using case-based reasoning in an algorithm portfolio for constraint solving},
  author={O’Mahony, Eoin and Hebrard, Emmanuel and Holland, Alan and Nugent, Conor and O’Sullivan, Barry},
  booktitle={Irish conference on artificial intelligence and cognitive science},
  pages={210--216},
  year={2008}, 
  publisher={Proceedings of the 19th Irish Conference on Artificial Intelligence and Cognitive Science}
}


@ARTICLE{585893,
  author={Wolpert, D.H. and Macready, W.G.},
  journal={IEEE Transactions on Evolutionary Computation}, 
  title={No free lunch theorems for optimization}, 
  year={1997},
  volume={1},
  number={1},
  pages={67-82},
  keywords={Iron;Evolutionary computation;Information theory;Minimax techniques;Simulated annealing;Algorithm design and analysis;Performance analysis;Probability distribution;Bayesian methods},
  doi={10.1109/4235.585893}}

@Inbook{Karp1972,
author="Karp, Richard M.",
editor="Miller, Raymond E.
and Thatcher, James W.
and Bohlinger, Jean D.",
title="Reducibility among Combinatorial Problems",
bookTitle="Complexity of Computer Computations: Proceedings of a symposium on the Complexity of Computer Computations, held March 20--22, 1972, at the IBM Thomas J. Watson Research Center, Yorktown Heights, New York, and sponsored by the Office of Naval Research, Mathematics Program, IBM World Trade Corporation, and the IBM Research Mathematical Sciences Department",
year="1972",
publisher="Springer US",
address="Boston, MA",
pages="85--103",
abstract="A large class of computational problems involve the determination of properties of graphs, digraphs, integers, arrays of integers, finite families of finite sets, boolean formulas and elements of other countable domains. Through simple encodings from such domains into the set of words over a finite alphabet these problems can be converted into language recognition problems, and we can inquire into their computational complexity. It is reasonable to consider such a problem satisfactorily solved when an algorithm for its solution is found which terminates within a number of steps bounded by a polynomial in the length of the input. We show that a large number of classic unsolved problems of covering, matching, packing, routing, assignment and sequencing are equivalent, in the sense that either each of them possesses a polynomial-bounded algorithm or none of them does.",
isbn="978-1-4684-2001-2",
doi="10.1007/978-1-4684-2001-2_9",
url="https://doi.org/10.1007/978-1-4684-2001-2_9"
}


@article{Tange2011a,
  title = {{GNU Parallel - The Command-Line Power Tool}},
  author = {O. Tange},
  journal = {The USENIX Magazine},
  number = {1},
  volume = {36},
  url = {http://www.gnu.org/s/parallel},
  year = {2011},
  pages = {42-47},
  doi = {http://dx.doi.org/10.5281/zenodo.16303}
}

@article{BISCHL201641,
title = "{ASlib}: A benchmark library for algorithm selection",
journal = "Artificial Intelligence",
volume = "237",
pages = "41 - 58",
year = "2016",
author = "Bernd Bischl and Pascal Kerschke and Lars Kotthoff and Marius Lindauer and Yuri Malitsky and Alexandre Fr{\'e}chette and Holger Hoos and Frank Hutter and Kevin Leyton-Brown and Kevin Tierney and Joaquin Vanschoren",
keywords = "Algorithm selection, Machine learning, Empirical performance estimation"
}
@BOOK{Balyo2016,
  title = "Proceedings of {SAT} Competition 2016 : Solver and Benchmark Descriptions",
  author = "Martins, Ruben and Jarvisalo, Matti and Bacchus, Fahiem",
  year = 2016,
  publisher = "University of Helsinki", 
  issn = {1458-4786},
  isbn = {978-951-51-2345-9}
}

@article {jtom1286288,
	journal = {Journal of Turkish Operations Management},
	issn = {2630-6433},
	eissn = {2630-6433},
	publisher = {Ankara Yildirim Beyazit University},
	year = {2023},
	volume = {7},
	number = {1},
	pages = {1579 - 1590},
	doi = {10.56554/jtom.1286288},
	title = {{A Monte Carlo simulation approach to the gap-time relationship in solving scheduling problem}},
	key = {cite},
	author = {Torağay,  Oğuz and Pouya,  Shaheen}
}

@BOOK{maxsat2019,
  title = "MaxSAT Evaluation 2019",
  author = "Bacchus, Fahiem and Jarvisalo, Matti and Martins, Ruben",
  year =  2019
  }

@article{LINDAUER201986,
title = {{The algorithm selection competitions 2015 and 2017}},
journal = {Artificial Intelligence},
volume = {272},
pages = {86-100},
year = {2019},
issn = {0004-3702},
doi = {https://doi.org/10.1016/j.artint.2018.10.004},
url = {https://www.sciencedirect.com/science/article/pii/S000437021830198X},
author = {Marius Lindauer and Jan N. {van Rijn} and Lars Kotthoff},
keywords = {Algorithm Selection, Meta-Learning, Competition Analysis},
abstract = {The algorithm selection problem is to choose the most suitable algorithm for solving a given problem instance. It leverages the complementarity between different approaches that is present in many areas of AI. We report on the state of the art in algorithm selection, as defined by the Algorithm Selection competitions in 2015 and 2017. The results of these competitions show how the state of the art improved over the years. We show that although performance in some cases is very good, there is still room for improvement in other cases. Finally, we provide insights into why some scenarios are hard, and pose challenges to the community on how to advance the current state of the art.}
}

@inproceedings {Gonard2019,
author="Gonard, Fran{\c{c}}ois
and Schoenauer, Marc
and Sebag, Mich{\`e}le",
title="{Algorithm Selector and Prescheduler in the ICON Challenge}",
bookTitle="Bioinspired Heuristics for Optimization",
year="2019",
publisher="Springer International Publishing",
pages="203-219"
}

@article{SINZ2001205,
title = {{PaSAT — Parallel SAT-Checking with Lemma Exchange: Implementation and Applications}},
journal = {Electronic Notes in Discrete Mathematics},
volume = {9},
pages = {205-216},
year = {2001},
note = {LICS 2001 Workshop on Theory and Applications of Satisfiability Testing (SAT 2001)},
issn = {1571-0653},
doi = {https://doi.org/10.1016/S1571-0653(04)00323-3},
url = {https://www.sciencedirect.com/science/article/pii/S1571065304003233},
author = {Carsten Sinz and Wolfgang Blochinger and Wolfgang Küchlin},
keywords = {parallel algorithms, learning cooperating agents, applications},
abstract = {We present PaSAT, a parallel implementation of a Davis-Putnam-style prepositional satisfiability checker incorporating dynamic search space partitioning, intelligent backjumping, as well as lemma generation and exchange; the main focus of our implementation is on speeding up SAT-checking of prepositional encodings of real-world combinatorial problems. We investigate and analyze the speed-ups obtained by parallelization in conjunction with lemma exchange and describe the effects we observed during our experiments. Finally, we present performance measurements from the application of our prover in the areas of formal consistency checking of industrial product documentation, cryptanalysis, and hardware verification. We would like to thank Jürgen Ellinger for help on carrying out the experiments.}
}

@InProceedings{10.1007/978-3-642-31612-8_18,
author="Xu, Lin
and Hutter, Frank
and Hoos, Holger
and Leyton-Brown, Kevin",
editor="Cimatti, Alessandro
and Sebastiani, Roberto",
title="{Evaluating Component Solver Contributions to Portfolio-Based Algorithm Selectors}",
booktitle="Theory and Applications of Satisfiability Testing -- SAT 2012",
year="2012",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="228--241",
abstract="Portfolio-based methods exploit the complementary strengths of a set of algorithms and---as evidenced in recent competitions---represent the state of the art for solving many NP-hard problems, including SAT. In this work, we argue that a state-of-the-art method for constructing portfolio-based algorithm selectors, {\$}{\backslash}texttt{\{}SATzilla{\}}{\$}, also gives rise to an automated method for quantifying the importance of each of a set of available solvers. We entered a substantially improved version of {\$}{\backslash}texttt{\{}SATzilla{\}}{\$}to the inaugural ``analysis track'' of the 2011 SAT competition, and draw two main conclusions from the results that we obtained. First, automatically-constructed portfolios of sequential, non-portfolio competition entries perform substantially better than the winners of all three sequential categories. Second, and more importantly, a detailed analysis of these portfolios yields valuable insights into the nature of successful solver designs in the different categories. For example, we show that the solvers contributing most to {\$}{\backslash}texttt{\{}SATzilla{\}}{\$}were often not the overall best-performing solvers, but instead solvers that exploit novel solution strategies to solve instances that would remain unsolved without them.",
isbn="978-3-642-31612-8"
}
@inproceedings{collautti2013snnap,
  title={{SNNAP: Solver-based nearest neighbor for algorithm portfolios}},
  author={Collautti, Marco and Malitsky, Yuri and Mehta, Deepak and O’Sullivan, Barry},
  booktitle={Machine Learning and Knowledge Discovery in Databases: European Conference, ECML PKDD 2013, Prague, Czech Republic, September 23-27, 2013, Proceedings, Part III 13},
  pages={435--450},
  year={2013},
  organization={Springer}
}

@InProceedings{10.1007/978-3-642-20895-9_40,
author="Gebser, Martin
and Kaminski, Roland
and Kaufmann, Benjamin
and Schaub, Torsten
and Schneider, Marius Thomas
and Ziller, Stefan",
editor="Delgrande, James P.
and Faber, Wolfgang",
title="{A Portfolio Solver for Answer Set Programming: Preliminary Report}",
booktitle="Logic Programming and Nonmonotonic Reasoning",
year="2011",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="352--357",
abstract="We propose a portfolio-based solving approach to Answer Set Programming (ASP). Our approach is homogeneous in considering several configurations of the ASP solver clasp. The selection among the configurations is realized via Support Vector Regression. The resulting portfolio-based solver claspfolio regularly outperforms clasp's default configuration as well as manual tuning.",
isbn="978-3-642-20895-9"
}

@inproceedings{10.5555/2540128.2540217,
author = {Malitsky, Yuri and Sabharwal, Ashish and Samulowitz, Horst and Sellmann, Meinolf},
title = {{Algorithm portfolios based on cost-sensitive hierarchical clustering}},
year = {2013},
isbn = {9781577356332},
publisher = {AAAI Press},
abstract = {Different solution approaches for combinatorial problems often exhibit incomparable performance that depends on the concrete problem instance to be solved. Algorithm portfolios aim to combine the strengths of multiple algorithmic approaches by training a classifier that selects or schedules solvers dependent on the given instance. We devise a new classifier that selects solvers based on a cost-sensitive hierarchical clustering model. Experimental results on SAT and MaxSAT show that the new method outperforms the most effective portfolio builders to date.},
booktitle = {Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence},
pages = {608–614},
numpages = {7},
location = {Beijing, China},
series = {IJCAI '13}
}

@InProceedings{10.1007/978-3-030-80223-3_31,
author="Pimpalkhare, Nikhil
and Mora, Federico
and Polgreen, Elizabeth
and Seshia, Sanjit A.",
editor="Li, Chu-Min
and Many{\`a}, Felip",
title="{MedleySolver: Online SMT Algorithm Selection}",
booktitle="Theory and Applications of Satisfiability Testing -- SAT 2021",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="453--470",
abstract="Satisfiability modulo theories (SMT) solvers implement a wide range of optimizations that are often tailored to a particular class of problems, and that differ significantly between solvers. As a result, one solver may solve a query quickly while another might be flummoxed completely. Predicting the performance of a given solver is difficult for users of SMT-driven applications, particularly when the problems they have to solve do not fall neatly into a well-understood category. In this paper, we propose an online algorithm selection framework for SMT called MedleySolver that predicts the relative performances of a set of SMT solvers on a given query, distributes time amongst the solvers, and deploys the solvers in sequence until a solution is obtained. We evaluate MedleySolver against the best available alternative, an offline learning technique, in terms of pure performance and practical usability for a typical SMT user. We find that with no prior training, MedleySolver solves 93.9{\%} of the queries solved by the virtual best solver selector achieving 59.8{\%} of the par-2 score of the most successful individual solver, which solves 87.3{\%}. For comparison, the best available alternative takes longer to train than MedleySolver takes to solve our entire set of 2000 queries.",
isbn="978-3-030-80223-3"
}


@InProceedings{10.1007/3-540-46135-3_37,
author="Leyton-Brown, Kevin
and Nudelman, Eugene
and Shoham, Yoav",
editor="Van Hentenryck, Pascal",
title="{Learning the Empirical Hardness of Optimization Problems: The Case of Combinatorial Auctions}",
booktitle="Principles and Practice of Constraint Programming - CP 2002",
year="2002",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="556--572",
abstract="We propose a new approach for understanding the algorithm-specific empirical hardness of -Hard problems. In this work we focus on the empirical hardness of the winner determination problem---an optimization problem arising in combinatorial auctions---when solved by ILOG's CPLEX software. We consider nine widely-used problem distributions and sample randomly from a continuum of parameter settings for each distribution. We identify a large number of distribution-nonspecific features of data instances and use statistical regression techniques to learn, evaluate and interpret a function from these features to the predicted hardness of an instance.",
isbn="978-3-540-46135-7"
}


@article{genericportfolio,
author = {Liu, Wenwen and Yuen, Shiu Yin and Sung, Chi},
year = {2022},
month = {09},
pages = {1-18},
title = {A generic method to compose an algorithm portfolio with a problem set of unknown distribution},
volume = {14},
journal = {Memetic Computing},
doi = {10.1007/s12293-022-00367-8}
}

@InProceedings{10.1007/978-3-642-31612-8_17,
author="Hyv{\"a}rinen, Antti E. J.
and Manthey, Norbert",
editor="Cimatti, Alessandro
and Sebastiani, Roberto",
title="{Designing Scalable Parallel SAT Solvers}",
booktitle="Theory and Applications of Satisfiability Testing -- SAT 2012",
year="2012",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="214--227",
abstract="Solving instances of the propositional satisfiability problem (SAT) in parallel has received a significant amount of attention as the number of cores in a typical workstation is steadily increasing. With the increase of the number of cores, in particular the scalability of such approaches becomes essential for fully harnessing the potential of modern architectures. The best parallel SAT solvers have, until recently, been based on algorithm portfolios, while search-space partitioning approaches have been less successful. We prove, under certain natural assumptions on the partitioning function, that search-space partitioning can always result in an increased expected run time, justifying the success of the portfolio approaches. Furthermore, we give first controlled experiments showing that an approach combining elements from partitioning and portfolios scales better than either of the two approaches and succeeds in solving instances not solved in a recent solver competition.",
isbn="978-3-642-31612-8"
}


@InProceedings{10.1007/978-3-642-16242-8_27,
author="Hyv{\"a}rinen, Antti E. J.
and Junttila, Tommi
and Niemel{\"a}, Ilkka",
editor="Ferm{\"u}ller, Christian G.
and Voronkov, Andrei",
title="{Partitioning SAT Instances for Distributed Solving}",
booktitle="Logic for Programming, Artificial Intelligence, and Reasoning",
year="2010",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="372--386",
abstract="In this paper we study the problem of solving hard propositional satisfiability problem (SAT) instances in a computing grid or cloud, where run times and communication between parallel running computations are limited.We study analytically an approach where the instance is partitioned iteratively into a tree of subproblems and each node in the tree is solved in parallel.We present new methods for constructing partitions which combine clause learning and lookahead. The methods are incorporated into the iterative approach and its performance is demonstrated with an extensive comparison against the best sequential solvers in the SAT competition 2009 as well as against two efficient parallel solvers.",
isbn="978-3-642-16242-8"
}

@article{FROLEYKS2021103572,
title = {{SAT Competition 2020}},
journal = {Artificial Intelligence},
volume = {301},
pages = {103572},
year = {2021},
issn = {0004-3702},
doi = {https://doi.org/10.1016/j.artint.2021.103572},
url = {https://www.sciencedirect.com/science/article/pii/S0004370221001235},
author = {Nils Froleyks and Marijn Heule and Markus Iser and Matti Järvisalo and Martin Suda},
keywords = {SAT, Boolean satisfiability, SAT Competition, SAT solvers, Empirical evaluation, Benchmarking},
abstract = {The SAT Competitions constitute a well-established series of yearly open international algorithm implementation competitions, focusing on the Boolean satisfiability (or propositional satisfiability, SAT) problem. In this article, we provide a detailed account on the 2020 instantiation of the SAT Competition, including the new competition tracks and benchmark selection procedures, overview of solving strategies implemented in top-performing solvers, and a detailed analysis of the empirical data obtained from running the competition.}
}

@article{ZHANG1996543,
title = {{PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems}},
journal = {Journal of Symbolic Computation},
volume = {21},
number = {4},
pages = {543-560},
year = {1996},
issn = {0747-7171},
doi = {https://doi.org/10.1006/jsco.1996.0030},
url = {https://www.sciencedirect.com/science/article/pii/S0747717196900309},
author = {HANTAO ZHANG and MARIA PAOLA BONACINA and JIEH HSIANG},
abstract = {We present a distributed/parallel prover for propositional satisfiability (SAT), called PSATO, for networks of workstations. PSATO is based on the sequential SAT prover SATO, which is an efficient implementation of the Davis –Putnam algorithm. The master–slave model is used for communication. A simple and effective workload balancing method distributes the workload among workstations. A key property of our method is that the concurrent processes explore disjoint portions of the search space. In this way, we use parallelism without introducing redundant search. Our approach provides solutions to the problems of (i) cumulating intermediate results of separate runs of reasoning programs; (ii) designing highly scalable parallel algorithms and (iii) supporting “fault-tolerant” distributed computing. Several dozens of open problems in the study of quasigroups have been solved using PSATO. We also show how a useful technique called the cyclic group construction has been coded in propositional logic.}
}

@article{arbelaez2009online,
  title={{Online heuristic selection in constraint programming}},
  author={Arbelaez, Alejandro and Hamadi, Youssef and Sebag, Michele},
  year={2009}
}

@phdthesis{lindauer2014algorithm,
  title={{Algorithm selection, scheduling and configuration of Boolean constraint solvers}},
  author={Lindauer, T Marius},
  year={2014},
  school={Universit{\"a}t Potsdam}
}

@incollection{kashgarani2023automatic,
  title={{Automatic Parallel Portfolio Selection}},
  author={Kashgarani, Haniye and Kotthoff, Lars},
  booktitle={ECAI 2023},
  pages={1215--1222},
  year={2023},
  publisher={IOS Press}
}

@inproceedings{Marius2015,
  title={{From sequential algorithm selection to parallel portfolio selection}},
  author={Lindauer, Marius and Hoos, Holger and Hutter, Frank},
  booktitle={International Conference on Learning and Intelligent Optimization},
  pages={1--16},
  year={2015},
  organization={Springer}
}

@article{Hamadi2009,
author = {Hamadi, Youssef and Jabbour, Said and Sais, Lakhdar},
doi = {10.3233/sat190070},
issn = {1574-0617},
journal = {Journal on Satisfiability, Boolean Modeling and Computation},
title = {{ManySAT: a Parallel SAT Solver}},
year = {2009}
}

@article{LINDAUER2017272,
title = {Automatic construction of parallel portfolios via algorithm configuration},
journal = {Artificial Intelligence},
volume = {244},
pages = {272-290},
year = {2017},
issn = {0004-3702},
doi = {https://doi.org/10.1016/j.artint.2016.05.004},
url = {https://www.sciencedirect.com/science/article/pii/S0004370216300625},
author = {Marius Lindauer and Holger Hoos and Kevin Leyton-Brown and Torsten Schaub},
keywords = {Algorithm configuration, Parallel SAT solving, Algorithm portfolios, Programming by optimization, Automated parallelization},
}

@inproceedings{guo_learning-based_2005,
	address = {Berlin, Heidelberg},
	title = {A {Learning}-{Based} {Algorithm} {Selection} {Meta}-{Reasoner} for the {Real}-{Time} {MPE} {Problem}},
	isbn = {978-3-540-30549-1},
	doi = {10.1007/978-3-540-30549-1_28},
	abstract = {The algorithm selection problem aims to select the best algorithm for an input problem instance according to some characteristics of the instance. This paper presents a learning-based inductive approach to build a predictive algorithm selection system from empirical algorithm performance data of the Most Probable Explanation(MPE) problem. The learned model can serve as an algorithm selection meta-reasoner for the real-time MPE problem. Experimental results show that the learned algorithm selection models can help integrate multiple MPE algorithms to gain a better overall performance of reasoning.},
	language = {en},
	booktitle = {{AI} 2004: {Advances} in {Artificial} {Intelligence}},
	publisher = {Springer},
	author = {Guo, Haipeng and Hsu, William H.},
	editor = {Webb, Geoffrey I. and Yu, Xinghuo},
	year = {2005},
	keywords = {Algorithm Selection, Approximate Algorithm, Bayesian Network, Good Algorithm, Tabu Search},
	pages = {307--318},
	file = {Full Text PDF:/home/hkashgar/Zotero/storage/E373SYMH/Guo and Hsu - 2005 - A Learning-Based Algorithm Selection Meta-Reasoner for the Real-Time MPE Problem.pdf:application/pdf},
}
@inproceedings{10.5555/1630659.1630927,
author = {Leyton-Brown, Kevin and Nudelman, Eugene and Andrew, Galen and McFadden, Jim and Shoham, Yoav},
title = {{A portfolio approach to algorithm selection}},
year = {2003},
publisher = {Morgan Kaufmann Publishers Inc.},
address = {San Francisco, CA, USA},
booktitle = {Proceedings of the 18th International Joint Conference on Artificial Intelligence},
pages = {1542–1543},
numpages = {2},
location = {Acapulco, Mexico},
series = {IJCAI'03}
}

@InProceedings{10.1007/978-3-319-09584-4_4,
author="Hutter, Frank
and L{\'o}pez-Ib{\'a}{\~{n}}ez, Manuel
and Fawcett, Chris
and Lindauer, Marius
and Hoos, Holger H.
and Leyton-Brown, Kevin
and St{\"u}tzle, Thomas",
editor="Pardalos, Panos M.
and Resende, Mauricio G.C.
and Vogiatzis, Chrysafis
and Walteros, Jose L.",
title="{AClib: A Benchmark Library for Algorithm Configuration}",
booktitle="Learning and Intelligent Optimization",
year="2014",
publisher="Springer International Publishing",
address="Cham",
pages="36--40",
abstract="Modern solvers for hard computational problems often expose parameters that permit customization for high performance on specific instance types. Since it is tedious and time-consuming to manually optimize such highly parameterized algorithms, recent work in the AI literature has developed automated approaches for this algorithm configuration problem [1, 3, 10, 11, 13, 16].",
isbn="978-3-319-09584-4"
}


@article{Rice1976,
abstract = {The problem of selecting an effective algorithm arises in a wide variety of situations. This chapter starts with a discussion on abstract models: the basic model and associated problems, the model with selection based on features, and the model with variable performance criteria. One objective of this chapter is to explore the applicability of the approximation theory to the algorithm selection problem. There is an intimate relationship here and that the approximation theory forms an appropriate base upon which to develop a theory of algorithm selection methods. The approximation theory currently lacks much of the necessary machinery for the algorithm selection problem. There is a need to develop new results and apply known techniques to these new circumstances. The final pages of this chapter form a sort of appendix, which lists 15 specific open problems and questions in this area. There is a close relationship between the algorithm selection problem and the general optimization theory. This is not surprising since the approximation problem is a special form of the optimization problem. Most realistic algorithm selection problems are of moderate to high dimensionality and thus one should expect them to be quite complex. One consequence of this is that most straightforward approaches (even well-conceived ones) are likely to lead to enormous computations for the best selection. The single most important part of the solution of a selection problem is the appropriate choice of the form for selection mapping. It is here that theories give the least guidance and that the art of problem solving is most crucial. {\textcopyright} 1976 Academic Press Inc.},
author = {Rice, John R.},
doi = {10.1016/S0065-2458(08)60520-3},
issn = {00652458},
journal = {Advances in Computers},
title = {{The Algorithm Selection Problem}},
year = {1976}
}
@article{3s,
abstract = {Algorithm portfolios aim to increase the robustness of our ability to solve problems efficiently. While recently proposed algorithm selection methods come ever closer to identifying the most appropriate solver given an input instance, they are bound to make wrong and, at times, costly decisions. Solver scheduling has been proposed to boost the performance of algorithm selection. Scheduling tries to allocate time slots to the given solvers in a portfolio so as to maximize, say, the number of solved instances within a given time limit. We show how to solve the corresponding optimization problem at a low computational cost using column generation, resulting in fast and high quality solutions. We integrate this approach with a recently introduced algorithm selector, which we also extend using other techniques. We propose various static as well as dynamic scheduling strategies, and demonstrate that in comparison to pure algorithm selection, our novel combination of scheduling and solver selection can significantly boost performance. {\textcopyright} 2011 Springer-Verlag.},
author = {Kadioglu, Serdar and Malitsky, Yuri and Sabharwal, Ashish and Samulowitz, Horst and Sellmann, Meinolf},
doi = {10.1007/978-3-642-23786-7_35},
isbn = {9783642237850},
issn = {03029743},
journal = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
pages = {454--469},
title = {{Algorithm selection and scheduling}},
volume = {6876 LNCS},
year = {2011}
}

@article{wotzlawpfoliouzk,
  title={{pfolioUZK: Solver description}},
  author={Wotzlaw, Andreas and van der Grinten, Alexander and Speckenmeyer, Ewald and Porschen, Stefan},
  journal={Balint et al.(Balint et al., 2012a)},
  pages={45},
  year={2012}
}


@article{roussel2012,
  title={Description of ppfolio (2011)},
  author={Roussel, Olivier},
  journal={Proc. SAT Challenge},
  pages={46},
  year={2012}
}

@article{gagliolo2006dynamic,
  title={{Dynamic algorithm portfolios}},
  author={Gagliolo, Matteo and Schmidhuber, J{\"u}rgen},
  journal={Annals of Mathematics and Artificial Intelligence},
  volume={47},
  pages={3--4},
  year={2006}
}

@article{petrik2006learning,
  title={{Learning parallel portfolios of algorithms}},
  author={Petrik, Marek and Zilberstein, Shlomo},
  journal={Annals of Mathematics and Artificial Intelligence},
  volume={48},
  number={1-2},
  pages={85--106},
  year={2006},
  publisher={Springer}
}

@inproceedings{10.5555/1661445.1661516,
author = {Bordeaux, Lucas and Hamadi, Youssef and Samulowitz, Horst},
title = {{Experiments with Massively Parallel Constraint Solving}},
year = {2009},
publisher = {Morgan Kaufmann Publishers Inc.},
address = {San Francisco, CA, USA},
abstract = {The computing industry is currently facing a major architectural shift. Extra computing power is not coming anymore from higher processor frequencies, but from a growing number of computing cores and processors. For AI, and constraint solving in particular, this raises the question of how to scale current solving techniques to massively parallel architectures.While prior work focusses mostly on small scale parallel constraint solving, we conduct the first study on scalability of constraint solving on 100 processors and beyond in this paper. We propose techniques that are simple to apply and show empirically that they scale surprisingly well. These techniques establish a performance baseline for parallel constraint solving technologies against which more sophisticated parallel algorithms need to compete in the future.},
booktitle = {Proceedings of the 21st International Jont Conference on Artifical Intelligence},
pages = {443–448},
numpages = {6},
location = {Pasadena, California, USA},
series = {IJCAI'09}
}

@article{taitler-et-al-aimag2024,
  author       = {Ayal Taitler and Ron Alford and Joan Espasa and Gregor Behnke and Daniel
    Fi{\v{s}}er and Michael Gimelfarb and Florian Pommerening and Scott Sanner and Enrico
    Scala and Dominik Schreiber and Javier Segovia-Aguas and Jendrik Seipp},
  title        = {The 2023 {International Planning Competition}},
  journal      = {AI Magazine},
  year         = 2024,
  pages        = {1--17},
}

@article{GEBSER_2019,
   title={{The Seventh Answer Set Programming Competition: Design and Results}},
   volume={20},
   ISSN={1475-3081},
   url={http://dx.doi.org/10.1017/S1471068419000061},
   DOI={10.1017/s1471068419000061},
   number={2},
   journal={Theory and Practice of Logic Programming},
   publisher={Cambridge University Press (CUP)},
   author={GEBSER, MARTIN and MARATEA, MARCO and RICCA, FRANCESCO},
   year={2019},
   month=may, pages={176–204} }

@article{tornede2023algorithm,
  title={{Algorithm selection on a meta level}},
  author={Tornede, Alexander and Gehring, Lukas and Tornede, Tanja and Wever, Marcel and H{\"u}llermeier, Eyke},
  journal={Machine Learning},
  volume={112},
  number={4},
  pages={1253--1286},
  year={2023},
  publisher={Springer}
}

@article{Stuckey_Feydy_Schutt_Tack_Fischer_2014, title={{The MiniZinc Challenge 2008–2013}}, volume={35}, url={https://ojs.aaai.org/aimagazine/index.php/aimagazine/article/view/2539}, DOI={10.1609/aimag.v35i2.2539}, abstractNote={MiniZinc is a solver agnostic modeling language for defining and solver combinatorial satisfaction and optimization problems. MiniZinc provides a solver independent modeling language which is now supported by constraint programming solvers, mixed integer programming solvers, SAT and SAT modulo theory solvers, and hybrid solvers. Since 2008 we have run the MiniZinc challenge every year, which compares and contrasts the different strengths of different solvers and solving technologies on a set of MiniZinc models. Here we report on what we have learnt from running the competition for 6 years.}, number={2}, journal={AI Magazine}, author={Stuckey, Peter J. and Feydy, Thibaut and Schutt, Andreas and Tack, Guido and Fischer, Julien}, year={2014}, month={Jun.}, pages={55-60} }

@article{Heule2019,
author = {Heule, Marijn J. H. and J{\"{a}}rvisalo, Matti and Suda, Martin},
doi = {10.3233/sat190120},
issn = {1574-0617},
journal = {Journal on Satisfiability, Boolean Modeling and Computation},
title = {{SAT Competition 2018}},
year = {2019}
}

@article{kadiogluwin,
  title={{How to Win Gold at a SAT Competition Without Writing a SAT Solver}},
  author={Kad{\i}oglu, Serdar and Malitsky, Yuri and Sellmann, Meinolf}, 
  published={}
}

@article{balyo_sat_2017,
	title = {{SAT} {Competition} 2017 {Solver} and {Benchmark} {Descriptions}},
	issn = {1458-4786},
	abstract = {The area of Boolean satisfiability (SAT) solving has seen tremendous progress over the last years. Many problems (e.g., in hardware and software verification) that seemed to be completely out of reach a decade ago can now be handled routinely. Besides new algorithms and better heuristics, refined implementation techniques turned out to be vital for this success. To keep up the driving force in improving SAT solvers, SAT solver competitions provide opportunities for solver developers to present their work to a broader audience and to objectively compare the performance of their own solvers with that of other state-of-the-art solvers. SAT Competition 2014 (SC 2014), an open competitive event for SAT solvers, was orga-nized as a satellite event of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014) and FLoC Olympic Games 2014 within the largest event in the history of logic, Vienna Summer of Logic (VSL) 2014, and the Federated Logic Con-ference (FLoC 2014) in Vienna, Austria. SC 2014 stands in the tradition of the previously organized main competitive events for SAT solvers: the SAT Competitions held 2002-2005 and biannually during 2007-2013, the SAT-Races held in 2006, 2008 and 2010, and SAT Challenge 2012. SC 2014 consisted of a total of 13 competition tracks, each track being characterized by the combination of},
	journal = {Proceedings of SAT COMPETITION 2017},
	author = {Balyo, Tomáš and Heule, Marijn J H and Järvisalo, Matti},
	year = {2017},
	note = {ISBN: 9789515100436},
	pages = {14--15},
	file = {PDF:/home/haniye/Zotero/storage/2UYBVYQH/m-api-405e5882-2f53-6b07-3720-e2754c3255d4.pdf:application/pdf},
}

@article{Malitsky2012,
abstract = {Combining differing solution approaches by means of solver portfolios has proven as a highly effective technique for boosting solver performance. We consider the problem of generating parallel SAT solver portfolios. Our approach is based on a recently introduced sequential SAT solver portfolio that excelled at the last SAT competition. We show how the approach can be generalized for the parallel case, and how obstacles like parallel SAT solvers and symmetries induced by identical processors can be overcome. We compare different ways of computing parallel solver portfolios with the best performing parallel SAT approaches to date. Extensive experimental results show that the developed methodology very significantly improves our current parallel SAT solving capabilities. {\textcopyright} 2012 Springer-Verlag.},
author = {Malitsky, Yuri and Sabharwal, Ashish and Samulowitz, Horst and Sellmann, Meinolf},
doi = {10.1007/978-3-642-33558-7_38},
isbn = {9783642335570},
issn = {03029743},
journal = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
pages = {512--526},
title = {{Parallel SAT solver selection and scheduling}},
volume = {7514 LNCS},
year = {2012}
}