diff-SAT -- A Software for Sampling and Probabilistic Reasoning for SAT and Answer Set Programming

Code

• github.com/MatthiasNickles/diff-SAT
  OfficialIn papernone★ 70

Abstract

This paper describes diff-SAT, an Answer Set and SAT solver which combines regular solving with the capability to use probabilistic clauses, facts and rules, and to sample an optimal world-view (multiset of satisfying Boolean variable assignments or answer sets) subject to user-provided probabilistic constraints. The sampling process minimizes a user-defined differentiable objective function using a gradient descent based optimization method called Differentiable Satisfiability Solving (SAT) respectively Differentiable Answer Set Programming (ASP). Use cases are i.a. probabilistic logic programming (in form of Probabilistic Answer Set Programming), Probabilistic Boolean Satisfiability solving (PSAT), and distribution-aware sampling of model multisets (answer sets or Boolean interpretations).

Reproductions