Property Directed Reachability with Extended Resolution

Property Directed Reachability ($\text{textsc}Pdr$), also known as IC3, is a state-of-the-art model checking algorithm widely used for verifying safety properties. While $\text{textsc}Pdr$ is effective in finding inductive invariants, its underlying proof system, Resolution, limits its ability to construct short proofs for certain verification problems. This paper introduces $\text{textsc}PdrER$, a novel generalization of $\text{textsc}Pdr$ that uses Extended Resolution (ER), a proof system exponentially stronger than Resolution, when constructing a proof of correctness. \PdrEV leverages ER to construct shorter bounded proofs of correctness, enabling it to discover more compact inductive invariants. While \PdrEV is based on $\text{textsc}Pdr$, it includes algorithmic enhancements that had to be made in order to efficiently use ER in the context of model checking. We implemented $\text{textsc}PdrER$ in a new open-source verification framework and evaluated it on the Hardware Model Checking Competition benchmarks from 2019, 2020 and 2024. Our experimental evaluation demonstrates that $\text{textsc}PdrER$ outperforms $\text{textsc}Pdr$, solving more instances in less time and uniquely solving problems that $\text{textsc}Pdr$ cannot solve within a given time limit. We argue that this paper represents a significant step toward making strong proof systems practically usable in model checking.