Sampling-Based SAT/ASP Multi-Model Optimization as a Framework for Probabilistic Inference (Extended Abstract)

This extended abstract reports an earlier work [8] which introduced multi-model optimization through SAT witness or answer set sampling where the sampling process is controlled by a user-provided differentiable loss function over the multiset of sampled models. Probabilistic reasoning tasks are the primary use cases, including deduction-style probabilistic inference and hypothesis weight learning. Technically, our approach enhances a CDCL-based SAT and ASP solving algorithm to differentiable satisfiability solving (respectively differentiable answer set programming), by using a form of Gradient Descent as branching literal decision approach, and optionally a cost backtracking mechanism. Sampling of models using these methods minimizes a task-specific, user-provided multi-model loss function while adhering to given logical background knowledge (background knowledge being either a Boolean formula in CNF or a logic program under stable model semantics). Features of the framework include its relative simplicity and high degree of expressiveness, since arbitrary differentiable cost functions and background knowledge can be provided.