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:20260730T152640Z
LOCATION:Exhibit Hall
DTSTART;TZID=America/Los_Angeles:20260728T174400
DTEND;TZID=America/Los_Angeles:20260728T174400
UID:dac_DAC 2026_sess306_LBR124@linklings.com
SUMMARY:SAT-Helper: A Multi-Agent System for Adaptive Optimizing Large-Sca
 le Conjunctive Normal Form
DESCRIPTION:Zhiyuan HE and Rongliang Fu (The Chinese University of Hong Ko
 ng), Pin-Yu Chen (IBM Research), and Tsung-Yi Ho (The Chinese University o
 f Hong Kong)\n\nLarge-scale CNFs exceed LLM context windows, and direct re
 writing can break equivalence. SAT-Helper is a zero-shot multi-agent CNF o
 ptimizer that samples sliding windows, selects small high-impact blocks an
 d local strategies, rewrites only those blocks, and accepts updates only a
 fter SAT-based equivalence checking. This jointly addresses scalability, a
 daptivity, and correctness. On CNFgen and SAT Competition 2025, SAT-Helper
  cuts solving time by 68.0% and 80.2% while reducing memory by 18.7--25.7%
 . The results show that verified input-side optimization is a practical di
 rection for LLM-assisted SAT solving.\n\nTrack: Student\n\n
END:VEVENT
END:VCALENDAR