← Search

Leroy Chew

2 accepted papers

2024

Hardness of Random Reordered Encodings of Parity for Resolution and CDCL

AAAI 2024technical

Parity reasoning is challenging for Conflict-Driven Clause Learning (CDCL) SAT solvers. This has been observed even for simple formulas encoding two contradictory parity constraints with different variable orders (Chew and Heule 2020). We provide an analytical explanation for their hardness by showi…