On $\exists \forall \exists$ Solving: A Case Study on Automated Synthesis of Magic Card Tricks

Susmit Jha, Vasumathi Raman, and Sanjit A. Seshia. On $\exists \forall \exists$ Solving: A Case Study on Automated Synthesis of Magic Card Tricks. In Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), October 2016.

Download

[pdf] 

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.

BibTeX

@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.},
}