Tags:CDCL, lower bounds, proof complexity, QBF, resolution and simulations
Abstract:
We continue the investigation on the relations of QCDCL and QBF resolution systems. In particular, we introduce QCDCL versions that tightly characterise QU-Resolution and (a slight variant of) long-distance Q-Resolution. We show that most QCDCL variants -- parameterised by different policies for decisions, unit propagations and reductions -- lead to incomparable systems for almost all choices of these policies.