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

TL;DR

This paper introduces a novel method combining symbolic execution, model counting, and entropy maximization to automatically synthesize optimal search steps from problem specifications, with proven convergence and practical effectiveness.

Contribution

It presents a new integrated approach that automates search step synthesis using symbolic analysis, probabilistic modeling, and information theory, validated through a domain-specific language and case studies.

Findings

Effective in solving search problems across multiple domains

Proven convergence to correct solutions

Demonstrated scalability and practical utility

Abstract

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.