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

Modern solvers for the Boolean Satisfiability Problem (SAT) are powerful, versatile and fast tools for logical inference. SAT solvers underlie a large number of other optimization and reasoning approaches as well as industry applications, for example many constraint programming and Satisfiability Modulo Theories (SMT) solvers, bounded model checking, package managers, hardware and software verification tools, crypto-analysis, and planning and scheduling approaches [13, 8, 9]. Answer Set Programming (ASP) [5] is a form of logic programming (with syntax similar to Prolog and Datalog) which is closely related to SAT solving and oriented primarily towards NP-hard search and combinatorial problems.

Regular SAT and Answer Set solvers do not have the capability to handle or reason about probabilistic knowledge, or to sample multisets of models governed by specific probability distributions. diff-SAT (formerly named delSAT) is an open source SAT and ASP solver which has those capabilities. diff-SAT is programmed in Scala and runs on any contemporary standard Java VM. Its solver core incorporates modern SAT solving techniques such as CDCL (Conflict-Driven Clause Learning)-style solving, Glucose-style restart policy [1], adaptive branching heuristics, rephasing, and parallel portfolio solving in multi-core environments.

Symbolic knowledge can be provided in various formats, including Boolean formulas in CNF and logic programs in Answer Set Programming (ASP) intermediate format (obtained from an ASP grounder). Soft constraints can be provided by attaching probabilities to clauses, facts or rules, or by specifying differentiable objective functions directly as mathematical expressions. In contrast to most existing logic programming approaches, probabilistic databases and approaches based on a reduction to Weighed Model Counting [3], diff-SAT does not require any independence assumptions about probabilistic variables. Compared to Markov Logic Networks [12] (the arguably most popular probabilistic logic), diff-SAT allows for probabilistic logic programming and has thus the ability to deal with inductive definitions and to use probabilities directly as weights despite being able to model complex interdependencies.
diff-SAT’s output is a multiset of models (if the given problem has a solution) corresponding to a probability distribution over possible worlds, allowing for probabilistic inference in the usual way.

On the technical level, diff-SAT achieves its functionality by finding optimal distributions of entire multi-sets of satisfying models (related to the concept of “worldviews” in epistemic logic programming [6]). An incremental sampling process minimizes a user-defined objective function (loss function) over symbol statistics in model multisets using a gradient descent-based branching literal selection approach called Differentiable Satisfiability Solving respectively Differentiable Answer Set Programming [10, 11] ($\partial\mathrm{SAT},\ \partial\mathrm{ASP}$).

Probabilistic annotations of logical items like clauses or rules can be automatically translated into such differentiable functions. Multi-models optimization could be stylized as a form of model optimization where the optimal model is a meta-model which comprises multiple models, but diff-SAT avoids this stylization as it would require clunky techniques like model reification. Remark: Multi-models optimization should not be confused with other optimization types involving multiple models, such as the concurrent discovery of several optimal models.

In contrast to existing approaches to ASP- or SAT-based optimization such as MaxWalkSAT for Weighted MaxSAT solving [7], the differentiable objective function evaluates and optimizes statistics over an entire multiset of models instead of finding an optimal single model which is optimal wrt. the sum of the weights of satisfied soft constraints (soft clauses). Compared to other SAT sampling approaches, in particular [2], diff-SAT samples multiple models using a form of gradient descent until a given minimization threshold of the objective function has been reached. Clauses can be attached probabilities directly instead of non-normalized weights. Note that diff-SAT is not a Stochastic Local Search (SLS) solver but a complete solver (i.e., a solver which returns UNSAT if the input formula is not satisfiable) with probabilistic optimization features.
A more detailed description of diff-SAT’s algorithm and comparison with further related approaches can be found in [11, 10].

Notwithstanding being based on a single, relatively simple technical principle ($\partial\mathrm{SAT}\ /\ \partial\mathrm{ASP}$), diff-SAT goes beyond regular SAT/ASP solving by providing a wide range of additional use cases (besides plain SAT and ASP solving), including probabilistic SAT (PSAT), Probabilistic Answer Set Programming (PrASP), and distribution-dependent model sampling where a family of target distributions can be specified by differentiable objective functions of the form described in the previous section.

• 1.

  Parallel portfolio ASP and SAT solving based on Conflict-Driven Nogood Learning (CDNL), a variant of CDCL)

• 2.

  Runs on the JVM (Java 1.8 or higher)

• 3.

  Model sampling as randomized, gradient-steered search for optimal multisets of models (answer sets respectively Boolean assignments)

• 4.

  Objective functions are arbitrary differentiable functions over atom frequencies in models, allowing for, e.g., probabilistic atoms (clauses, rules) and probabilistic inference, i.e., computation of the probabilities of logical query formulas.

• 5.

  A range of alternative input formats, including for Probabilistic SAT and Probabilistic Answer Set Programming. See below for the complete list of supported formats.

• 6.

  User API for working with probabilistic and non-probabilistic clause and rule sets

• 7.

  Direct support for basic non-ground ASP rules (unrestricted non-ground answer set programs can also be used, but that requires a preceding grounding step using a grounder such as Gringo or Clingo [4], as usual with Answer Set solvers)

Input is accepted in various standard as well as non-standard forms (where no commonly accepted format exists yet, in particular in the area of probabilistic input):

• 1.

  DIMACS CNF (for regular SAT solving)

• 2.

  Probabilistic DIMACS CNF (PCNF) where each clause can optionally be annotated with a probability to turn it into a soft clause

• 3.

  Enhanced DIMACS CNF with a list of parameter atoms and objective function terms appended to the DIMACS part

• 4.

  ASP Intermediate Format (ASPIF), optionally extended with parameter atoms and objective function terms defined using special predicates

• 5.

  Enhanced ASPIF format with a list of parameter atoms and objective function terms appended to the ASPIF part

• 6.

  Probabilistic ASP Intermediate Format (PASPIF) which enhances ASPIF standard format with optional rule probabilities

diff-SAT’s output for satisfiable problems is a multiset of models (possible worlds) where the normalized count of a model represents its probability. The probabilities of individual clauses, facts or rules can be obtained using a simple subsequent filtering and counting step as in most other probabilistic logic programming approaches, but diff-SAT can optionally perform this step itself for user-specified query clauses, facts and rules.