Satisfiability modulo user propagators

DOI10.1613/JAIR.1.16163MaRDI QIDQ7033965zbMATH OpenFDO

Authors Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere

Publication date 3 February 2025

Published in The Journal of Artificial Intelligence Research (JAIR) (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1613/JAIR.1.16163

zbMATH Keywords

automated reasoningsatisfiabilityuser interfaces

Mathematics Subject Classification ID

Reasoning under uncertainty in the context of artificial intelligence (68T37)

Cites work

• A SAT attack on Rota's basis conjecture
• A SAT solver's opinion on the Erdős-Faber-Lovász conjecture
• Applying computer algebra systems with SAT solvers to the Williamson conjecture
• Backing backtracking
• Breaking symmetries with high dimensional graph invariants and their combination
• Certifying incremental SAT solving
• Chronological backtracking
• Complex Golay pairs up to length 28: a search via computer algebra and programmatic SAT
• Dafny: an automatic program verifier for functional correctness
• Efficient SAT solving under assumptions
• Flexible proof production in an industrial-strength SMT solver
• GRASP: a search algorithm for propositional satisfiability
• Handbook of satisfiability. In 2 parts
• scientific article; zbMATH DE number 1903356 (Why is no real title available?)
• Improving Glucose for incremental SAT solving with assumptions: application to MUS extraction
• Incremental inprocessing in SAT solving
• Incremental preprocessing methods for use in BMC
• Inprocessing rules
• Introducing Intel\(\circledR\) SAT solver
• IPASIR-up: user propagators for CDCL
• MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
• Nonexistence Certificates for Ovals in a Projective Plane of Order Ten
• On searching for small Kochen-Specker vector systems
• Optimal symmetry breaking for graph problems
• Preprocessing in incremental SAT
• RC2: an efficient MaxSAT solver
• Reusing the assignment trail in CDCL solvers
• SAT modulo graphs: acyclicity
• SAT race 2015
• SAT-based generation of panar graphs
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Solving the incremental satisfiability problem
• Speeding up assumption-based SAT
• Stratified abstraction of access control policies
• Temporal induction by incremental SAT solving
• The MathSAT5 SMT solver
• The SAT+CAS method for combinatorial search with applications to best matrices
• Theory and Applications of Satisfiability Testing
• Ultimately incremental SAT

This page was built for publication: Satisfiability modulo user propagators

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