FOCON: Formula-Conditioned Receiver-Aware Clause Communication Network for Parallel SAT Solving

Learned-clause exchange is a key mechanism in parallel conflict-driven clause learning (CDCL), whereas existing sharing policies largely assess clause utility through global statistics, overlooking the dependence of utility on formula structure and the evolving search state of the receiver. We formulate clause exchange as formula-conditioned, receiver-aware communication and propose FOCON, a lightweight learned router that selects clause imports without modifying symbolic CDCL. A polarity-equivariant factor network processes each CNF once to produce signed structural context and formula-specific routing coefficients. Each candidate transfer is then scored from clause structure and directed sender-receiver states through a compact event-level scorer. FOCON learns from latency-discounted clause reuse, regulates communication through adaptive budget control, and falls back to native sharing outside the learned support. Experiments demonstrate that FOCON achieves aggregate gains over state-of-the-art learning-guided methods and solver baselines while accepting only about $20\%$ of candidate transfers and remaining effective across unseen SAT families and distinct problem encodings.