Automated Reencoding of Boolean Formulas

Beschreibung

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.

Zeitraum	06 Nov. 2012
Ereignistitel	8th Intl. Haifa Verification Conference
Veranstaltungstyp	Konferenz
Ort	IsraelAuf Karte anzeigen