Proof Generation in CDSAT
Logic in Computer Science
2021-07-07 v1 Artificial Intelligence
Authors:
Maria Paola Bonacina
Abstract
The main ideas in the CDSAT (Conflict-Driven Satisfiability) framework for SMT are summarized, leading to approaches to proof generation in CDSAT.
Cite
@article{arxiv.2107.02351,
title = {Proof Generation in CDSAT},
author = {Maria Paola Bonacina},
journal= {arXiv preprint arXiv:2107.02351},
year = {2021}
}
Comments
In Proceedings PxTP 2021, arXiv:2107.01544
Related papers
View all related →
Logic in Computer Science · Computer Science
On the proof complexity of MCSAT
Gereon Kremer, Erika Abraham, Vijay Ganesh
2021-09-06
Logic in Computer Science · Computer Science
DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
Nick Feng, Alan J. Hu, Sam Bayless, Syed M. Iqbal +4
2024-04-19
Logic in Computer Science · Computer Science
A Survey of Satisfiability Modulo Theory
David Monniaux
2016-06-16
Logic in Computer Science · Computer Science
SAT-based Explicit LTLf Satisfiability Checking
Jianwen Li, Kristin Y. Rozier, Geguang Pu, Yueling Zhang +1
2018-11-09
Logic in Computer Science · Computer Science
DRAT-based Bit-Vector Proofs in CVC4
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar +1
2019-07-04
Logic in Computer Science · Computer Science
Resolution Proof Transformation for Compression and Interpolation
S. F. Rollini, R. Bruttomesso, N. Sharygina, A. Tsitovich
2014-04-16
Artificial Intelligence · Computer Science
A Deep Dive into Conflict Generating Decisions
Md Solimul Chowdhury, Martin Müller, Jia You
2021-05-12
Logic in Computer Science · Computer Science
Proof Generation for CDCL Solvers Using Gauss-Jordan Elimination
Mate Soos, Randal E. Bryant
2023-04-11
Logic in Computer Science · Computer Science
On CDCL-based proof systems with the ordered decision strategy
Nathan Mull, Shuo Pang, Alexander Razborov
2019-09-11
Artificial Intelligence · Computer Science
AutoSAT: Automatically Optimize SAT Solvers via Large Language Models
Yiwen Sun, Furong Ye, Xianyin Zhang, Shiyu Huang +3
2024-11-14
Artificial Intelligence · Computer Science
EduSAT: A Pedagogical Tool for Theory and Applications of Boolean Satisfiability
Yiqi Zhao, Ziyan An, Meiyi Ma, Taylor Johnson
2023-08-16
Artificial Intelligence · Computer Science
Explaining SAT Solving Using Causal Reasoning
Jiong Yang, Arijit Shaw, Teodora Baluta, Mate Soos +1
2023-06-13
Software Engineering · Computer Science
Compositional Test Generation of Industrial Synchronous Systems
Daisuke Ishii, Takashi Tomita, Kenji Onishi, Toshiaki Aoki
2021-12-13
Logic in Computer Science · Computer Science
SAT Modulo Monotonic Theories
Sam Bayless, Noah Bayless, Holger H. Hoos, Alan J. Hu
2014-06-03
Logic in Computer Science · Computer Science
Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
2009-06-25
Logic in Computer Science · Computer Science
Solving bitvectors with MCSAT: explanations from bits and pieces (long version)
Stéphane Graham-Lengrand, Dejan Jovanović, Bruno Dutertre
2020-04-20
Logic in Computer Science · Computer Science
Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
Erika Abraham, James H. Davenport, Matthew England, Gereon Kremer
2021-08-12
Logic in Computer Science · Computer Science
Proof-Stitch: Proof Combination for Divide and Conquer SAT Solvers
Abhishek Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir +1
2022-09-13
Symbolic Computation · Computer Science
Improving NLSAT for Nonlinear Real Arithmetic
Zhonghan Wang
2025-09-30
Software Engineering · Computer Science
Practical Constraint Solving for Generating System Test Data
Ghanem Soltana, Mehrdad Sabetzadeh, Lionel C. Briand
2020-05-19
Logic in Computer Science · Computer Science
Certified Branch-and-Bound MaxSAT Solving (Extended Version)
Dieter Vandesande, Jordi Coll, Bart Bogaerts
2025-11-18
Logic in Computer Science · Computer Science
CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)
Christoph Wernhard
2022-07-19
Logic in Computer Science · Computer Science
Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis
Sanjit A. Seshia
2015-03-19
Logic in Computer Science · Computer Science
Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses
Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
2026-05-11
Artificial Intelligence · Computer Science
IntSat: Integer Linear Programming by Conflict-Driven Constraint-Learning
Robert Nieuwenhuis, Albert Oliveras, Enric Rodriguez-Carbonell
2024-02-27