Compilation for Critically Constrained Knowledge Bases

We show that many "critically constrained" Random 3SAT knowledge bases (KBs) and other KBs commonly used as benchmarks for propositional knowledge compilation (KC) can be compiled into disjunctive normal form easily by using a variant of the "Davis-Putnam" proof procedure (DP). From these compiled KBs we can answer all queries about entailment of conjunctive normal formulas, also easily --- compared to a "brute-force" approach to approximate KC into unit clauses for the same KBs. We exploit this fact to develop an aggressive hybrid approach which attempts to compile a KB exactly until a given resource limit is reached, then falls back to approximate compilation into unit clauses. The resulting approach, which we call "bootstrapped KC", handles all of the critically constrained Random 3SAT KBs with aggregate savings of an order of magnitude over the brute-force approach. Having developed an effective KC framework, we then explore several promising refinements and optimizations to it an..