Automated Reencoding of Boolean Formulas

We introduce a novel preprocessing technique that automatically reduces the size of a Boolean formula. This technique, called Bounded Variable Addition (BVA), exchanges clauses for variables. Similar to other preprocessing techniques, BVA greedily lowers the sum of variables and clauses, a rough measure for the hardness to solve a formula. We show that cardinality constraints (CCs) can efficiently be reencoded: Given a naive CC encoding, BVA automatically constructs a compact translation, which is smaller than sophisticated encodings for several interesting CCs. Experimental results show that applying BVA on bio-informatics problems, circuit designs and benchmarks from recent satisfiability competitions that also contain other patterns than CCs improves performance.