Empirical results on anytime propositional reasoning

An anytime family of propositional reasoners is a sequence |-₀,|-₁,...of inference relations such that each |-_k is sound, tractable, and makes more inferences than |- _k-1, and each theory has a complete reasoner in the family. Anytime families are useful for resource-bounded reasoning in knowledge representation systems. We describe implementations of an anytime family {|-_k} of clausal propositional reasoners using three different strategies. We present empirical results comparing the three strategies, the completeness of reasoning, the time for making inferences, and the space used for reasoning. Our results show that the reasoners with higher values of k infer significantly more formulas than reasoners with lower valves of k, and the time for inferencing decreases significantly as k is increased from 0 to 2