With the increasing availability of parallel computing power, there is a growing focus on parallelizing algorithms for important automated reasoning problems such as Boolean satisfiability (SAT). Divide-and-Conquer (D&C) is a popular parallel SAT solving paradigm that partitions SAT instances into independent sub-problems which are then solved in parallel. For unsatisfiable instances, state-of-the-art D&C solvers generate DRAT refutations for each sub-problem. However, they do not generate a single refutation for the original instance. To close this gap, we present Proof-Stitch, a procedure for combining refutations of different sub-problems into a single refutation for the original instance. We prove the correctness of the procedure and propose optimizations to reduce the size and checking time of the combined refutations by invoking existing trimming tools in the proof-combination process. We also provide an extensible implementation of the proposed technique. Experiments on instances from last year's SAT competition show that the optimized refutations are checkable up to seven times faster than unoptimized refutations.
翻译:随着平行计算能力越来越容易获得,人们越来越重视对重要的自动推理问题,如Boolean satisfifility(SAT)等重要的自动推理问题的平行算法。分化和制化(D &C)是一个流行的平行的平行SAT解决模式,它把SAT情况分割成独立的子问题,然后平行解决。对于不满意的情况,最先进的D&C解答器为每个子问题产生DRAT的反驳。然而,它们并不为最初的例子产生单一的反驳。为了缩小这一差距,我们提出校对-Stitch,这是一个将不同子问题的反驳合并为单一的对原案例的反驳的程序。我们证明程序的正确性,并提议优化,通过在校对过程中取消现有的三联手工具来减少合并的反驳时间。我们还提供拟议的技术的可延续性实施。对去年不相容的SAT竞争实例进行实验,显示最优化的回溯时间比优化的回溯时间要快。