Tags:fixed parameter tractable, knowledge compilation, model counting, quantification and treewidth
Abstract:
We show how knowledge compilation can be used as a tool for QBF. More precisely, we show that certain one can apply quantification on certain data structures used in knowledge compilation which in combination with the fact that restricted classes of CNF-formulas can be compiled into these data structures can be used to show fixed-parameter tractable results for QBF.
Tractability results for structured quantified CNF-formulas via knowledge compilation