Automatic Generation of Formula Simplifiers based on Conditional Rewrite Rules

TL;DR

This paper presents a method that automatically synthesizes logic formula simplifiers using machine learning and constraint-based techniques, enabling tailored simplification tools for specific problem domains.

Contribution

It introduces a novel approach combining machine learning with constraint-based synthesis to automatically generate domain-specific formula simplifiers.

Findings

Effective synthesis of formula simplifiers for logic problems

Improved performance on SyGuS benchmarks

Potential applications in automated grading systems

Abstract

This paper addresses the problem of creating simplifiers for logic formulas based on conditional term rewriting. In particular, the paper focuses on a program synthesis application where formula simplifications have been shown to have a significant impact. We show that by combining machine learning techniques with constraint-based synthesis, it is possible to synthesize a formula simplifier fully automatically from a corpus of representative problems, making it possible to create formula simplifiers tailored to specific problem domains. We demonstrate the benefits of our approach for synthesis benchmarks from the SyGuS competition and automated grading.