6 papers
Understanding CDCL Solvers via Scalability Studies and Proofdoors
Shimin Zhang, Yechuan Xia, Chunxiao Li +3
Over the past several decades, CDCL SAT solvers have proven remarkably effective on large industrial formulas, despite SAT being NP-complete and widely believed to be intractable.…
TreeTeaming: Autonomous Red-Teaming of Vision-Language Models via Hierarchical Strategy Exploration
Chunxiao Li, Lijun Li, Jing Shao
The rapid advancement of Vision-Language Models (VLMs) has brought their safety vulnerabilities into sharp focus. However, existing red teaming methods are fundamentally constraine…
A Reinforcement Learning based Reset Policy for CDCL SAT Solvers
Chunxiao Li, Charlie Liu, Jonathan Chung +3
Restart policy is an important technique used in modern Conflict-Driven Clause Learning (CDCL) solvers, wherein some parts of the solver state are erased at certain intervals durin…
Limits of CDCL Learning via Merge Resolution
Marc Vinyals, Chunxiao Li, Noah Fleming +2
In their seminal work, Atserias et al. and independently Pipatsrisawat and Darwiche in 2009 showed that CDCL solvers can simulate resolution proofs with polynomial overhead. Howeve…
On the Hierarchical Community Structure of Practical Boolean Formulas
Chunxiao Li, Jonathan Chung, Soham Mukherjee +5
Modern CDCL SAT solvers easily solve industrial instances containing tens of millions of variables and clauses, despite the theoretical intractability of the SAT problem. This gap…
Towards a Complexity-theoretic Understanding of Restarts in SAT solvers
Chunxiao Li, Noah Fleming, Marc Vinyals +2
Restarts are a widely-used class of techniques integral to the efficiency of Conflict-Driven Clause Learning (CDCL) Boolean SAT solvers. While the utility of such policies has been…