Differentiable Satisfiability and Differentiable Answer Set Programming for Sampling-Based Multi-Model Optimization

TL;DR

This paper introduces Differentiable SAT/ASP, a novel approach for multi-model optimization that uses gradient descent in SAT/ASP solving, enabling scalable probabilistic logic programming and distribution-aware sampling.

Contribution

It presents a new differentiable solving framework, enhances existing algorithms, and provides an open-source implementation with competitive performance for probabilistic logic inference.

Findings

DelSAT performs comparably to Markov Logic Networks in probabilistic inference.

The main algorithm outperforms alternative approaches in efficiency.

Differentiable SAT/ASP enables scalable probabilistic logic programming.

Abstract

We propose Differentiable Satisfiability and Differentiable Answer Set Programming (Differentiable SAT/ASP) for multi-model optimization. Models (answer sets or satisfying truth assignments) are sampled using a novel SAT/ASP solving approach which uses a gradient descent-based branching mechanism. Sampling proceeds until the value of a user-defined multi-model cost function reaches a given threshold. As major use cases for our approach we propose distribution-aware model sampling and expressive yet scalable probabilistic logic programming. As our main algorithmic approach to Differentiable SAT/ASP, we introduce an enhancement of the state-of-the-art CDNL/CDCL algorithm for SAT/ASP solving. Additionally, we present alternative algorithms which use an unmodified ASP solver (Clingo/clasp) and map the optimization task to conventional answer set optimization or use so-called propagators. We also report on the open source software DelSAT, a recent prototype implementation of our main algorithm, and on initial experimental results which indicate that DelSATs performance is, when applied to the use case of probabilistic logic inference, on par with Markov Logic Network (MLN) inference performance, despite having advantageous properties compared to MLNs, such as the ability to express inductive definitions and to work with probabilities as weights directly in all cases. Our experiments also indicate that our main algorithm is strongly superior in terms of performance compared to the presented alternative approaches which reduce a common instance of the general problem to regular SAT/ASP.