{'fraction_non_alphanumeric': 0.018668326073428748, 'fraction_numerical': 0.0, 'mean_word_length': 5.991304347826087, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
The Power of Auxiliary Variables for Propositional and Quantified Boolean Formulas

Using auxiliary variables to introduce definitions is a popular and powerful technique in knowledge representation which can lead to shorter and more natural encodings without long repetitions. In this paper, we formally define the notion of auxiliary variables and then examine their expressive power and discuss interesting applications. We relate the idea of reusing intermediate results without copying by definitions to similar concepts in other representations of Boolean functions. In particular, we show that propositional logic with definitions has essentially the same expressive power as Boolean circuits with arbitrary fan-out and existentially quantified Boolean formulas in which the bound variables satisfy the Horn property (called ∃HORN(superscript b)). The paper also considers restrictions on the structure of definitions and extensions of propositional definitions. In particular, we examine the relationship between positive propositional definitions and positive definitions with existential quantification or, equivalently, the relationship between ∃HORN(superscript b) formulas and existentially quantified CNF formulas without the Horn restriction on the bound variables (∃CNF(superscript *)). A further extension is to allow arbitrary quantifiers or, equivalently, nesting of Boolean formulas. The expressive power of the bound variables in a quantified CNF formula is shown to be determined by the structure of minimal unsatisfiable or minimal false subformulas of the bound parts of the clauses.