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

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

URL: http://arxiv.org/abs/2101.00589v1
Date: Sun, 3 Jan 2021 09:04:31 GMT
Title: diff-SAT -- A Software for Sampling and Probabilistic Reasoning for SAT and Answer Set Programming
Authors: Matthias Nickles
Abstract summary: diff-SAT combines regular solving with the capability to use probabilistic clauses, facts and rules. The sampling process minimizes a user-defined differentiable objective function.
Score: 0.0
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
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 ($\partial\mathrm{SAT}$) respectively Differentiable Answer Set Programming ($\partial\mathrm{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).

Related papers

Resource-Constrained Heuristic for Max-SAT [0.848762374187855]
We propose a resource-constrained for instances of Max-SAT that iteratively decomposes a larger problem into smaller subcomponents. We analyze a set of variable selection methods, including a novel graph-based method that exploits the structure of a given SAT instance. We demonstrate our results on a set of randomly generated Max-SAT instances as well as real world examples from the Max-SAT evaluation benchmarks.
arXiv Detail & Related papers (2024-10-11T18:20:08Z)
Probabilistic Answer Set Programming with Discrete and Continuous Random Variables [0.18416014644193066]
Probabilistic Answer Set Programming (PASP) extends Answer Set Programming with probabilistic facts that represent uncertain information. We propose Hybrid Probabilistic Answer Set Programming (HPASP) We discuss, implement, and assess the performance of two exact algorithms based on projected answer set enumeration and knowledge compilation.
arXiv Detail & Related papers (2024-09-30T13:24:42Z)
Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
We introduce the notion of decomposition hardness (d-hardness) We show that the d-hardness expresses an estimate of the hardness of $C$ w.r.t.
arXiv Detail & Related papers (2023-12-16T12:44:36Z)
$\omega$PAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs [64.25762042361839]
$omega$PAP spaces are spaces for reasoning denotationally about expressive differentiable and probabilistic programming languages. Our semantics is general enough to assign meanings to most practical probabilistic and differentiable programs. We establish the almost-everywhere differentiability of probabilistic programs' trace density functions.
arXiv Detail & Related papers (2023-02-21T12:50:05Z)
Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
We show that the hardness of SAT encodings for LEC instances can be estimated textitw.r.t some SAT partitioning. The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy.
arXiv Detail & Related papers (2022-10-04T09:19:13Z)
Multi-block-Single-probe Variance Reduced Estimator for Coupled Compositional Optimization [49.58290066287418]
We propose a novel method named Multi-block-probe Variance Reduced (MSVR) to alleviate the complexity of compositional problems. Our results improve upon prior ones in several aspects, including the order of sample complexities and dependence on strongity.
arXiv Detail & Related papers (2022-07-18T12:03:26Z)
Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
arXiv Detail & Related papers (2021-07-15T04:47:35Z)
Transforming Probabilistic Programs for Model Checking [0.0]
We apply static analysis to probabilistic programs to automate large parts of two crucial model checking methods. Our method transforms a probabilistic program specifying a density function into an efficient forward-sampling form. We present an implementation targeting the popular Stan probabilistic programming language.
arXiv Detail & Related papers (2020-08-21T21:06:34Z)
Tractable Inference in Credal Sentential Decision Diagrams [116.6516175350871]
Probabilistic sentential decision diagrams are logic circuits where the inputs of disjunctive gates are annotated by probability values. We develop the credal sentential decision diagrams, a generalisation of their probabilistic counterpart that allows for replacing the local probabilities with credal sets of mass functions. For a first empirical validation, we consider a simple application based on noisy seven-segment display images.
arXiv Detail & Related papers (2020-08-19T16:04:34Z)
Improving probability selecting based weights for Satisfiability Problem [6.59413630027528]
We present a new SLS algorithm named SelectNTS for uniform random k-SAT and HRS. Our algorithm outperforms state-of-the-art random SAT algorithms, and our SelectNTS can effectively solve both uniform random k-SAT and HRS.
arXiv Detail & Related papers (2020-07-30T02:23:07Z)

This list is automatically generated from the titles and abstracts of the papers in this site.