Theory Learning with Symmetry Breaking

Howe, Jacob M. and Robbins, Ed and King, Andy (2017) Theory Learning with Symmetry Breaking. In: Pientka, Brigitte, ed. International Symposium on Principles and Practice of Declarative Programming. ACM, Namur, Belgium, pp. 85-96. ISBN 978-1-4503-5291-8. (doi:https://doi.org/10.1145/3131851.3131861) (Full text available)

Abstract

This paper investigates the use of a Prolog coded SMT solver in tack- ling 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 y, 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 e ect 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: Book section
Divisions: Faculties > Sciences > School of Computing
Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Andy King
Date Deposited: 21 Jul 2017 17:11 UTC
Last Modified: 26 Oct 2017 08:16 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/62377 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year