Autumn 2015 — 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.

Some paper links may point into the ACM Digital Library or the Springer online collection. Using a UW IP address, or the UW libraries off-campus 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

Suggestions

Programming Models

• Nondeterministic Algorithms Robert Floyd, JACM 1967.

  Programs to solve combinatorial search problems may often be simply written by using multiple-valued 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 feature-rich 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 syntax-guided 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 fine-grain 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 off-the shelf and embed them in large object-oriented 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: four-voice harmonization of tonal melodies, seen as a representative complex configuration problem

Constraint Solver Technology

• 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 bit-vectors, 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 state-of-the-art bit-vector 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 real-world instances. However, to-date there have been few results that precisely characterise this structure. In this paper, we provide evidence that the community structure of real-world 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.

  Counterexample-guided 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 counterexample-guided 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 Solar-Lezama. CAV 2013.

  One problem with the constraint-based 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 high-level 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.

  High-performance SMT solvers contain many tightly integrated, hand-crafted 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 state-of-the 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 model-checking, 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 worst-case 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 real-world 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.

Reactive Programming

• 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 Pei-Hsin Ho.

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