Skip to main content

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:10.1145/3131851.3131861) (KAR id:62377)

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
DOI/Identification number: 10.1145/3131851.3131861
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Andy King
Date Deposited: 21 Jul 2017 17:11 UTC
Last Modified: 09 Dec 2022 06:53 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/62377 (The current URI for this page, for reference purposes)

University of Kent Author Information

Robbins, Ed.

Creator's ORCID:
CReDIT Contributor Roles:

King, Andy.

Creator's ORCID: https://orcid.org/0000-0001-5806-4822
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.