Learning a representation for optimizable formulas

Abstract

Roughly speaking, a class of formulas K is called optimizable, if there is a class K′ such that for each formula in K there exists a short equivalent formula in K′, where the deduction problem of K′ is solvable in polynomial time. We consider the problem, whether for such classes an optimized representation can be learned using membership, equivalence and clause queries.