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.
The paper "Latent Class Models for Algorithm Portfolio Methods", which develops the core solver behavior model applied in borg, was presented at the Twenty-Fourth AAAI Conference on Artificial Intelligence (AAAI-10) in Atlanta, Georgia this past week. The conference featured plenty of excitement around portfolio methods; some interesting and related papers from other research groups are highlighted in our updates feed.
