Binary Implication Hypergraphs for the Representation and Simplification of Propositional Formulae

Propositional simplification and preprocessing are of key importance in the fields of automated reasoning and theorem proving. We present a novel propositional formula representation able to capture all of its n-ary implication information in a tractable manner. From the exploration of this novel encoding in the form of a directed hypergraph, we derive a novel simplification rule which is guaranteed to be equivalence-preserving, monotonically decreasing in the size of the problem, and capable of deep inference. We are not aware of any such generic preprocessing framework capable of systematically simplifying propositional problems in arbitrary form. Interestingly, our rule effectively generalises and streamlines most of the known equivalence-preserving SAT preprocessing techniques. Additionally, since our problem transformations are domain- and application-independent, they can be used in combination with any propositional-logic-based techniques, including those currently used in automated reasoning, solving and optimisation tools.