Different solvers for computationally difficult problems such as satisfiability (SAT) have different strengths. "Algorithm portfolios" exploit this phenomenon by employing multiple solvers and appropriately allocating computational resources among them.
This proposal outlines a novel algorithm portfolio architecture constructed around "models of search", probabilistic models of solver behavior fitted to domain-specific data. Two natural latent class mixture models of search are developed and tested, providing evidence that such models can be built, learned, and used effectively. Three directions for future research are then proposed: improved models of search that leverage existing work on probabilistic models of other domains; better action selection methods that extract problem features and plan beyond immediate reward; and new techniques for evaluating solvers and synthesizing new portfolios.