2 papers
cs.DM2025
An Expansion-Based Approach for Quantified Integer Programming
Michael Hartisch, Leroy Chew
Quantified Integer Programming (QIP) bridges multiple domains by extending Quantified Boolean Formulas (QBF) to incorporate general integer variables and linear constraints while a…
cs.CC2024
Hardness of Random Reordered Encodings of Parity for Resolution and CDCL
Leroy Chew, Alexis de Colnet, Friedrich Slivovsky +1
Parity reasoning is challenging for Conflict-Driven Clause Learning (CDCL) SAT solvers. This has been observed even for simple formulas encoding two contradictory parity constraint…