Presentation
Dropping Multiple Literals per SAT Call in IC3 Model Checking
DescriptionIC3 is the state-of-the-art model checking algorithm where generalizing
cubes by dropping literals one-by-one is the most computationally
expensive step. We propose multi-literal drop strategies that
eliminate two or more literals simultaneously. Successful n-drop saves
n−1 SAT invocations. To mitigate performance losses from failures,
we introduce deduction mechanisms that analyze counterexamples to
generalization and identify non-droppable literals early. With these, failed
multi-drop attempts are sometimes as useful as conventional
single-drops. Additionally we analyze the diminishing returns of higher-order
drops. Implementation on ABC solves 28 unique and 16 more cases than
vanilla ABC and implementation on rIC3 runs 6% faster.
cubes by dropping literals one-by-one is the most computationally
expensive step. We propose multi-literal drop strategies that
eliminate two or more literals simultaneously. Successful n-drop saves
n−1 SAT invocations. To mitigate performance losses from failures,
we introduce deduction mechanisms that analyze counterexamples to
generalization and identify non-droppable literals early. With these, failed
multi-drop attempts are sometimes as useful as conventional
single-drops. Additionally we analyze the diminishing returns of higher-order
drops. Implementation on ABC solves 28 unique and 16 more cases than
vanilla ABC and implementation on rIC3 runs 6% faster.
Event Type
Research Manuscript
TimeWednesday, July 2910:54am - 11:06am PDT
LocationMtg Room 202AB