BEGIN:VCALENDAR
VERSION:2.0
PRODID:Linklings LLC
BEGIN:VTIMEZONE
TZID:America/Los_Angeles
X-LIC-LOCATION:America/Los_Angeles
BEGIN:DAYLIGHT
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
DTSTART:19700308T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=2SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
DTSTART:19701101T020000
RRULE:FREQ=YEARLY;BYMONTH=11;BYDAY=1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20260730T152728Z
LOCATION:Mtg Room 202AB
DTSTART;TZID=America/Los_Angeles:20260729T105400
DTEND;TZID=America/Los_Angeles:20260729T110600
UID:dac_DAC 2026_sess163_RESEARCH2512@linklings.com
SUMMARY:Dropping Multiple Literals per SAT call in IC3 Model Checking
DESCRIPTION:Tianjun Bu, Zhichao Lyu, and Qiusong Yang (Institute of Softwa
 re, Chinese Academy of Sciences)\n\nIC3 is the state-of-the-art model chec
 king algorithm where generalizing\ncubes by dropping literals one-by-one i
 s the most computationally\nexpensive step. We propose multi-literal drop 
 strategies that\neliminate two or more literals simultaneously. Successful
  n-drop saves\nn−1 SAT invocations. To mitigate performance losses from fa
 ilures, \nwe introduce deduction mechanisms that analyze counterexamples t
 o \ngeneralization and identify non-droppable literals early. With these, 
 failed \nmulti-drop attempts are sometimes as useful as conventional\nsing
 le-drops. Additionally we analyze the diminishing returns of higher-order\
 ndrops. Implementation on ABC solves 28 unique and 16 more cases than\nvan
 illa ABC and implementation on rIC3 runs 6% faster.\n\nTopics: EDA\n\nTrac
 k: EDA2. Design Verification and Validation\n\nSession Chairs: Jeff Dyck (
 Siemens) and Nan Wu (George Washington University)\n\n
END:VEVENT
END:VCALENDAR