IC3/PDR

P-IC3: Racing Three IC3 Workers with Different Literal-Deletion Orders

Parallel portfolios provide a practical means of exploiting the behavioral diversity of IC3/PDR heuristics. Building on the observation that different literal-deletion orders can lead to different generalized clauses and verification trajectories, we …