Symbolic Execution + Model Counting + Entropy Maximization = Automatic Search Synthesis

Mara Downing
(Harvey Mudd College)
Abtin Molavi
(Harvey Mudd College)
Lucas Bang
(Harvey Mudd College)

We present a method of automatically synthesizing steps to solve search problems. Given a specification of a search problem, our approach uses symbolic execution to analyze the specification in order to extract a set of constraints which model the problem. These constraints are used in a process called model counting, which is leveraged to compute probability distributions relating search steps to predicates about an unknown target. The probability distribution functions determine an information gain objective function based on Shannon entropy, which, when maximized, yields the next optimal step of the search. We prove that our algorithm converges to a correct solution, and discuss computational complexity issues. We implemented a domain specific language in which to write search problem specifications, enabling our static analysis phase. Our experiments demonstrate the effectiveness of our approach on a set of search problem case studies inspired by the domains of software security, computational geometry, AI for games, and user preference ranking.

In Jean-Francois Raskin and Davide Bresolin: Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2020), Brussels, Belgium, September 21-22, 2020, Electronic Proceedings in Theoretical Computer Science 326, pp. 50–65.
Published: 20th September 2020.

ArXived at: https://dx.doi.org/10.4204/EPTCS.326.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org