理论计算机科学电子笔记128（2005）75-90www.elsevier.com/locate/entcs并行多线程可满足性求解器的设计与实现Yulik Feldmana、Nachum Dershowitzb和Ziyad Hannaaa英特尔公司，海法，{yulik.feldman，ziyad.hanna}@ intel.comb以色列特拉维夫，特拉维夫大学计算机科学学院nachum. cs.tau.ac.il摘要我们描述了一个高度优化的，多线程算法的命题满足性问题的设计和实现。该算法基于Davis-Putnam-Logemann- Loveland顺序算法，但包括近年来引入的许多优化技术。我们提供了实验结果的并行算法在各种多处理器机器上的共享内存架构的执行。特别地，研究了并行执行对处理器Cache性能的不利影响保留字： 并行多线程DPLL缓存性能1介绍本文描述了一个高度优化的，并行多线程算法解决命题满足性问题（SAT）的设计和实现。SAT是计算理论中的一个基本问题，自从1960年引入第一个算法以来，已经被广泛研究了四十多年[5]。11年后，它成为第一个被证明是NP完全的问题，在Cook的著名论文中。如今，这个问题在广泛的学科中具有重要的实际意义，包括硬件验证[17]，人工智能[10]，计算机视觉[2]等。事实上，一项满意度调查[6]包含200多个应用参考。尽管其计算复杂性，但在工业中对高性能SAT求解算法多年来，许多不同的...1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.10.02076Y. Feldman等人理论计算机科学电子笔记128（2005）75已经开发了不同的方法和优化来更有效地解决该问题。算法已经通过用新的、更强大的优化来扩展现有的方法而逐渐发展。目前关于命题可满足性的研究主要集中在两类SAT求解方法上：完全算法和不完全过程。完整的方法，主要是回溯搜索算法，识别满意和不满意的问题，并在这两种类型上表现出相当好的性能。不完整的方法，主要表现为局部搜索过程的变化回溯搜索算法能够处理不令人满意的问题，这一事实通常使它们成为需要证明不令人满意的领域的首选。我们实现了一个完整的回溯搜索并行算法，在企业最先进的顺序技术，近年来推出。重点一直是提供一个高效的便携式implementation，将工作在任何典型的多处理器工作站在工业环境中，并提高运行时间，与核心顺序算法相比，通过分配工作负载在几个处理器上的机器。为了确保实现是有效的，并且正确理解低级实现细节，求解器的实现不是基于其他求解器的现有公开源代码，而是从头开始设计和编码。该实现经过精心设计，可以直接将其行为与现有的顺序算法进行比较。算法实现完成后，在不同的现实生活环境中的行为进行了测量。特别地，研究了多线程并发执行对平台体系结构原语（如处理器缓存、总线利用率和资源 分 配 ） 的 影 响 这 项 工 作 的 主 要 贡 献 是 ， 它 显 示 了 一 般 的discrimineousness并行执行的回溯搜索算法在多处理器工作站上，由于增加高速缓存未命中。本文的其余部分组织如下：第2节简要介绍了SAT问题。第3节给出了一个概述的国家的最先进的技术用于实现顺序求解器，而第4节描述了用于并行化的核心顺序算法的方法。第5节报告的结果，实验运行的实施并行SAT求解器。第6节描述了并行SAT求解领域的相关工作，并在简短的结论部分。Y. Feldman等人理论计算机科学电子笔记128（2005）75772SAT问题命题可满足性问题可以简单地用一句话来表述：给定一个布尔公式，检查是否存在布尔真值对公式中命题变量的赋值，使得公式求值为真。如果存在这样的赋值，则称公式是可满足的;如果不存在这样的赋值，则称公式是不可满足的。对于一个有n个变量的公式，有2n个可能的真值赋值。虽然有许多方法来表示布尔公式，但合取范式（CNF）最常用于此目的。一般来说，使用CNF表示公式并不是一个限制，因为任何布尔公式都可以在多项式时间内转换为CNF（带有额外变量）中的等价满足公式[14]。 在CNF中，公式中的变量以文字形式出现，它要么是一个单独的变量（x），要么是一个变量（x′）的函数。 文字被分组到子句中，子句表示它们所包含的文字的析取（逻辑或）。单个文本可以出现在任意数量的子句中。 所有子句代表一种形式。例如，用于多个（x 1 <$x<$2）<$（x<$3）<$（x1<$x3）的CNF包含三个类：x1<$x<$2、x<$3和x1<$x3。两个例子中的两个例子是po sitive（x1，x3）和两个representative（x<$2，x<$3）。 注意，对于满足CNF公式的可变赋值，它必须满足其每个子句。为例如，如果x1为真，x3为假，则所有三个子句都满足，而不管x2的值如何。3顺序SAT在我们的并行实现中使用的顺序SAT求解算法基于常用的Davis-Putnam-Logemann-Loveland算法（DPLL）[4]，该算法执行分配的系统枚举，寻找满足公式的分配。为了构建赋值，算法以一定的顺序选择变量，并递增地为每个变量赋值只要得到的部分赋值没有伪造公式，它就会继续选择变量并赋值。如果产生的部分赋值使公式证伪，则算法将相反的值赋给最后选择的变量，并检查产生的赋值是否仍然使公式证伪。如果没有，则继续为更多变量赋值。如果公式被证伪，不管最近赋值的变量的值如何，它都会回溯到先前选择的变量，并为其赋值相反的值。该算法以类似的方式继续搜索，如签名、重新分配和取消分配值，直到所有变量都被分配并且公式满足为止，或者，直到所有可能的分配为止。78Y. Feldman等人理论计算机科学电子笔记128（2005）75“不，不。请注意，DPLL并不总是显式访问所有2n个分配，因为一旦发现不满意的部分分配，它就会回溯。原始的DPLL算法结合了一种称为单位传播或布尔约束传播（BCP）的优化技术。 如果当前部分变量赋值导致某个子句的所有文字（除了一个文字）都具有值false，则必须将剩余的文字赋值为true，以便不伪造子句，从而不伪造整个公式。这样的文字称为单位文字，这样的子句称为单位子句。当找到一个单元子句时，算法选择下一个单元文字的变量，并为其分配使子句为真的值。近年来，许多先进的优化技术已经被引入到提高性能的核心DPLL算法。这些方法包括监视文字、冲突分析、非时序回溯、可变状态独立衰减和（VSIDS）决策算法和重启。有关这些技术的描述，请参考[11，13]，所有这些技术都已纳入本文介绍的并行求解器中。我们的求解器在约500个工业测试的基准套件上的单线程配置的实际性能与获奖的zCha时序求解器的性能相当，尽管略低于zCha时序求解器[13]。在这个基准测试套件上，我们的求解器的总运行时间比zChaPython高出约10%，其总内存消耗少了约12%。我们的求解器能够在实验期间设置的时间和内存限制内解决另外七个测试。4并行SAT为了使顺序DPLL算法并行化，将搜索空间划分为若干个不相交的部分，并行处理。SAT搜索空间的一个重要特征是很难预测完成搜索空间的特定分支因此，在算法开始时静态地划分搜索空间是不切实际的，因为对所选划分的复杂性的不正确预测将导致不均匀的工作负载分布，并且伴随地导致算法的效率降低。为了解决这个问题，实现的并行算法动态分区的搜索空间，分配可用的工作，在运行时的可用线程。Y. Feldman等人理论计算机科学电子笔记128（2005）75794.1搜索空间划分为了划分搜索空间，该算法使用引导路径的概念，首先在[1]中引入。引导路径描述搜索过程的当前状态。它通过记录变量列表来实现，直到给定的执行点为止，算法为这些变量赋值。对于每个记录的变量，引导路径关联当前分配的布尔值，以及布尔标记，该标记表示是否已尝试将两个布尔值分配给给定变量，或者当前分配的值是否是唯一尝试分配的值如果一个变量同时被赋值为两个布尔值，则该变量被称为关闭变量;如果一个变量只被赋值为一个布尔值，则该变量被称为打开变量。开放变量表示引导路径上的交叉点，这些交叉点通向尚未探索的搜索空间。在顺序SAT求解算法中，它可以被看作是用单线程工作的并行SAT求解算法的特殊情况被赋予新值的变量被推到堆栈上，因此被添加到当前引导路径的末尾。由于回溯而从堆栈中删除的变量被从引导路径的末尾删除。由于单个线程仅探索开放变量的当前分配值，因此其他线程通过将引导路径上所选开放变量之前的变量分配给引导路径上存储的值，并将分配给开放变量的值重新分配来开始执行。然后将选定的open变量标记为“closed”，以防止其他线程遵循已探索的路径。注意，每个运行的线程维护与其执行状态相关联的私有引导路径。然后，可用的线程可以自由地从任何现有的引导路径中选择任何开放变量来拾取新任务。具有所选开放变量的线程和选择该变量的线程被称为父子关系：具有所选开放变量的线程是父线程;选择该变量的线程是子线程。运行线程形成概念树，其中节点表示线程，边表示父子关系。4.2任务调度并行算法的执行始于由单个节点组成的线程树，该节点被分配了解决整个问题实例的任务。80Y. Feldman等人理论计算机科学电子笔记128（2005）75当第一个线程开始执行时，第一个线程的引导路径上会出现一些打开的变量。第二线程挑选开放变量之一，并将线程树作为根的子节点加入，并探索根正在探索的解空间的子空间。其他线程从其中一个正在运行的线程中选择一个开放变量并加入树，探索其父线程正在探索的子空间。只要有可用的线程加入算法的执行，树就会增长工作线程以两种方式之一完成当前任务的执行：要么线程找到所有变量的赋值，使整个公式得到满足，要么线程发现子空间中不存在这样的赋值。在第一种情况下，停止并行算法并报告解决方案。在第二种情况下，结果并不一定意味着整个公式是不令人满意的，因为当前线程没有搜索到其他线程正在探索的子空间。在这种情况下，已完成的线程从其他线程中的一个线程获取一个开放变量，并开始探索相应的子空间。 完成其最新任务的线程从树中删除，并在不同的分支上再次加入。 如果此时不存在可用的开放变量， 一个可用的线程寻找一个新的任务，线程被暂时挂起，直到一个打开的变量出现。如果所有线程都完成了它们的执行，并且在等待可用任务时处于挂起状态，则这表明搜索空间已被充分探索，问题是无法满足的。注意，通过这种搜索空间的动态划分，工作负载在工作线程之间均匀分布，并且这些线程都保持忙碌，直到问题得到解决。为了最小化线程等待时间和找到新任务所需的时间，维护了一个可用任务列表。当线程引入新的打开变量时，线程将与新变量相关联的任务的描述添加到可用任务列表中。由于打开变量的数量通常比工作线程的数量大得多，线程只在列表大小达到某个阈值时才向列表添加新任务。当线程完成当前任务的执行时，它从列表中选择一个可用的任务，并从列表中删除该任务。 其他线程迅速添加 新任务添加到列表中，并将其大小保持在阈值附近。由于打开变量的数量和线程的数量之间存在很大的差异，空列表上的线程等待时间非常短。这些时间仅限于算法执行开始后的阶段，此时列表仍然为空，直到执行完成前的时间，此时不再有打开的变量。以减少重新初始化线程状态的开销，Y. Feldman等人理论计算机科学电子笔记128（2005）7581从一个任务的执行切换到另一个任务，可用的任务是以这样一种方式选择的这是通过选择最接近引导路径起点的开放变量来实现的。在每个线程中，选择这样一个开放变量作为进入可用任务列表的候选变量。可用任务的列表通过相同的方式根据引导路径的长度进行排序，该引导路径导致任务中的开放变量。这种方法可以防止频繁的任务切换，与顺序算法相比，这种切换会产生额外的开销。除了减少任务切换的开销之外，这些变量的选择还消除了在线程之间实现复杂的消息传递机制的需要，如下所述。4.3合同条款交换虽然线程彼此独立地工作，但并行算法需要对每个线程产生的冲突子句进行特殊处理。冲突子句是由冲突分析算法生成的子句，如[11]所述。这些子句与并行算法使用的其他一些内部数据结构类似，具有与之关联的线程特定数据。 这个数据应该在每个线程的上下文中初始化，让线程从冲突子句的存在中受益。由于子句是由特定的线程生成的，因此有关生成的子句的信息应该分发给其他线程。 这是通过维护可从所有线程访问的生成的冲突子句的列表来实现的。当线程生成冲突子句时，生成它的线程将它放到列表中。其他线程经常检查此列表中是否存在新子句。如果线程检测到在该线程的上下文中尚未初始化的新子句已添加到列表中，则它将该子句重新命名为它自己的上下文，并将子句标记为在它的上下文中初始化。 每当如果一个子句在所有工作线程的上下文中被初始化，则它将从列表中删除。线程之间的冲突子句的分布提高了每个线程执行的搜索的效率，就像它在顺序SAT求解算法中所做它还消除了在线程之间实现复杂的消息传递机制的需要，该机制将允许线程在发现这些任务对于解决问题不是必需的时终止其他线程中的任务的执行。当线程发现冲突并回溯多个变量以解决冲突时，就需要这种终止信号。如果由于另一个线程开始探索解空间的相应子空间而导致其中一个回溯变量关闭，则应通知该探索线程82Y. Feldman等人理论计算机科学电子笔记128（2005）75它的当前任务是超级复杂的，因为它会导致当前线程发现的冲突。终止信号的实现可能是复杂和低效的，这是由于需要实现同步机制来保护线程数据免受来自不同线程的同时访问。幸运的是，如果实现了冲突子句的分发，就不需要显式地向其他线程发出信号。 当当前线程发现一个冲突时，除了回溯几个变量赋值之外，它还生成一个冲突子句来描述冲突的原因，并将该子句放在冲突列表中。一旦另一个线程检测到这个子句在列表中的存在，并在自己的上下文中重新启动它，它将被迫回溯自己，以避免冲突子句中描述的冲突由于任务是基于最接近对应引导路径的开始处发现的开放变量来创建的，因此保证了线程的引导路径上不再有开放变量，并且一旦任务到达引导路径的开始处，回溯算法将终止任务的执行。4.4线程同步开销从实现的角度来看，可用任务列表和尚未被所有线程学习的冲突子句列表与线程执行的其余工作相比，新任务生成和新冲突子句生成都是相对不常见的任务。这使得这些数据结构的同步开销与整体性能相比微不足道。除了这两个全局数据结构之外，求解器还维护另一个全局结构，该全局结构表示正在求解的公式的子句。然而，由于这个数据结构是只读的，它不需要线程同步。其余的数据结构由拥有它们的单个线程访问，因此不需要任何线程同步。因此，线程同步机制的引入不会对核心顺序算法的性能造成显著的开销（更多细节请参见第5图1显示了求解器的高级架构。5实验结果在本节中，提供了在各种机器配置上运行实现的并行多线程SAT求解器的实验结果。应当指出的是，一般来说，很难精确地测量每Y. Feldman等人理论计算机科学电子笔记128（2005）7583可用任务互斥所有线程互斥线程1线程1私有数据线程2线程2私有数据...线程N线程N私有数据原始公式条款（只读）图1.一、并行多线程满意度求解器的高级架构由于在相同环境中连续调用相同测试的运行时的高方差，导致求解器的不稳定。这可归因于两个因素的结合。首先是多线程程序并行执行的固有不确定性。第二个因素是SAT问题的搜索空间的不可预测的不平衡结构。这两个因素一起使得测量单个测试的性能变得困难，单个测试的性能可能在运行与运行之间以数量级变化。为了尽量减少不确定性对结果的影响，本节中的测试运行了几次，并记录了总运行时间。标准偏差在20- 30%的范围内在第一组测试中，我们测量了求解器在单个中等规模SAT问题上的整体性能-在具有不同数量并发运行线程的各种不同机器架构上。选择特定的SAT问题的方式是，它足够复杂，可以客观地测试求解器的整体性能，并且足够小，可以在合理的时间范围内运行多个测试。它也被选中，以便内存消耗不会导致性能瓶颈，并且只测试处理器性能问题是dlx2 aa从“Superscalar对于具有有序执行的2个发布超标量DLX处理器，具有2个流水线，每个流水线具有5个阶段。这个问题有490个变量和2804个子句，是不能令人满意的。求解器的单线程配置需要大约7000个决策和120，000个含义才能得出结论，这是不可满足的。在运行期间，求解器消耗大约1.5MB的堆内存。表1显示了测试中使用的不同机器配置。的84Y. Feldman等人理论计算机科学电子笔记128（2005）75表1机器配置OS处理器类型MHzHTCPUL2一Windows 2000作为 奔腾III700没有41024KB500没有2512KCWindows XP移动式奔腾III800没有1512KD奔腾M1700没有11024KELinux RH 7.1奔腾42400没有1512KF至强2200是的第一章（二）512KG2400是的第二章（四）512KHLinux RH AW 2.1Itanium 2（64位）1300没有2（*）HTcol umnspecifeher技术（HT）启用。当HT被启用时，每个物理处理器被OS视为两个逻辑处理器，从而在系统中的线程之间实现更多的并发性L2列指定每个进程中的L2缓存量所有处理器都有两级缓存，除了Itanium 2处理器（配置H），它有三级缓存（256K的L2缓存和3072K的L3缓存）。表2显示了SAT求解器在表1中的每种配置下的总体性能，其中并发工作线程的数量不同。数字以秒为单位，表示同一测试的10次连续调用的运行时总和可执行文件启动、线程初始化和解析问题的开销在每次调用0.1-0.2秒之间。最后一列给出了四线程配置与单线程配置的性能之比。正如这组测试所示，求解器的整体性能不仅不会随着并发工作线程数量的增加而提高，而且会随着工作线程数量的增加而性能下降在具有多个处理器（无论是物理处理器还是逻辑处理器）的系统上尤为严重。在配置C、D和E（单处理器）中观察到的退化最小。最严重的降级发生在配置G（具有两个处理器并启用HT）。随着线程数量的增加，性能下降的趋势并不局限于表2中所示的配置，最多有四个线程;每个线程Y. Feldman等人理论计算机科学电子笔记128（2005）7585表2不同工作线程配置一两三四四：一一131561896.8B202142472.4C141619221.6D131514151.2E777101.4F82027536.6G65519516828.0H6528610717.8当工作线程的数量增加到四个以上时，线程的性能会继续下降。当在其他问题上调用求解器时，观察到类似的情况。上述结果表明，运行在不同处理器上的线程之间存在某种干扰，从而导致性能下降。 为了定位这种干扰的可能来源，详细分析了具有不同三个广告中有一个没有。我不知道VTuneTM性能分析器[8]用于收集数据并进行分析。 初查相对于系统中其他进程的求解器进程行为的分布、进程内线程的负载分布和线程内函数调用的分布并没有揭示随着工作线程数量的增加而导致性能下降的原因。与工作线程的数量无关，求解器进程占据了处理器总负载的很大一部分，进程线程之间的负载分布均匀，线程内部的性能瓶颈出现相同的函数调用模式与其他DPLL满意度求解器的性能报告一致，在大约70%的总运行时间内，线程忙于运行布尔约束传播算法，而这个数字并不随工作线程的数量而变化。随着线程数量的增加，唯一改变的是不同函数等待共享数据结构的同步锁的时间。但是，即使在四个运行线程的情况下，总等待时间也没有达到总运行时间的10%，这个百分比无法解释性能86Y. Feldman等人理论计算机科学电子笔记128（2005）75在上述测试中观察到的降解。在VTune采样性能分析的帮助下虽然求解器进程的CPI在具有一个线程的配置中约为1.4，这对于此类处理器来说被认为是非常好的，但CPI在具有四个线程的配置中增长到约3.7，这被认为是差的。为了进一步调查这种降级的原因，分析了处理器监视事件的行为。处理器监视事件是硬件级处理器专用计数器，用于监视低级处理器事件，例如缓存未命中和总线利用率。（有关处理器监视事件的详细说明，请参阅[7]。）总共进行了200多项不同的测试，并收集了详细的统计数据。由于篇幅有限，表3只显示了最有趣的结果。表中的所有测试都是在同一台机器上针对同一个SAT问题运行的（表1中的配置B）。该表显示的不是各种处理器监视事件的原始值，而是这些事件与其他相关基本事件的比率。这些比率使数字独立于进程的实际运行时间。 特别是，由于工作线程数量的增加而增加的测试运行时间对比率没有影响。例如，“已解码指令/时钟信号”比率表示每个处理器时钟信号的已解码指令的平均数量，与实际执行了多少个如表3所示，上述比率中的大多数都受到线程数量增加的强烈影响。运行的线程越多，比率看起来就越差。最严重的问题是高速缓存和内存未命中的增加，这会大大降低执行速度。当一个线程运行时，平均需要再次注意的是，这些数字与实际执行时间无关，实际执行时间随线程数而变化。有几个因素可能导致高速缓存未命中增加。一个是并行SAT求解算法的本质要求为每个附加线程复制存储算法的当前状态的大多数辅助数据结构。线程之间唯一可以共享的数据是公式子句的文字集。这并不构成全部处理数据的主要部分。内存分配数量的增加导致高速缓存未命中数量的增加。表4显示了Y. Feldman等人理论计算机科学电子笔记128（2005）7587表3不同工作线程数的处理器监视事件比率比一两三四部分失速周期/时钟信号0.02160.04130.04830.0427资源相关暂停/时钟信号0.27580.76200.45650.4439二级缓存读取/DMR（*）0.01350.01750.03030.0314二级缓存写入/DMR0.00170.00410.00960.0088L2 M状态线路分配/DMR0.00050.00530.00940.0066L2 M状态行被逐出/DMR0.00040.00360.01090.0082外部总线周期/时钟信号0.00080.00700.00790.0095指令解码/时钟信号0.79080.59840.48550.4511二级缓存请求未命中/DMR0.00130.00750.01260.0096（*）数据存储器引用表4不同工作线程决定1000200030004000500060007000一个线程87296810361104130814641596两个线程1172140815281624175618281912三个线程1416147215841668192819762100四个线程1648176820802232234023922592分配的堆内存作为工作线程数和求解器所做决策数的函数。请注意，当使用多个线程时，由于算法的不确定性，在测试SAT问题的解决过程中做出的决策的实际数量可能在大约2000到大约9000之间变化。表4中的数据显示了在求解器调用期间进行的近似内存分配（以MB为单位），这些调用总共产生了大约7000个决策。除了增加的内存分配数量之外，该算法无法以线性方式处理数据以允许预取即将到来的相反，数据是以几乎随机的顺序访问的，在单个线程内，此外，不同线程之间没有相关性。频繁88Y. Feldman等人理论计算机科学电子笔记128（2005）75对来自增加数量的位置的数据的访问也导致增加的高速缓存未命中。当该算法在多处理器机器上运行时，由于一个处理器对数据的改变使保持其他处理器中改变的数据周围的存储器区域的高速缓存行现代SAT求解器的数据结构和算法在高速缓存未命中方面是高度优化的，因此在多线程环境中高速缓存未命中数量的急剧增加似乎超过了在单个多处理器机器上并行执行部分问题的潜在优势。这些假设的根本原因的性能下降是基于实验结果和详细分析的实现算法，在已经投入了相当大的努力，试图优化缓存的行为。然而，在多线程环境中，数据结构的某些替代组织或不同的顺序或并行算法可能会减少缓存未命中的数量。6相关工作关于并行化SAT求解算法的研究可以追溯到1994年Bohm和Speckenmeyer的论文[1]，他们在由320台T800 Transputer组成的并行MIMD机器上提出了一种用于k-SAT问题的简单顺序Davis-Putnam（DP）SAT求解算法的并行化。作者展示了随着处理器数量的增加而线性加速。 在随后的几年里，一些著作在该领域的并行SAT算法出版。这些包括并行化DP/DPLL算法的更高级版本，例如PSATO [19]和并行Satz [9]，并行化局部搜索算法[12]和基于硬件的方法[20]。其中最有趣的是PaSAT的实现[15，16]，这是一个基于DPLL的SAT求解器的并行版本，它结合了许多最近引入的技术，如冲突分析，非时序回溯和动态学习。 作者着重研究了并行环境下的动态学习行为及其对系统整体性能的影响。并行求解器在24个Sun工作站的集群上运行，并观察到不同的动态学习参数在几个测试用例上的变化。在许多情况下，作者实现了线性，甚至超线性，在运行线程数量方面加速本文所介绍的工作与上述工作有两个主要方面的不同。首先，已经进行了大量的实验，以有效地实现最先进的顺序SAT求解Y. Feldman等人理论计算机科学电子笔记128（2005）7589技术，使得单线程算法的性能直接与其他现代SAT求解器相媲美。这允许在现实环境中研究算法的并行执行的代价，在现实环境中，它必须与SAT求解算法的其他实现优化共存。这也使得观察到对顺序算法的高度优化的缓存性能的负面影响成为可能这和以前的作品之间的另一个主要区别是，我们已经调查了并行执行的SAT求解算法在一个单一的多处理器工作站共享内存体系结构，而不是在一个集群的网络连接的机器上执行。在一个典型的工业环境中，由于缺乏足够的资源，通常很难将一组联网的机器专用于解决SAT问题。另一方面，公司工作站上的一个或多个处理器空闲是很常见的，因为操作系统无法将单线程SAT求解算法的工作负载分配给其他处理器。然而，虽然它是可能实现一个线性的速度提高一个集群的网络连接的机器，共享内存architec- ture对缓存性能的影响似乎减少了并行执行的优势，在一个单一的多处理器工作站。7结论前面的部分给出了在具有共享存储器结构的单个多处理器工作站上运行高度优化的并行SAT求解算法结果显示缓存性能以及总运行时间受到非常显著的不利影响。高速缓存的性能是如此之大的影响，总的运行时间的增长与运行线程的数量增加，尽管不同的处理器之间的工作负载分布。这种效应在各种硬件和系统配置上保持相似，随着处理器数量的增加，这种效应会变得更强。SAT问题的结构和回溯搜索SAT算法使得在并行执行部分问题时很难调整数据结构或算法以获得更好的缓存局部性。因此，试图通过在多处理器工作站上并行执行来优化回溯搜索算法似乎没有实际的优势。90Y. Feldman等人理论计算机科学电子笔记128（2005）75引用[1] 马克斯·博姆和埃瓦尔德·斯佩肯迈尔。http://citeseer.ist.psu.edu/51782.html“A fast parallelSAT-solver - efficient workload balancing”, URL:[2] 罗纳德·T.Chin和Charles R.戴尔机器人视觉中基于模型的识别，ACM Computing Surveys，67[3] Stephen A.厨师. 定理证明过程的复杂性，第三届ACM计算理论研讨会论文集，151[4] 马丁·戴维斯，乔治·洛格曼和唐纳德·W·洛夫兰定理证明的机器程序，ACM杂志，394[5] 马丁·戴维斯和希拉里·帕特南A computing procedure for quantification theory，Journalof the ACM，201[6] JunGu ，Paul W. 作者声明：by J. 哇。“http://citeseer.ist.psu.edu/56722.html 满 足 性（SAT）问题的算法：调查”，URL：www.example.com，1996年。[7] Intel Corp.http://developer.intel.com/design/Pentium4/[8] 我的天啊。 “I n t e l r V Tune T M Pe r for m an n c e A n a l y z e r“，U RL：http：//www.intel.com/software/products/vtune/vpa/index.htm、2004年[9] Bernard Jurkowiak，Chu Min Li和Gil Utard。使用动态工作负载平衡来优化Satz，离散数学中的电子笔记，9（2001）。[10] 亨利·考茨和巴特·塞尔曼统一基于SAT和基于图形的规划，基于逻辑的人工智能研讨会，1999年。[11] JoJaoP.MArqu es-S ilvandK. A. 一个小时。 Conpropositionalsatisability，Proceedings ofthe IEEE International Conference on Tools with Arti tificial Intelligence，1996。[12] 西蒙尼湖塞尔索·马丁斯毛里西奥·里贝罗苏扎一个并行GRASP的Steiner问题的图，工作坊并行算法不规则结构的问题，1998年。[13] 马修·WConor F. MoskewiczMadigan，Ying Zhao，Lintao Zhang and Sharad Malik.蔡文龙：一种有效的SAT求解器，第38届设计自动化会议论文集，2001年。[14] David A.普莱斯特和史蒂文·格林鲍姆。一个结构保持子句形式的翻译，符号计算杂志2（1986），293[15] 汽 车 吨 Sinz ， WolfgangBlochinger 和 WolfgangKuch lin 。PaSAT-paralelSAT-check ingithlemma exchange：implementation and applications，Proceedings of SAT 2001.[16] 汽 车 吨 Sinz ， WolfgangBlochinger 和 WolfgangKuch lin 。Parallelepro p opoii o nalsatisfiabilitychecking with distributed dynamic learning ， Parallel Computing 29 （ 7 ）（2003），969-994.[17] 米罗斯拉夫·N Velev和Randal E.布莱恩特有效使用布尔可满足性过程在超标量和VLIW微处理器的形式验证中，设计自动化会议论文集，226[18] 米罗斯拉夫·N维列夫http://www.ece.cmu.edu/“Superscalar Suite 1.0”, URL:[19] 张汉涛，玛丽亚·保拉·博纳西纳，杰祥。PSATO：一个分布式命题证明器及其在拟群问题中的应用，符号计算杂志，1996。[20] 赵颖，沙拉德·马利克，马修·莫斯凯维奇和康纳·马迪根。通过特定应用程序处理加速布尔满足，ISSS，2001年。
我的内容管理
展开
