Advanced SMT techniques for weighted model integration

DOI10.1016/J.ARTINT.2019.04.003MaRDI QIDQ2321319zbMATH OpenOpenAlexWikidataFDO

Authors Paolo Morettin, Andrea Passerini, Roberto Sebastiani

Publication date 28 August 2019

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.artint.2019.04.003

zbMATH Keywords

probabilistic inferencesatisfiability modulo theoriesweighted model countingweighted model integration

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Reasoning under uncertainty in the context of artificial intelligence (68T37)

Recommendations

• Approximate weighted model integration on DNF structures
• Extending the Smodels system with cardinality and weight constraints
• Light-weight SMT-based model checking
• Weighted models for higher-order computation
• A comparison of SMT-solvers for timed weighted interpreted systems
• Toward a formal theory of model integration

Cites work

• scientific article; zbMATH DE number 2238781 (Why is no real title available?)
• Approximate counting in SMT and value estimation for probabilistic programs
• Compiling probabilistic graphical models using sentential decision diagrams
• Efficient solutions to factored MDPs with imprecise transition probabilities
• How to integrate a polynomial over a simplex
• Importance sampling-based estimation over AND/OR search spaces for graphical models
• Inference and learning in probabilistic logic programs using weighted Boolean formulas
• Inference in hybrid Bayesian networks using mixtures of polynomials
• Lazy satisfiability modulo theories
• On probabilistic inference by weighted model counting
• Probabilistic databases
• Probabilistic planning via heuristic forward search and weighted model counting
• Solving \#SAT and Bayesian inference with backtracking search
• The MathSAT5 SMT solver
• Uniform generation of NP-witnesses using an NP-oracle
• Weighted model counting without parameter variables

Cited in

(9)

• scientific article; zbMATH DE number 7566047 (Why is no real title available?)
• Algebraic model counting
• Entailment vs. verification for partial-assignment satisfiability and enumeration
• A compositional approach to probabilistic knowledge compilation
• On probabilistic inference by weighted model counting
• On enumerating short projected models
• Enhancing SMT-based weighted model integration by structure awareness
• On CNF conversion for SAT and SMT enumeration
• Approximate weighted model integration on DNF structures

Describes a project that uses

Uses Software

• Dsharp
• MathSAT
• LattE

This page was built for publication: Advanced SMT techniques for weighted model integration

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2321319)