Image de couverture de livre

Rethinking Clause Management for CDCL SAT Solvers

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Cai, Yalun, Zhang, Xindi, Shi, Zhengyuan, Tao, Mengxia, Xu, Qiang
Format:	Preprint
Publié:	2026
Sujets:	Logic in Computer Science
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

Revisiting Restarts of CDCL: Should the Search Information be Preserved?
par: Zhang, Xindi, et autres
Publié: (2024)

A Reinforcement Learning based Reset Policy for CDCL SAT Solvers
par: Li, Chunxiao, et autres
Publié: (2024)

Proofdoors and Efficiency of CDCL Solvers
par: Singh, Sunidhi, et autres
Publié: (2026)

Understanding CDCL Solvers via Scalability Studies and Proofdoors
par: Zhang, Shimin, et autres
Publié: (2026)

Logic Optimization Meets SAT: A Novel Framework for Circuit-SAT Solving
par: Shi, Zhengyuan, et autres
Publié: (2024)

Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
par: Beyersdorff, Olaf, et autres
Publié: (2021)

Probabilistic-bit Guided CDCL for SAT Solving using Ising Consensus Assumptions
par: Bino, Melki
Publié: (2026)

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses
par: Spallitta, Giuseppe, et autres
Publié: (2024)

Extending CDCL-based Model Enumeration with Weights
par: Spallitta, Giuseppe, et autres
Publié: (2026)

Extending CDCL to disjunctions of parity equations
par: Beame, Paul, et autres
Publié: (2026)

Circuit-Aware SAT Solving: Guiding CDCL via Conditional Probabilities
par: Zhu, Jiaying, et autres
Publié: (2025)

Dsat: A Native SAT Solver for Discrete Logic
par: Zhang, Yaofang, et autres
Publié: (2026)

Learning to Rank the Initial Branching Order of SAT Solvers
par: Eriksson, Arvid, et autres
Publié: (2026)

Deeply Optimizing the SAT Solver for the IC3 Algorithm
par: Su, Yuheng, et autres
Publié: (2025)

Search-Driven Clause Learning for Product-State Quantum $k$-SAT (PRODSAT-QSAT)
par: González-Castillo, Samuel, et autres
Publié: (2026)

Evaluating SAT and SMT Solvers on Large-Scale Sudoku Puzzles
par: Davis, Liam, et autres
Publié: (2025)

CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses
par: Dobos-Kovács, Mihály, et autres
Publié: (2025)

Partial Quantifier Elimination By Certificate Clauses
par: Goldberg, Eugene
Publié: (2020)

RustSAT: A Library For SAT Solving in Rust
par: Jabs, Christoph
Publié: (2025)

Equational Theorem Proving for Clauses over Strings
par: Kim, Dohan
Publié: (2023)

Disjoint Partial Enumeration without Blocking Clauses
par: Spallitta, Giuseppe, et autres
Publié: (2023)

CTL* Verification and Synthesis using Existential Horn Clauses
par: Carelli, Mishel, et autres
Publié: (2024)

Testing for Renamability to Classes of Clause Sets
par: Brandl, Albert, et autres
Publié: (2025)

Extended Resolution Clause Learning via Dual Implication Points
par: Buss, Sam, et autres
Publié: (2024)

SAT-Based Subsumption Resolution
par: Coutelier, Robin, et autres
Publié: (2024)

Life span of SAT techniques
par: Fleury, Mathias, et autres
Publié: (2024)

SAT-Inspired Higher-Order Eliminations
par: Blanchette, Jasmin, et autres
Publié: (2022)

Between proof construction and SAT-solving
par: Schubert, Aleksy, et autres
Publié: (2024)

Efficient Neural Clause-Selection Reinforcement
par: Suda, Martin
Publié: (2025)

Empirical Impact of Dimensionality on Random Geometric SAT
par: Rädiker, Flora
Publié: (2026)

Compact SAT Encoding for Power Peak Minimization
par: Van Kieu, Tuyen, et autres
Publié: (2025)

SAT Solving for Variants of First-Order Subsumption
par: Coutelier, Robin, et autres
Publié: (2024)

SAT-based Learning of Computation Tree Logic
par: Pommellet, Adrien, et autres
Publié: (2024)

Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
par: Katsura, Hiroyuki, et autres
Publié: (2025)

A Coq Library of Sets for Teaching Denotational Semantics
par: Cao, Qinxiang, et autres
Publié: (2024)

Catamorphic Abstractions for Constrained Horn Clause Satisfiability
par: De Angelis, Emanuele, et autres
Publié: (2024)

Approaching the Conway-99 problem using SAT solvers
par: Keramatipour, Ali
Publié: (2026)

Structure-Aware Computing, Partial Quantifier Elimination And SAT
par: Goldberg, Eugene
Publié: (2024)

DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
par: Feng, Nick, et autres
Publié: (2024)

SAT-Based Techniques for Lexicographically Smallest Finite Models
par: Janota, Mikoláš, et autres
Publié: (2025)