HornCraft：LLM 辅助的双近似 CHC 求解框架

HornCraft 将 LLM 生成的 DPU（推导力欠近似）与不变量过近似结合，用于约束 Horn 子句求解。在 Spacer 运行 30 分钟仍未解决的 260 个 CHC-COMP 基准上，HornCraft 对 228 个实例给出经认证的判定结果，其中 42 个被认证为不安全，而禁用 DPU 构建与复用时该数字为 22。