View: session overviewtalk overviewside by side with other conferences

11:00 | ABSTRACT. Competitions such as the MiniZinc Challenges or the SAT competitions have been very useful sources for comparing performance of different solving approaches and for advancing the state-of-the-arts of the fields. Traditional competition setting often focuses on producing a ranking between solvers based on their average performance across a wide range of benchmark problems and instances. While this is a sensible way to assess the relative performance of solvers, such ranking does not necessarily reflect the full potential of a solver, especially when we want to utilise a portfolio of solvers instead of a single one for solving a new problem. In this paper, I will describe a portfolio-based analysis method which can give complementary insights into the performance of participating solvers in a competition. The method is demonstrated on the results of the MiniZinc Challenges and new insights gained from the portfolio viewpoint are presented. |

11:25 | Efficiently Explaining CSPs with Unsatisfiable Subset Optimization (extended abstract) PRESENTER: Emilio Gamba ABSTRACT. We build on a recently proposed method for step-wise explaining solutions of constraint satisfaction problems. An explanation here is a sequence of simple inference steps, where the simplicity of an inference step is measured by the number and types of constraints and facts used, and where the sequence explains all logical consequences of the problem. The explanation-generation algorithms presented in that work rely heavily on calls for Minimal Unsatisfiable Subsets (MUS) of a derived unsatisfiable formula, exploiting a one-to-one correspondence between so-called non-redundant explanations and MUSs. The generation of an explanation sequence for a logic grid puzzle ranges from a few minutes to a few hours, which is more than a human would take. Therefore, we build on these formal foundations and tackle the main points of improvement, namely how to efficiently generate explanations that are provably optimal (with respect to the given cost metric). To address this issue, we develop (1) an algorithm based on the hitting set duality for finding optimal constrained unsatisfiable subsets, where `constrainedness' reduces the multiple calls for (optimal) unsatisfiable subsets to a single call; (2) a method for re-using relevant information over multiple calls to these algorithms and; (3) methods exploiting domain-specific information to speed-up explanation sequence generation. We experimentally validate our algorithms on a large number of CSP instances. These experiments show that our algorithms outperform the MUS approach both in terms of quality of the explanation and in time to generate it. We show that this approach can be used to effectively find sequences of optimal explanation steps for a large set of constraint satisfaction problems. |

11:50 | Automatic Generation of Dominance Breaking Nogoods for Constraint Optimization PRESENTER: Allen Z. Zhong ABSTRACT. Dominance relations describe the relations among solutions of Constraint Optimization Problems (COPs), where some solutions are known to be subordinate compared with others concerning satisfiability of constraints and/or optimality of the objective. Dominance breaking is an effective technique to speed up Branch-and-Bound search for optimal solutions by exploiting dominance relations to prune away search space containing only dominated solutions. In this paper, we review recent progress of dominance breaking, and introduce a new line of work on automatic dominance breaking, a framework to automate the identification and exploitation of dominance relations in COPs thereby generating effective dominance breaking nogoods. The major idea is to generate (a) only nogoods as the building blocks to model arbitrary dominance breaking constraints and (b) only the nogoods that are efficiently and conveniently identifiable by constraint satisfaction. We also discuss possible directions of future work. |

Lunches will be held in Taub hall and in The Grand Water Research Institute.