Theory Learning with Symmetry Breaking

Howe, J. M., Robbins,, E & King, A (2017). Theory Learning with Symmetry Breaking. Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, pp. 85-96. doi: 10.1145/3131851.3131861

[img]
Preview
Text - Accepted Version
Download (607kB) | Preview

Abstract

This paper investigates the use of a Prolog coded SMT solver in tackling a well known constraints problem, namely packing a given set of consecutive squares into a given rectangle, and details the developments in the solver that this motivates. The packing problem has a natural model in the theory of quantifier-free integer difference logic, a theory supported by many SMT solvers. The solver used in this work exploits a data structure consisting of an incremental Floyd-Warshall matrix paired with a watch matrix that monitors the entailment status of integer difference constraints. It is shown how this structure can be used to build unsatisfiable theory cores on the fly, which in turn allows theory learning to be incorporated into the solver. Further, it is shown that a problem-specific and non-standard approach to learning can be taken where symmetry breaking is incorporated into the learning stage, magnifying the effect of learning. It is argued that the declarative framework allows the solver to be used in this white box manner and is a strength of the solver. The approach is experimentally evaluated.

Item Type: Article
Additional Information: © Howe, J. et al 2017. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, http://dx.doi.org/10.1145/3131851.3131861.
Uncontrolled Keywords: SAT solving, Constraints
Divisions: School of Informatics > Department of Computing
URI: http://openaccess.city.ac.uk/id/eprint/18378

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year

View more statistics