  This paper describes learning in a compiler for algorithms solving classes of
the logic minimization problem MINSAT, where the underlying propositional
formula is in conjunctive normal form (CNF) and where costs are associated with
the True/False values of the variables. Each class consists of all instances
that may be derived from a given propositional formula and costs for True/False
values by fixing or deleting variables, and by deleting clauses. The learning
step begins once the compiler has constructed a solution algorithm for a given
class. The step applies that algorithm to comparatively few instances of the
class, analyses the performance of the algorithm on these instances, and
modifies the underlying propositional formula, with the goal that the algorithm
will perform much better on all instances of the class.
