Towards Clause Learning \`a la Carte through VarMonads

TL;DR

This paper introduces a generic framework for clause learning applicable to various constraint solvers, leveraging Monads to track dependencies and enable conflict analysis, with implementation in Agda.

Contribution

It presents a novel, language-agnostic approach to integrate clause learning into constraint solvers using Monads and dependency tracking.

Findings

Framework works for recursive algebraic data types

Implemented in Agda for clarity

Enables clause learning without full search system

Abstract

More and more languages have a need for constraint solving capabilities for features like error detection or automatic code generation. Imagine a dependently typed language that can immediately implement a program as soon as its type is given. In SAT-solving, there have been several techniques to speed up a search process for satisfying assignments to variables that could be used for program synthesis. One of these techniques is clause learning where, if a search branch runs into a conflict, the cause of the conflict is analysed and used to create a new clause that lets a branch fail earlier if the conflict arises again. We provide a framework with which this technique can come for free not just for Boolean solvers, but for any constraint solver running on recursive algebraic data types. We achieve this by tracking the read operations that happen before a variable is assigned and use this information to create the dependency graph needed for conflict analysis. Our results are implemented in Agda for best readability, but they transfer to other functional languages as well. For brevity, we do not provide an entire search system utilizing the clause learning, but it will become clear from the formalisms that our technique indeed enables a clause learning search system to be built.