Gradient-Based Optimization on G\"odel Logic as Discrete Local Search
About
A fundamental challenge in neurosymbolic systems is applying continuous gradient-based optimization to discrete logical domains. While fuzzy relaxations provide differentiability, they often lack a formal structural alignment with classical logic. In this work, we show that G\"odel semantics addresses this limitation through a homomorphism that maps its continuous interpretations to Boolean ones, allowing discrete variables to be encoded while maintaining full differentiability. Building on this foundation, we show that gradient-based optimization on G\"odel logic instantiates a discrete local search for Boolean satisfiability. Our formal analysis proves that each optimization step identifies and modifies a single variable within a unsatisfied clause, precisely mimicking the steps of a discrete solver. We identify local optima as the primary limitation of such dynamics and introduce the G\"odel Trick, a stochastic reparameterization technique designed to improve the exploration of the solution space. We further show a formal connection between this approach, probabilistic inference, and the Gumbel-Max trick. Experimental results on SAT benchmarks and the Visual Sudoku task validate our theoretical findings, demonstrating that our approach effectively navigates complex combinatorial landscapes and provides a solid foundation for differentiable discrete search.
Related benchmarks
| Task | Dataset | Result | Rank | |
|---|---|---|---|---|
| Sudoku Classification | Visual Sudoku 9x9 | Accuracy62.95 | 5 | |
| SAT solving | SATLIB UF | Solved Rate74.5 | 4 | |
| SAT solving | SATLIB RTI BMS | Sample Solved Rate46.2 | 4 | |
| SAT solving | SATLIB CBS | Sample Solved Rate70.3 | 4 | |
| SAT solving | SATLIB FLAT | Solved Rate (%)41.8 | 4 | |
| SAT solving | SATLIB SW | Sample Solved Rate30.2 | 4 | |
| SAT solving | SATLIB PLANNING | Sample Solved Rate9.9 | 4 | |
| SAT solving | SATLIB AIS | Sample Solved Rate29.8 | 4 | |
| SAT solving | SATLIB QG | Sample Solved Rate0.4 | 4 | |
| SAT solving | SATLIB DIMACS | Sample Solved Rate1.4 | 4 |