pseudo-boolean

本文研究针对具有伪布尔约束的布尔可满足性问题的并行连续局部搜索（CLS），发现冗余约束会抑制收敛，且CLS在混合设置中作为子求解器具有潜力。

本文提出了加速傅里叶SAT（AFSAT），一种基于连续局部搜索的GPU加速伪布尔可满足性求解器。它通过支持异构约束并利用JAX进行并行计算，改进了先前的概念验证实现。