Learning in a Compiler for MINSAT Algorithms

Title: Learning in a Compiler for MINSAT Algorithms

Research Question: Can we improve the performance of algorithms for solving classes of logic minimization problems by incorporating a learning process?

Methodology: The researchers developed a compiler that constructs solution algorithms for specific classes of the MINSAT problem. They then implemented a learning process that modifies the underlying propositional formula based on the performance of the algorithm on a few instances of the class. The learning process adds and deletes clauses to the formula, creating what they call "lemmas." These lemmas are either always valid or valid only when the algorithm has already found a solution, and they are used to improve the algorithm's performance.

Results: The learning process reduced the worst-case time for a given class by a factor ranging from 1.5 to 60,319. The total time for the learning process ranged from 1 second to almost 8 hours, with the majority of classes requiring less than 15 minutes. While an 8-hour learning time may seem long, the researchers argue that it is acceptable if the worst-case solution times are below a critical bound that cannot be satisfied by other means.

Implications: The researchers' work suggests that incorporating a learning process into algorithms for solving logic minimization problems can significantly improve their performance. This could have practical implications for fields such as expert systems, natural language processing, and medical diagnosis, where such problems are commonly encountered. However, further research is needed to fully understand the potential benefits and limitations of this approach.

Link to Article: https://arxiv.org/abs/0312032v1 Authors: arXiv ID: 0312032v1