Formal Methods in Computer-Aided Design (FMCAD 20129)
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
Autarkies for SAT are partial assignments for
boolean CNF, which either satisfy a clause or leave it untouched.
We introduce the natural generalisation of autarkies for DQCNF
(dependency-quantified boolean CNF), by generalising constant
boolean functions 0; 1, as used in SAT, to arbitrary boolean
functions assigned to existential variables, as allowed by the
dependency-specification. We regard here DQCNF as a proper
generalisation of QCNF (QBF with CNF), and all results naturally
apply also to QCNF. We provide the most basic theory, considering
confluence of autarky reduction (removing the clauses
satisfied by some autarky), and the Autarky Decomposition
Theorem, the unique decomposition of a DQCNF into the lean
kernel (free from any autarky) and the clauses satisfiable by some
autarky. Finding autarkies is NEXPTIME-hard (or PSPACEhard,
when restricting to QCNF), and so autarky systems are
introduced, which allow for more feasible restricted notions of
autarkies, while maintaining the basic properties. The two most
basic autarky systems restrict either the number of existential
variables assigned, or the number of universal variables used in
the boolean functions assigned.