Learning in a Compiler for MINSAT Algorithms

TL;DR

This paper introduces a learning-enhanced compiler for MINSAT algorithms that adapts to specific problem classes by analyzing initial instances and modifying the underlying formulas to improve overall algorithm performance.

Contribution

It presents a novel learning approach within a compiler for MINSAT algorithms, enabling tailored optimization for classes of related problems.

Findings

Improved algorithm performance on targeted MINSAT classes

Effective modification of propositional formulas based on initial instance analysis

Enhanced efficiency in solving classes of logic minimization problems

Abstract

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.