@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@InProceedings{jha-fmcad16,
  Author = {Susmit Jha and Vasumathi Raman and Sanjit A. Seshia},
  Title = {On $\exists \forall \exists$ Solving: A Case Study on Automated Synthesis of Magic Card Tricks},
  booktitle = {Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD)},
  month = "October",
  year = {2016},
  abstract = {In formal synthesis, the goal is to find a composition 
of components from a finite library such that the composition 
satisfies a given logical specification. In this paper, we consider 
the problem of synthesizing magic card tricks from component 
actions, where some of the actions depend on non-deterministic 
choices made by the audience. This problem can be naturally 
represented as a quantified logical formula of the form: Exists 
a composition, Forall nondeterministic choices, Uniquely-Exists 
intermediate and final outputs satisfying a logical specification, 
that is, an Exists-Forall-Exists satisfiability problem.  
We present a novel 
approach to solve this problem that exploits the unique-existence 
of intermediate and final outputs for any given composition and 
choice values. We illustrate how several popular magic card 
tricks can be recovered using this approach. These tricks evolved 
through human ingenuity over decades, but we demonstrate that 
formal synthesis can generate a number of novel variants of these 
tricks within minutes. In contrast, a direct encoding to quantified 
SMT problem fails to find a solution in hours.},
}