Presentation
SAT-Helper: A Multi-Agent System for Adaptive Optimizing Large-Scale Conjunctive Normal Form
DescriptionLarge-scale CNFs exceed LLM context windows, and direct rewriting can break equivalence. SAT-Helper is a zero-shot multi-agent CNF optimizer that samples sliding windows, selects small high-impact blocks and local strategies, rewrites only those blocks, and accepts updates only after SAT-based equivalence checking. This jointly addresses scalability, adaptivity, 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 direction for LLM-assisted SAT solving.
Event Type
Late Breaking Results
TimeMonday, July 275:48pm - 5:51pm PDT
LocationExhibit Hall