Summary

		p-simulation		unit
	rep. eff.	hierarchy	inference	propagation	learning
SAT	1	EEE	resolution	watched literals	relevance
cardinality	exp	P?E	not unique	watched literals	relevance
PB	exp	P?E	unique	watched literals	+ strengthening
symmetry	1	EEE$^*$	not in P	same as SAT	same as SAT
QPROP	exp	???	in P using reasons	exp improvement	+ first-order

As usual, there are a few points to be made.

• There is an important difference in practice between the exponential savings in representation provided by QPROP and the savings provided by pseudo-Boolean or cardinality encodings. While the exponential savings in previous cases were mathematical possibilities that were of uncertain use in practice, the savings provided by QPROP can be expected to be achieved in any axiomatization that is constructed by grounding out a relative handful of universally quantified physical laws.
• It is not clear whether QPROP leads to polynomially sized solutions to the pigeonhole and clique coloring problems. It appears at first blush that it should, since quantification over pigeons or holes is the QPROP analog of the identification of the corresponding symmetry as in the previous section. We know of no detailed proof in the literature, however, and our attempts to construct one have been unsuccessful. Similar remarks apply to parity problems.
• Inference in QPROP requires the introduction of a (linear complexity) unification step, and is only uniquely defined if reasons are maintained for the choices made in the search.
• The exponential savings claimed for unit propagation are obviously an average case result, as opposed to a worst case one. They are a consequence of the fact that it is possible to use subsearch as part of unit propagation, as opposed to the ``generate and test'' mechanism used by ground methods.
• In addition to the usual idea of relevance-based learning, quantified methods can extend the power of individual nogoods by resolving quantified clauses instead of their ground instances.

Finally, we remark that a representation very similar to QPROP has also been used in Answer Set Programming (ASP) [Marek TruszczynskiMarek Truszczynski1999,NiemeläNiemelä1999] under the name ``propositional schemata'' [East TruszczynskiEast Truszczynski2001,East TruszczynskiEast Truszczynski2002]. The approach used in ASP resembles existing satisfiability work, however, in that clauses are always grounded out. The potential advantages of intelligent subsearch are thus not exploited, although we expect that many of the motivations and results given here would also apply in ASP. In fact, ASP has many features in common with SAT:

• In the most commonly used semantics, that of (non-disjunctive) stable model logic programming [Gelfond LifschitzGelfond Lifschitz1988], the representational power is precisely that of NP (or $NP^{NP}$ for disjunctive programming).
• Cardinality constraints are allowed [East TruszczynskiEast Truszczynski2002,SimonsSimons2000].
• Solution methods [Leone, Pfeifer, et al.Leone et al.2002,NiemeläNiemelä1999,SimonsSimons2000] use DPLL and some form of propagation.

The most significant difference between conventional satisfiability work and ASP with stable model semantics is that the relevant logic is not classical but the ``logic of here and there'' [PearcePearce1997]. In the logic of here and there, the law of the excluded middle does not hold, only the weaker $\neg p \vee \neg \neg p$. This is sufficient for DPLL to be applied, but does imply that classical resolution is no longer valid. As a result, there seems to be no proof theory for the resulting system, and learning within this framework is not yet understood. Backjumping is used, but the mechanism does not seem to learn new rules from failed subtrees in the search. In an analogous way, cardinality constraints are used but cutting plane proof systems are not. Despite the many parallels between SAT and ASP, including the approach in this survey seems to be somewhat premature.