Automated Reencoding of Boolean Formulas

Description

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.

Period	06 Nov 2012
Event title	8th Intl. Haifa Verification Conference
Event type	Conference
Location	IsraelShow on map