Norbert Manthey, Marijn Heule, Armin Biere,
"Automated Reencoding of Boolean Formulas"
: preliminary Proc. Haifa Verification Conference HVC'12, 11-2012
Original Titel:
Automated Reencoding of Boolean Formulas
Sprache des Titels:
Englisch
Original Buchtitel:
preliminary Proc. Haifa Verification Conference HVC'12
Original Kurzfassung:
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.