A Caltech Library Service

Faster Constraint Solving Using Learning Based Abstractions

Dathathri, Sumanth and Arechiga, Nikos and Gao, Sicun (2016) Faster Constraint Solving Using Learning Based Abstractions. In: Southern California Machine Learning Symposium, 18 November 2016, Pasadena, CA. (Unpublished)

[img] PDF - Submitted Version
See Usage Policy.


Use this Persistent URL to link to this item:


This work addresses the problem of scalable constraint solving. Our technique combines traditional constraint-solving approaches with machine learning techniques to propose abstractions that simplify the problem. First, we use a collection of heuristics to learn sets of constraints that may be well abstracted as a single, simpler constraint. Next, we use an asymmetric machine learning procedure to abstract the set of clauses, using satisfying and falsifying instances as training data. Next, we solve a reduced constraint problem to check that the learned formula is indeed a consequent (or antecedent) of the formula we sought to abstract, and finally we use the learned formula to check the original property. Our experiments show that our technique allows improved handling of constraint solving instances that are slow to complete on a conventional solver. Our technique is complementary to existing constraint solving approaches, in the sense that it can be used to improve the scalability of any existing tool.

Item Type:Conference or Workshop Item (Poster)
Contact Email
Subject Keywords:Interpolants, Satisfiability Modulo Theories, Constraint Solving, Machine Learning, Formal Methods
Record Number:CaltechAUTHORS:20161118-140826831
Persistent URL:
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:72174
Deposited By: Sumanth Dathathri
Deposited On:27 Nov 2016 19:44
Last Modified:03 Oct 2019 16:15

Repository Staff Only: item control page