Programming with Constraints Reading Group
591R
Winter 2016 — Tuesday, 2:30pm — CSE 203
Subscribe to the calendar: iCal or Google Calendar.We’ll be reading and discussing papers relating to programming models for working with search procedures and solvers, solver technology, and reactive programming. In addition, this quarter we will also have some sessions on local work in progress, and other sessions devoted to working with different tools (solvers and languages), in which participants who are using specific tools will give informal talks/demos/code walkthroughs of the application.
Some paper links may point into the ACM Digital Library or the Springer online collection. Using a UW IP address, or the UW libraries offcampus access, should provide access. To receive announcements and news, please subscribe to the 591R mailing list.
Date  Who  What 

Jan 5

Everyone 
Select papers and schedule tool sessions 
Jan 12

Calvin and Talia 
Integrating constraint satisfaction techniques with complex object structures 
Jan 19

Sam and Alex 
Constraints as Control 
Jan 26

Alan 
Wallingford: Toward a Constraint Reactive Programming Language For background see Checks and Balances  Constraint Solving without Surprises in ObjectConstraint Programming Languages 
Feb 2

Pavel 
Cassius 
Feb 9

Eric Butler 
Algebra Synthesis 
Feb 16

Julian 
Answer Set Programming 
Feb 23

Arvind 
Vega 
Mar 1

Julie 
Hints DSL 
Mar 8

 
No meeting (Visit days) 
Suggestions
Programming Models

Constraints as Control. Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter. POPL 2012
We present an extension of Scala that supports constraint programming over bounded and unbounded domains. The resulting language, Kaplan, provides the benefits of constraint programming while preserving the existing features of Scala. Kaplan integrates constraint and imperative programming by using constraints as an advanced control structure; the developers use the monadic ’for’ construct to iterate over the solutions of constraints or branch on the existence of a solution. The constructs we introduce have simple semantics that can be understood as explicit enumeration of values, but are implemented more efficiently using symbolic reasoning.

Integrating constraint satisfaction techniques with complex object structures. François Pachet, Pierre Roy. 15th Annual Conference of the British Computer Society Specialist Group on Expert Systems
Integrating constraint satisfaction techniques with complex object structures is highly desirable. Several libraries are now available to use algorithms offthe shelf and embed them in large objectoriented systems. However, the design of complex object + constraint problems is an open issue that severely limits the applicability of available libraries. We compare two radically different approaches in designing systems integrating objects and finite domain constraints. In the first approach, constraints are defined within classes and constrain attributes of the class, thereby introducing “partially instantiated” objects in the reasoning. In the second approach, constraints are defined outside classes, and constrain fully instantiated objects. We show that, for a particular class of problem, the second solution yields a simpler design while being more efficient. We exemplify our claims by comparing these two approaches on a hard object + constraint problem: fourvoice harmonization of tonal melodies, seen as a representative complex configuration problem
Constraint Solver Technology

Stochastic Local Search for Satisfiability Modulo Theories Frohlich et al. AAAI 2015.
We present a novel stochastic local search (SLS) algorithm to solve SMT problems, especially those in the theory of bitvectors, directly on the theory level. We explain how several successful techniques used in modern SLS solvers for SAT can be lifted to the SMT level. Experimental results show that our approach can compete with stateoftheart bitvector solvers on many practical instances and, sometimes, outperform existing solvers. This offers interesting possibilities in combining our approach with existing techniques, and, moreover, new insights into the importance of exploiting problem structure in SLS solvers for SAT

Impact of Community Structure on SAT Solver Performance. Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard, and Laurent Simon. SAT 2015.
Modern CDCL SAT solvers routinely solve very large industrial SAT instances in relatively short periods of time. It is clear that these solvers somehow exploit the structure of realworld instances. However, todate there have been few results that precisely characterise this structure. In this paper, we provide evidence that the community structure of realworld SAT instances is correlated with the running time of CDCL SAT solvers.

Are There Good Mistakes? A Theoretical Analysis of CEGIS.. Susmit Jha and Sanjit A. Seshia. SYNT 2014.
Counterexampleguided inductive synthesis (CEGIS) is used to synthesize programs from a candidate space of programs. The technique is guaranteed to terminate and synthesize the correct program if the space of candidate programs is finite. But the technique may or may not terminate with the correct program if the candidate space of programs is infinite. In this paper, we perform a theoretical analysis of counterexampleguided inductive synthesis technique. We investigate whether the set of candidate spaces for which the correct program can be synthesized using CEGIS depends on the counterexamples used in inductive synthesis, that is, whether there are good mistakes which would increase the synthesis power. We investigate whether the use of minimal counterexamples instead of arbitrary counterexamples expands the set of candidate spaces of programs for which inductive synthesis can successfully synthesize a correct program. We consider two kinds of counterexamples: minimal counterexamples and history bounded counterexamples. The history bounded counterexample used in any iteration of CEGIS is bounded by the examples used in previous iterations of inductive synthesis. We examine the relative change in power of inductive synthesis in both cases. We show that the synthesis technique using minimal counterexamples MinCEGIS has the same synthesis power as CEGIS but the synthesis technique using history bounded counterexamples HCEGIS has different power than that of CEGIS, but none dominates the other.

The Strategy Challenge in SMT Solving Leonardo de Moura and Grant Olney Passmore. Automated Reasoning and Mathematics, 2013.
Highperformance SMT solvers contain many tightly integrated, handcrafted heuristic combinations of algorithmic proof methods. While these heuristic combinations tend to be highly tuned for known classes of problems, they may easily perform badly on classes of problems not anticipated by solver developers. We present a challenge to the SMT community: to develop methods through which users can exert strategic control over core heuristic aspects of SMT solvers. We present evidence that the adaptation of ideas of strategy prevalent both within the Argonne and LCF theorem proving paradigms can go a long way towards realizing this goal.

Backdoors to Typical Case Complexity. Ryan Williams, Carla P. Gomes, and Bart Selman. IJCAI 2003.
There has been significant recent progress in reasoning and constraint processing methods. In areas such as planning and finite modelchecking, current solution techniques can handle combinatorial problems with up to a million variables and five million constraints. The good scaling behavior of these methods appears to defy what one would expect based on a worstcase complexity analysis. In order to bridge this gap between theory and practice, we propose a new framework for studying the complexity of these techniques on practical problem instances. In particular, our approach incorporates general structural properties observed in practical problem instances into the formal complexity analysis. We introduce a notion of “backdoors”, which are small sets of variables that capture the overall combinatorics of the problem instance. We provide empirical results showing the existence of such backdoors in realworld problems. We then present a series of complexity results that explain the good scaling behavior of current reasoning and constraint methods observed on practical problem instances.

QueryGuided Maximum Satisfiability. Xin Zhang, Ravi Mangal, Aditya V. Nori, and Mayur Naik. POPL 2016.
We propose a new optimization problem “QMAXSAT”, an extension of the wellknown Maximum Satisfiability or MAXSAT problem. In contrast to MAXSAT, which aims to find an assignment to all variables in the formula, QMAXSAT computes an assignment to a desired subset of variables (or queries) in the formula. Indeed, many problems in diverse domains such as program reasoning, information retrieval, and mathematical optimization can be naturally encoded as QMAXSAT instances.
Reactive Programming

Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and PeiHsin Ho.

Practical Principled FRP. Atze van der Ploeg and Koen Claessen. (paper suggestion stolen from the 590P list)

Asynchronous Functional Reactive Programming for GUIs. Evan Czaplicki and Stephen Chong. PLDI 2013.
Tools
Solvers
 Cassowary. Paper: The Cassowary Linear Arithmetic Constraint Solving Algorithm. Greg Badros, Alan Borning, and Peter Stuckey. Cassowary projects website: http://overconstrained.io
Languages
Applications

A Practical FlowSensitive and ContextSensitive C and C++ Memory Leak Detector. David L. Heine and Monica S. Lam. PLDI 2003.

Static Detection of Leaks in Polymorphic Containers. David L. Heine and Monica S. Lam. ICSE 2006.

Software Dataplane Verification. Mihai Dobrescu and Katerina Argyraki. NSDI 2014.

UnderConstrained Symbolic Execution: Correctness Checking for Real Code. David A. Ramos and Dawson Engler. USENIX Security 2015.