提出并行算法分解复杂电路SAT实例，提升求解效率。
Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances
- 用专用约束将原SAT实例拆分为弱化公式族
- 通过并行计算硬度估计，高效找到优质分解方案
- 适用于布尔电路等价性验证和哈希函数预像攻击
我们提出一种新型并行算法，用于分解复杂的CircuitSAT实例。该方法利用特定约束将原始SAT实例划分为一系列弱化公式。算法以参数化并行形式实现，调整参数可高效识别高质量分解方案，其过程由并行计算的硬度估计引导。我们在具有挑战性的CircuitSAT实例上验证了该算法的实际有效性，包括编码布尔电路等价性检查及密码哈希函数预像攻击的实例。
原文摘要 · Abstract (English)
We propose a novel parallel algorithm for decomposing hard CircuitSAT instances. The technique employs specialized constraints to partition an original SAT instance into a family of weakened formulas. Our approach is implemented as a parameterized parallel algorithm, where adjusting the parameters allows efficient identification of high-quality decompositions, guided by hardness estimations computed in parallel. We demonstrate the algorithm's practical efficacy on challenging CircuitSAT instances, including those encoding Logical Equivalence Checking of Boolean circuits and preimage attacks on cryptographic hash functions.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。