The Language of Search

TL;DR

This paper establishes a framework linking exhaustive search algorithms on propositional knowledge bases to propositional languages, enabling analysis of their power and limitations through language properties.

Contribution

It introduces a novel perspective that maps search algorithms to propositional languages, facilitating understanding and improvement of knowledge compilation techniques.

Findings

Search traces can be interpreted as combinational circuits.

Exhaustive DPLL search corresponds to known languages like FBDD, OBDD, and d-DNNF.

Framework enables analysis of search algorithms via language tractability and succinctness.

Abstract

This paper is concerned with a class of algorithms that perform exhaustive search on propositional knowledge bases. We show that each of these algorithms defines and generates a propositional language. Specifically, we show that the trace of a search can be interpreted as a combinational circuit, and a search algorithm then defines a propositional language consisting of circuits that are generated across all possible executions of the algorithm. In particular, we show that several versions of exhaustive DPLL search correspond to such well-known languages as FBDD, OBDD, and a precisely-defined subset of d-DNNF. By thus mapping search algorithms to propositional languages, we provide a uniform and practical framework in which successful search techniques can be harnessed for compilation of knowledge into various languages of interest, and a new methodology whereby the power and limitations of search algorithms can be understood by looking up the tractability and succinctness of the corresponding propositional languages.