Jean-Marie Lagniez, Armin Biere,
"Factoring Out Assumptions to Speed Up MUS Extraction"
: Proc. 16th Intl. Conf. on Theory and Applications of Satisfiability Testing, Serie Lecture Notes in Computer Science (LNCS), Vol. 7962, Springer, Seite(n) 276-292, 2013
Original Titel:
Factoring Out Assumptions to Speed Up MUS Extraction
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 16th Intl. Conf. on Theory and Applications of Satisfiability Testing
Original Kurzfassung:
n earlier work on a limited form of extended resolution for
CDCL based SAT solving, new literals were introduced to facto
r out
parts of learned clauses. The main goal was to shorten clause
s, reduce
proof size and memory usage and thus speed up propagation and
conflict
analysis. Even though some reduction was achieved, the effect
iveness of
this technique was rather modest for generic SAT solving. In th
is paper
we show that factoring out literals is particularly useful f
or incremen-
tal SAT solving, based on assumptions. This is the most common
ap-
proach for incremental SAT solving and was pioneered by the au
thors
of MINISAT. Our first contribution is to focus on factoring out
only
assumptions, and actually all eagerly. This enables the use
of compact
dedicated data structures, and naturally suggests a new for
m of clause
minimization, our second contribution. As last main contri
bution, we
propose to use these data structures to maintain a partial pr
oof trace for
learned clauses with assumptions, which gives us a cheap way
to flush
useless learned clauses. In order to evaluate the effectiven
ess of our tech-
niques we implemented them within the version of MINISAT used
in the
publically available state-of-the-art MUS extractor MUSer
. An extensive
experimental evaluation shows that factoring out assumptio
ns in com-
bination with our novel clause minimization procedure and e
ager clause
removal is particularly effective in reducing average claus
e size, improves
running time and in general the state-of-the-art in MUS extra
ction.
Forschungs-