SAT solver, CDCL, Transformer, imitation learning, unit propagation, conflict analysis, neuro-symbolic AI

This contribution describes preliminary experiments aimed at testing whether an autoregressive Transformer can learn to imitate the steps of a symbolic SAT solver based on Conflict-Driven Clause Learning (CDCL). Using a custom solver implementation comprising three key procedures—Solve, Unit Propagation, and Conflict Analysis—we generated training data by recording execution traces from random CNF formulas. The solver assigns Boolean values via depth-first search, employing Unit Propagation to deduce values or detect conflicts, and Conflict Analysis to learn new clauses that restrict the search space upon backtracking. These recorded traces were converted into textual training examples for each procedure invocation, and the model was subsequently trained on traces from a set of training formulas and validated on a distinct set to evaluate its ability to replicate the solver's logic.

This contribution describes preliminary experiments aimed at testing whether an autoregressive Transformer can learn to imitate the steps of a symbolic SAT solver based on Conflict-Driven Clause Learning (CDCL). Using a custom solver implementation comprising three key procedures—Solve, Unit Propagation, and Conflict Analysis—we generated training data by recording execution traces from random CNF formulas. The solver assigns Boolean values via depth-first search, employing Unit Propagation to deduce values or detect conflicts, and Conflict Analysis to learn new clauses that restrict the search space upon backtracking. These recorded traces were converted into textual training examples for each procedure invocation, and the model was subsequently trained on traces from a set of training formulas and validated on a distinct set to evaluate its ability to replicate the solver's logic.