Modern heuristic solvers can tackle difficult computational problems, but each solver performs well only on certain tasks. An algorithm portfolio uses empirical knowledge—past experience of each solver's behavior—to run the best solvers on each task.
The borg project includes a practical algorithm portfolio, a web-based visualization tool for solver evaluations, and a research platform for the algorithm portfolio setting.
If you are interested in solving diverse instances of some computationally difficult decision problem, such as SAT or PB, borg may be able to automatically run the right solvers for different instances of your problem.
If you are doing research on algorithm portfolio methods, borg provides standalone tools and data sets that can aid your work, and a possible foundation for implementing your ideas.
The borg project is part of the NNRG in the Artificial Intelligence Laboratory of the University of Texas at Austin. Its primary author is Bryan Silverthorn.
Algorithm portfolio methods like borg leverage solver techniques developed by many other researchers. This project builds especially on the work of authors of satisfiability solvers and other contributors to the SAT research community, which is centered around annual conferences and competitions.
Borg has again placed first in the main category of the annual pseudo-Boolean solver competition, as it did in 2010. The borg-pb-11 description credits the subsolvers essential to the performance of its portfolio approach. Improvements this year include a more accurate model for reasoning about solver performance, a more effective method for scheduling their execution, and the integration of static instance features. Borg also solved the greatest number of instances in the "random" category of the most recent SAT competition, but a bug in certificate handling left it ineligible for a medal.
Our competition submissions are available online. If you are interested in testing or applying borg, however, a more recent version is strongly recommended.
The project has released an experimental web-based tool for visualizing solver performance data, such as those collected by evaluations like the SAT competitions. Visualizations of the phase 2 results for the 2009 competition are available now, and the 2011 results will be visualized soon after they are published. A modern browser is required; Google Chrome is strongly recommended.
The project has made available an initial "alpha" release of data sets and source code, in preparation for distributing a more complete collection of data and documentation. These data sets are intended to benefit the algorithm portfolio research community as a whole: they allow other research groups to avoid the substantial cost of gathering solver behavior data, and they provide a standard environment for portfolio experiments. They represent hundreds of thousands of hours of processor time.
The results of the Fifth Annual Competition of Pseudo-Boolean Solvers were announced at the Thirteenth International Conference on Theory and Applications of Satisfiability Testing in Edinburgh, Scotland, and the PB variant of borg won the core decision/linear-constraint categories. The margin between borg-pb and the second-place solvers (SCIPspx, SAT4J RES CP, and SAT4J RES) was significant, in some cases exceeding the gap between second and eighth.
As always, the portfolio's success would not be possible without the efforts of individual solver authors (borg-pb, for example, includes SAT4J as one of its subsolvers) and the open nature of the satisfiability research community. The borg-pb solver description credits the subsolvers it used.
