We’ll be reading and discussing papers relating to programming models for working with search procedures and solvers, solver technology, and reactive programming.
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 

Oct 6

Everyone 
Select papers 
Oct 13

Alex S and Calvin 
Nondeterministic Algorithms 
Oct 20

 
No meeting (Affiliates) 
Oct 27

Talia and Julie 
Modular Synthesis of Sketches Using Models 
Nov 3

Dominik and Doug 
Functional Reactive Animation 
Nov 10

Jared, Eric, Chandrakana 
Programming with Enumerable Sets of Structures 
Nov 17

James W and John 
Predicting Learnt Clauses Quality in Modern SAT Solvers 
Nov 24

Chenglong 
Flapjax: A Programming Language for Ajax Applications 
Dec 1

Stuart and Nate 
Curry, a functional logic programming language 
Dec 8

Alex P and James B 
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4 
Nondeterministic Algorithms Robert Floyd, JACM 1967.
Programs to solve combinatorial search problems may often be simply written by using multiplevalued functions. Such programs, although impossible to execute directly on conventional computers, may be converted in a mechanical way into conventional backtracking programs. The process is illustrated with algorithms to find all solutions to the eight queens problem on the chessboard, and to find all simple cycles in a network.
Curry, a functional logic programming language Antoy and Hanus, CACM 2010.
Combining the paradigm features of both logic and functional programming makes for some powerful implementations.
Programming with Enumerable Sets of Structures. Ivan Kuraj, Viktor Kuncak, Daniel Jackson. OOPSLA 2015.
We present SciFe, an efficient, modular, and featurerich framework for automated generation and validation of complex structures, suitable for tasks including automated testing (which explores the space of many structured test inputs) and syntaxguided synthesis (which explores a large number of candidate programs). Our framework is capable of exhaustive, incremental, lazy, and memoized enumeration of structured values from not only finite but also infinite domains, while providing finegrain control over the process.
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
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4. Reynolds et al. CAV 2015 (winner of the SyGuS 2015 competition!)
We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures.
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.
Modular Synthesis of Sketches Using Models. Rohit Singh, Rishabh Singh, Zhilei Xu, Rebecca Krosnick, and Armando SolarLezama. CAV 2013.
One problem with the constraintbased approaches to synthesis that have become popular over the last few years is that they only scale to relatively small routines, on the order of a few dozen lines of code. This paper presents a mechanism for modular reasoning that allows us to break larger synthesis problems into small manageable pieces. The approach builds on previous work in the verification community of using highlevel specifications and partially interpreted functions (we call them models) in place of more complex pieces of code in order to make the analysis modular.
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.
Predicting Learnt Clauses Quality in Modern SAT Solvers Gilles Audemard and Laurent Simon. IJCAI 2009.
Beside impressive progresses made by SAT solvers over the last ten years, only few works tried to understand why Conflict Directed Clause Learning algorithms (CDCL) are so strong and efficient on most industrial applications. We report in this work a key observation of CDCL solvers behavior on this family of benchmarks and explain it by an unsuspected side effect of their particular Clause Learning scheme. This new paradigm allows us to solve an important, still open, question: How to designing a fast, static, accurate, and predictive measure of new learnt clauses pertinence. Our paper is followed by empirical evidences that show how our new learning scheme improves stateofthe art results by an order of magnitude on both SAT and UNSAT industrial problems.
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.
Flapjax: A Programming Language for Ajax Applications. Leo A. Meyerovich, Arjun Guha, Jacob Baskin, Gregory H. Cooper, Michael Greenberg, Aleks Bromfield, Shriram Krishnamurthi. OOPSLA 2009
This paper presents Flapjax, a language designed for contemporary Web applications. These applications communicate with servers and have rich, interactive interfaces. Flapjax provides two key features that simplify writing these applications. First, it provides event streams, a uniform abstraction for communication within a program as well as with external Web services. Second, the language itself is reactive: it automatically tracks data dependencies and propagates updates along those dataflows. This allows developers to write reactive interfaces in a declarative and compositional style.
Functional Reactive Animation. Conal Elliott and Paul Hudak. ICFP 97.
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)