标签
This paper introduces an inprocessing framework for neural network verification driven by lookahead lemmas, improving the performance of verifiers Marabou and α-β-CROWN by proving up to 34% more instances unsatisfiable.
本文研究针对具有伪布尔约束的布尔可满足性问题的并行连续局部搜索（CLS），发现冗余约束会抑制收敛，且CLS在混合设置中作为子求解器具有潜力。
本文提出了加速傅里叶SAT（AFSAT），一种基于连续局部搜索的GPU加速伪布尔可满足性求解器。它通过支持异构约束并利用JAX进行并行计算，改进了先前的概念验证实现。
本文研究了如何将因子化规划任务（FTS）编码为SAT，提出了多种编码策略，并分析了任务转换对基于SAT的规划性能的影响。其目的是将SAT求解扩展到比启发式搜索更紧凑的规划表示。