Cover Image

Understanding CDCL Solvers via Scalability Studies and Proofdoors

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Zhang, Shimin, Xia, Yechuan, Li, Chunxiao, Li, Jianwen, Vardi, Moshe Y., Ganesh, Vijay
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Proofdoors and Efficiency of CDCL Solvers
by: Singh, Sunidhi, et al.
Published: (2026)

Extending CDCL-based Model Enumeration with Weights
by: Spallitta, Giuseppe, et al.
Published: (2026)

A Reinforcement Learning based Reset Policy for CDCL SAT Solvers
by: Li, Chunxiao, et al.
Published: (2024)

Rethinking Clause Management for CDCL SAT Solvers
by: Cai, Yalun, et al.
Published: (2026)

Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
by: Beyersdorff, Olaf, et al.
Published: (2021)

Automata Linear Dynamic Logic on Finite Traces
by: Smith, Kevin W., et al.
Published: (2021)

Verifying Equilibria in Finite-Horizon Probabilistic Concurrent Game Systems
by: Rajasekaran, Senthil, et al.
Published: (2025)

Computing Short SAT Implicants via Ising/QUBO Encodings
by: Spallitta, Giuseppe, et al.
Published: (2026)

On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts
by: Xiao, Shengping, et al.
Published: (2024)

Revisiting Restarts of CDCL: Should the Search Information be Preserved?
by: Zhang, Xindi, et al.
Published: (2024)

LTLf Synthesis Under Unreliable Input
by: Hagemeier, Christian, et al.
Published: (2024)

Extending CDCL to disjunctions of parity equations
by: Beame, Paul, et al.
Published: (2026)

Dynamic Programming for Symbolic Boolean Realizability and Synthesis
by: Lin, Yi, et al.
Published: (2024)

Dynamic Boolean Synthesis with Zero-suppressed Decision Diagrams
by: Lin, Yi, et al.
Published: (2025)

Extended Resolution Clause Learning via Dual Implication Points
by: Buss, Sam, et al.
Published: (2024)

On-the-fly LTLf Synthesis under Partial Observability
by: Alon, Nadav, et al.
Published: (2026)

Multi-Property Synthesis
by: Weinhuber, Christoph, et al.
Published: (2026)

Probabilistic-bit Guided CDCL for SAT Solving using Ising Consensus Assumptions
by: Bino, Melki
Published: (2026)

LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces
by: Aminof, Benjamin, et al.
Published: (2024)

Verified Certificates via SAT and Computer Algebra Systems for the Ramsey $R(3, 8)$ and $R(3, 9)$ Problems
by: Li, Zhengyu, et al.
Published: (2025)

Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization
by: Zhang, Zhiwei, et al.
Published: (2025)

Fast Obligation Translation and Synthesis
by: Duret-Lutz, Alexandre, et al.
Published: (2026)

Towards SMT Solver Stability via Input Normalization
by: Amrollahi, Daneshvar, et al.
Published: (2024)

Revisiting Assumptions Ordering in CAR-Based Model Checking
by: Dong, Yibo, et al.
Published: (2024)

SAT + NAUTY: Orderly Generation of Small Kochen-Specker Sets Containing the Smallest State-independent Contextuality Set
by: Li, Zhengyu, et al.
Published: (2026)

A proof-theoretic approach to abstract interpretation
by: D'Silva, Vijay, et al.
Published: (2026)

Can Transformers Reason Logically? A Study in SAT Solving
by: Pan, Leyan, et al.
Published: (2024)

An Exponential Separation between Deterministic CDCL and DPLL Solvers
by: Samar, Sahil, et al.
Published: (2026)

OSTRICH2: Solver for Complex String Constraints
by: Hague, Matthew, et al.
Published: (2025)

RLSF: Fine-tuning LLMs via Symbolic Feedback
by: Jha, Piyush, et al.
Published: (2024)

A Compositional Framework for On-the-Fly LTLf Synthesis
by: Li, Yongkang, et al.
Published: (2025)

A Hybrid SMT-NRA Solver: Integrating 2D Cell-Jump-Based Local Search, MCSAT and OpenCAD
by: Ding, Tianyi, et al.
Published: (2025)

Deeply Optimizing the SAT Solver for the IC3 Algorithm
by: Su, Yuheng, et al.
Published: (2025)

MCSat-based Finite Field Reasoning in the Yices2 SMT Solver
by: Hader, Thomas, et al.
Published: (2024)

MathConstraint: Automated Generation of Verified Combinatorial Reasoning Instances for LLMs
by: Pati, Viresh, et al.
Published: (2026)

LLM2SMT: Building an SMT Solver with Zero Human-Written Code
by: Janota, Mikoláš, et al.
Published: (2026)

Dsat: A Native SAT Solver for Discrete Logic
by: Zhang, Yaofang, et al.
Published: (2026)

Theta as a Horn Solver
by: Bajczi, Levente, et al.
Published: (2025)

Yet another cubical type theory, but via a semantic approach
by: Kapulkin, Chris, et al.
Published: (2025)

Some General Completeness Results for Propositionally Quantified Modal Logics
by: Ding, Yifeng, et al.
Published: (2024)