Autarkies for DQCNF

Description

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.

Period	25 Oct 2019
Event title	Formal Methods in Computer-Aided Design (FMCAD 20129)
Event type	Conference
Location	United StatesShow on map