并行化的约束满足问题解算机中的无锁状态合并

背景

诸如处理器、存储器和存储等硬件方面的技术进步持续地担当用于创建更 大且更复杂的、通过处理许多不同类型的媒体数据类型(例如，语音、文本和 视频)来提供更丰富的用户体验的软件应用程序、开发程序等的催化剂。

在单处理器系统中这些厂商所依靠的硬件支持可能是遥远的，因为与摩尔 定律相关联的历史上的电路高速发展(speedup)不再看上去是可容易地获得的。 摩尔定律的原理方面是通常由于设备制造方面的技术进步，芯片上的晶体管数 量将约每十八个月翻倍一次。历史上，当这实现时，处理器时钟速度也可被提 高。然而，现在与更紧密地压缩的晶体管相关联的热密度太高以致于提高时钟 速度意味着无法高效且有效地散热。因此，更小的设备不再直接转换成更快且 更凉快运行的机器。

正在利用的一种替换方案是简单地采用更多的设备。换言之，例如，在处 理器领域，设计并行或多处理器系统以适应软件需求。然而，并行处理系统需 要用于处理算法或计算线程处理的复杂的协调技术。约束解决在测试这些协调 技术时是有用的。然而，传统顺序算法众所周知地难以按有效地利用所有可用 共享存储器的并行处理器的方式来重构。

诸如布尔可满足性(SAT)解算机等约束满足问题(CSP)解算机对于先 前的观察结果也绝不例外。通常，顺序CSP解算机具有包括部分解(对约束变 量中的某一些的赋值)的当前状态，该解算机试图从该当前状态移至具有通过 对一个或多个当前未赋值的变量赋值来创建的增广解的新状态。该新的赋值可 通过约束的传播来引起其他赋值。约束的传播进而可导致检测到肯定是部分完 成的、必须被改变为新赋值并重新传播的当前赋值中的冲突(为了解除冲突)。

在并行处理系统中，该问题解决制度的并行实现必然具有以刚刚描述的方 式传播约束的若干并行计算。问题是将若干无冲突解算机状态合并(后传播) 成单个无冲突解算机状态。

概述

以下呈现了本发明的简化概述，以提供对所公开的本发明的某些方面的基 本理解。该概述不是详尽的概览，它不旨在标识关键/重要的元素，也不旨在描 绘其范围。其唯一的目的是以简化的形式来介绍一些概念，作为稍后提出的更 为详细的描述的序言。

所公开的体系结构提供了对通用约束满足问题(CSP)解算机中的并行处 理的支持。解算机的计算线程的状态被表示为一组支持图。各组支持图是经常 是通用CSP解算机的重要组件的真值维护系统(TMS)的高效实现中的已识 别机制。如此处所描述的，支持图通过以成对的方式来合并这些图从而产生新 的无冲突图来以新方式使用。这允许通过在多个新赋值上映射约束的并行传播 并通过合并从多个传播所得的状态来归约到新问题解算机状态(具有更多赋值 的变量)来构造CSP解算机。该体系结构一般可应用于具有特定形式特性的任 何CSP解算机。例如，在一个实现中，该体系结构可特别地在布尔可满足性 (SAT)解算机的上下文中应用。

此处所公开和所要求保护的体系结构包括便于解算机处理的计算机实现 的系统。该系统包括用于将计算线程的输入解算机状态表示为一组图的薄记组 件。合并组件执行该组图中的至少两个输入图到表示计算线程的最终状态的合 并图的成对合并。

为了实现前述及相关目的，在这里结合下列描述及附图来描述所公开的本 发明的某些说明性方面。然而，这些方面仅指示了其中可利用此处公开的原理 的各种方法中的少数几种，且旨在包括所有这些方面及其等效方面。结合附图 阅读下面的详细描述，则其他优点和新颖特征将变得清楚。

附图简述

图1示出了根据并行实现的便于解算机处理的系统。

图2示出了根据本发明的处理解算机状态的方法。

图3示出了采用学习和推理来推断对答案赋值的猜测的替换并行解算机 系统。

图4示出了从示例性约束传播过程中导出的(L，K)演绎图。

图5示出了用于处理从图4的支持图输出的冲突约束的新的图。

图6示出了准备并合并两个支持图的方法。

图7示出了用于成对合并过程的削减两个输入支持图的方法。

图8示出了处理合并图的冲突的方法。

图9示出了削减支持图并将其合并成顺序SAT解算机的最终合并的无冲 突图的方法。

图10示出了削减支持图并将其合并成并行SAT解算机的最终合并的无冲 突图的方法。

图11示出了将本发明的解算机状态处理应用于多核处理系统的系统的 图。

图12示出了将根据本发明的解算机状态处理应用于多核多处理器系统的 系统的图。

图13示出了将根据本发明的解算机状态处理应用于跨各单独计算系统的 解算机状态处理的系统的图。

图14示出了将应用程序的真值维护系统和推断引擎用作大型搜索空间中 的问题解算机的CSP解算机系统的图。

图15示出了可用于采用所公开的并行化的解算机状态体系结构的计算系 统的框图。

图16示出了可利用根据所公开的本发明的并行化的解算机处理的示例性 计算环境的示意性框图。

详细描述

所公开的体系结构提供了对于常规上已众所周知地难以甚至作为顺序问 题来解决的共享存储器的并行处理器系统的解决方案。本发明提供了并行约束 满足问题(CSP)解算机中的无锁状态合并。解算机的计算线程的状态被表示 为一组支持图。(为了简化起见，在不会随之发生混淆时将使用短语“支持图” 而不是“一组支持图”。)这些支持图通过以描述无锁的过程并产生新的无冲突 支持图的成对方式合并这些图来以新的方式使用。该体系结构一般可应用于其 中底层问题可归纳为布尔可满足性的任何CSP解算机，并且在一个具体实现 中，该体系结构可特别地在布尔可满足性(SAT)解算机的上下文中应用。

在该SAT解算机的具体实现中，SAT解算机问题开始于以两种方式中的 一种引起该问题的一组布尔公式。期望知道该公式是否始终为真。换言之，期 望确定该公式是否是定理。通过对任何公式取补(或反)，一等价问题是确定 该公式是否是可满足的。即询问，存在使该公式为真的变量赋值吗？出于机械 化的目的，这可以是处理该问题的方式。它作为可满足性问题而不是定理证明 问题来处理。

在数字设计的空间中，期望知道布尔公式是否是定理。显示否定式不是可 满足的，而不是证明将显示的公式是定理。布尔公式以诸如例如析取范式等正 则形式来呈现。析取范式是其中公式组是有穷的表示，并且在任一个公式中只 出现两个逻辑连接符，即，求反符(逻辑NOT)和析取(或逻辑OR)。因此， 为了使原始问题(现在是正则形式)变为可满足的，存在确保这些析取公式为 真的变量赋值。正则形式的每一个公式被称为子句。如此处所使用的，术语“子 句”也可指约束。

通常在诸如CSP解算机等这些复杂领域中，不存在可用于导出甚至部分 解的分析方法。必须假设答案，这基本上是猜测。因此，初始假设一旦被程序 认为是真就可随着时间改变并在稍后被发现为假。因此，该程序具有基于稍后 被发现为假的假设来撤销其可能已做出的推断的问题。为了高效，该过程试图 尽可能少地撤销。

由于为了展示可满足性而猜测答案的部分赋值，SAT面临刚刚描述的问 题。该猜测使得其他布尔变量答案由于新猜测的逻辑结果而被赋值。这一猜测 的结果是或者最终做出使得所有变量变为已赋值的一组成功的猜测，或者所做 出的最后一次猜测导致此时放弃这些猜测中的一个的逻辑不一致性。

常规上，可采用按时间顺序的回溯来向后移动，从而选择在某一时刻的一 个变量的值。该回溯可继续直到变量没有剩下供赋值的合法值。

所公开的本发明通过提供撤销最相关的假设(例如，只改变一个假设以及 对中间假设不做改变)的能力来采用“不按时间顺序的”回溯。换言之，与其中 备份改变当前位置和某一早先位置之间的所有节点的常规系统相反，该算法能 够以任意路径返回，挑选一个假设并且只改变该假设。

现在参照附图描述本发明，其中相同的附图标记用于指代全文中相同的元 素。在以下描述中，为解释起见，描绘了众多具体细节以提供对本发明的全面 理解。然而，显然，本发明可以在没有这些具体细节的情况下实现。在其它情 况下，以框图形式示出了公知的结构和设备以便于描述它们。

最初参考各附图，图1示出了根据并行实现的便于解算机处理的系统100。 系统100包括薄记组件102，其用于将与计算线程并行解算机的处理相关联的 解算机状态104(表示为解算机状态1、解算机状态2，...，解算机状态N，其中N 是正整数)表示为一组支持图。解算机状态104能够以并行的方式从不同的系 统接收以供薄记组件102处理。薄记组件102将解算机状态104处理成支持图 以供后续合并。系统100还可包括合并组件106，其用于将该组支持图中的至 少两个输入支持图成对地合并成表示计算线程的最终状态的合并图。

薄记和合并组件(102和106)对支持图的操纵可以是同时的。换言之， 来自一个解算机的解算机状态在处理来自另一个解算机的解算机状态期间接 收并处理。

在一个实现中，薄记组件102从在计算线程上操作的并行CSP解算机接 收输入解算机状态104。如将在下文中更详细地描述的，CSP解算机根据评估 点阵A和一组值D来定义，其中D和A是同一集合。在一更具体的替换实现 中，薄记组件102从在计算线程上操作的并行布尔SAT解算机接收输入解算 机状态104。

在输入解算机状态104是来自在计算线程上操作的两个并行SAT解算机 的情况下，合并组件102帮助将n个新的且不同的文字添加到L完整的、K一 致的演绎图的n个副本中的每一个，其中n是正整数。这也将在以下进一步描 述。

合并组件106在没有循环的情况下以无锁的方式将输入解算机状态合并 成合并图，并消除合并图中的冲突，由此输出无冲突的图108。

对于无锁处理，实现并行性的一种方式是具有处理并行线程处理的能力。 换言之，存在最终需要结果最终化(finalization)的多个并行线程。

执行并行线程处理的一种常规方式是第一线程简单地将其他线程锁定在 某一共享数据结构之外直到该第一线程已达到一结果。该第一线程对获取与先 前线程结果一致的结果的其他线程负有责任。

本发明通过提前一步并行地处理并且然后组合结果来避免常规锁定。因 此，该方法是无锁的，这表现在，因为存在m个独立代理，其中m是正整数， 所以每一个代理都提前一步并且为了获得总答案，这些代理必须组合结果。在 该过程的中心，一次组合两个结果。

在合并支持图时，存在可能发生的若干不合乎需要的事情。第一，在两个 图之间发生冲突。换言之，变量x已在第一图中被赋予一真值而另一图中的同 一变量x具有赋值假。通过求解，合并这两个图并发现导致该冲突的一组假设。 一旦发现，就撤回相关联的假设或假设中的一个。

第二问题可能在一个图中的赋值是假设而另一个图中的相同的赋值是通 过单项消解来导出的时候发生。如果现在试图合并图，则所得图将展示循环。 为了解决，使用贪婪法以非常经济的方式来放弃假设。这将在下面将更详细地 描述。

图2示出了根据本发明的处理解算机状态的方法。尽管出于解释简明的目 的，此处例如以流图或流程图形式示出的一个或多个方法被示出并描述为一系 列动作，但是可以理解和明白，本发明不受动作的次序的限制，因为根据本发 明，某些动作可以按与此处所示并描述的不同的次序和/或与其它动作同时发 生。例如，本领域技术人员将会明白并理解，方法可被替换地表示为一系列相 互关联的状态或事件，诸如以状态图的形式。而且，并非所有示出的动作都是 实施根据本发明的方法所必需的。

在200，从并行解算机的解算机状态中生成支持图。在202，接收解算机 状态的支持图，该解算机状态与计算线程的处理相关联。在204，同时削减来 自每一个解算机的支持图以合并具有相同文字的节点。在206，将支持图成对 地合并成表示计算线程的最终状态的合并的支持图。在208，启动约束传播以 实现合并图的完整性。在210，在约束传播期间利用不按时间顺序的回溯来改 变先前的假设并解决冲突。在212，消除冲突的文字以输出无冲突的合并图。

现在参考图3，示出了采用学习和推理来推断对答案赋值的猜测的替换并 行解算机系统300。系统300包括生成解算机状态的多个系统(例如，两个顺 序解算机系统)302。例如，第一系统304(表示为系统_A)，例如，第一顺序 CSP解算机，生成解算机状态306(表示为解算机状态_A1，...，解算机状态_AS，其 中S是正整数)，而第二系统308(表示为系统_B)，例如，第二串行CSP解 算机，生成解算机状态308(表示为解算机状态_B1，...，解算机状态_BT，其中T是 正整数)。

薄记组件102从相应的第一和第二系统(304和308)接收解算机状态(306 和310)并创建关于并行线程处理并解决系统约束的解算机状态的图(例如， 支持图)。这些图被传递给合并组件106以便合并成具有无冲突状态108的合 并图。然而，该合并图可能不是完整的。因此，利用由传播组件312来促进的 约束传播来确保合并图中的完整性。这将在下面将更详细地描述。传播组件312 还帮助作为约束传播的一部分的不按时间顺序的回溯以便在不改变中间假设 的情况下直接改变早先的假设。

系统300还采用帮助在约束传播期间基于猜测来做出关于变量赋值的推 断的学习和推理组件314(此处也被称为推断引擎)。

系统300可以在其中并非所有答案都是已知的应用中操作。因此，做出关 于世界上正在发生什么的假设。例如，当服务器程序被展示给更多数据时，可 能发生该程序所做出的早先的假设将被发现为假。该程序然后具有撤销可能已 基于假前提做出的推断的问题。

在可满足性问题中，可能存在类似的问题，因为为了展示可满足性，可能 必须猜测答案的赋值。换言之，在顺序的情况下，当做出新猜测时，这导致其 他布尔变量答案由于该新猜测的逻辑结果而被赋值。此外，两件事情中的一件 最终发生。或者做出使得所有变量变为已赋值的一组成功的猜测，或者所做出 的最后一个猜测导致逻辑不一致性，此时放弃这些猜测中的一个。

在布尔可满足性的最经典版本中，改变最后一个猜测的符号，于是如果早 先布尔变量被赋值为假，则将该赋值改为真并且该过程再次继续。逻辑不一致 性在赋值可以是既不为真也不为假时发生是可能的，这意味着某一早先做出的 赋值肯定是错误的。

标识导致所观察到的冲突的一组实际假设，而不是在需要时重复备份并前 进。一旦已观察到冲突，期望确切地诊断出是什么导致了可能是或不是最后一 个假设所造成的冲突。可精确地做出这一诊断并且因此标识一组不兼容的假 设。

本主题体系结构(例如，结合选择)可采用各种基于学习和推理的方案来 实现其各个方面。例如，用于确定要切换(例如，从真到假或从假到真)哪个 赋值的过程可经由自动分类器系统和进程来促进。

分类器是将输入属性向量x＝(x1，x2，x3，x4，xn)映射到类标签class(x)的函 数。分类器也可输出该输入属于一个类的置信度，即f(x)＝confidence(class(x))。 这样的分类可采用概率和/或其它统计分析(例如，分解成分析效用和成本以最 大化对一人或多人的期望价值)来预测或推断用户期望自动执行的动作。

如此处所使用的，术语“推断”和“推论”通常是指从经由事件和/或数据捕捉 的一组观测推理或推断系统、环境和/或用户的状态的过程。例如，推断可用于 标识特定的上下文或动作，或可生成状态的概率分布。推断可以是概率性的， 即，基于对数据和事件的考虑计算所关注状态的概率分布。推断也可以指用于 从一组事件和/或数据合成更高级事件的技术。这类推断导致从一组观察到的事 件和/或储存的事件数据中构造新的事件或动作，而无论事件是否在相邻时间上 相关，也无论事件和数据是来自一个还是若干个事件和数据源。

支持向量机(SVM)是可采用的分类器的一个示例。SVM通过在可能的 输入空间中查找以最佳方式将触发输入事件和非触发事件分离开来的超曲面 进行操作。直观上，这使得分类对于接近但不等同于训练数据的测试数据正确。 可采用其它定向和非定向模型分类方法，包括，例如，各种形式的统计回归、 朴素贝叶斯、贝叶斯网络、决策树、神经网络、模糊逻辑模型以及表示不同独 立性模式的其他统计分类模型。如此处所使用的分类也包括用于分派排序和/ 或优先级的方法。

如从本说明书中可以容易地理解的，本主题体系结构可以使用显式训练 (例如，经由一般训练数据)以及隐式训练(例如，经由观察用户行为、接收 外来信息)的分类器。例如，SVM经由分类器构造器和特征选择模块内的学 习或训练阶段来配置。因此，可采用分类器来根据预定准则自动学习和执行多 个功能。

换言之，学习和推理组件314可将学到的约束应用于冲突处理。一个示例， 如下所述，可将一个学到的约束添加到顺序SAT解算机以便解决冲突。类似 地，在并行SAT解算机中，可在约束传播处理期间添加若干学到的约束。

在查看约束传播示例之前，提供预备信息以便更好地理解。约束满足问题 (CSP)通常如下描述：给定一有限变量集V、(通常是有限的)一组值D， (可能是无限的)评估点阵A和有限函数(约束)集D^|V|→A，在D^|V|中找出 一元组以使得在所有约束下该元组的图像之间的点阵满足在A中最大。以下是 其中D和A两者都是布尔点阵的描述，从而在SAT解算机的上下文中具体描 述了本发明。尽管有此限制，但本发明可推广到其中D和A是相同的集合的 任何CSP。

变量被表示为x₁，x₂，...，x_n，其中n是正整数。文字是“有符号的(signed)” 变量：L是1的范围在L上的文字集。子句是包括表示为□的 空子句的有限文字集。子句经常被改写为(其 元素的逻辑OR(∨))。任何有限命题公式集都可被呈现为在逻辑上等价的有 限子句集。

变量可以是未赋值的，或被赋予值真(例如，x₁)或假(例如，)。 对变量x的值为真的赋值与文字x合并。对变量x的值为假的赋值与文字合并。评估作为将赋值从变量提升到子句的结果归因于子句。满足具有赋值真 的子句，而违反具有赋值假的子句。可满足性是是否存在满足一组子句的逻辑 变量的赋值的问题。重言式是每一个赋值是否满足子句集的问题。可满足性和 重言式是其中公式当且仅当其否定式是不可满足的时候才是重言式的对偶概 念。

让K成为L中的文字上的子句集。(L，K)演绎图是有向图，其节点用与L 的子集配对的单独文字来标记并且其边用K的成员来标记。当不存在关于哪个 L和K是有意义的混淆的时候，该图简单地被称为演绎图。节点是仅在存在其 中边用子句k来标记的从第一个节点到第二个节点的有向边的情况下的对于另 一个节点的k前项。

(L，K)演绎图仅在以下情况下才是正确标记的(well-labeled)：节点上的标 签是其前项节点的标签的并集，如果节点l不具有传入弧，则它用{l}来标记， 对于文字l的节点的所有传入边都用l∨k形式的子句来标记，来自文字l的节 点的所有传出边都用形式的子句来标记。只要存在入射到l节点的被标 记为l∨l₁∨...∨l_m的边，就存在也入射到l节点的被标记为l∨l₁∨...∨l_m的 m-1个其他边。

(L，K)演绎图中用由其本身组成的单元素集(例如，)来标记的 节点l被称为假设文字。正确标记的(L，K)演绎图在入射到节点的传入弧用正好 一个子句来标记的情况下被唯一地证明。正确标记的(L，K)演绎图仅在它不包含 节点1和两者的情况下是K一致的。正确标记的(L，K)演绎图仅在以下情况下 是K完整的：对于l∨l₁∨...∨l_m形式的K中的每一个k而言，只要在该图中，l就在输入入射边用k来标记的图中。无环正确标记的(L，K)演绎图 G在不存在更大的(在节点方面)正确标记的图G’的情况下是L完整的。

图4和图5示出了采用支持图来进行冲突处理的并行化的解算机示例。图 4示出了从示例性约束传播过程中导出的(L，K)演绎图400。为了示出以上定义 的应用，考虑可满足性问题和所尝试的部分解的示例。开始于初始约束集C， 其包括：

ω₈≡(x₁∨x₈)

以及当前假设栈。在演绎图400中，假设被建模为不具有输入弧的假设节 点。因此，图400的假设包括：

x₁@{x₁}，

$⫬x_9@\{⫬x_9\},$

$⫬x_{10}@\{⫬x_{10}\},$以及

$⫬x_{11}@\{⫬x_{11}\}.$

图400包括四个假设节点：第一假设节点402，其中x₁已被赋值为真(例 如，x₁)；第二假设节点404，其中x₉已被赋值为假(例如，)；第三假设 节点406，其中x₁₀已被赋值为假(例如，)；以及第四假设节点408，其 中x₁₁已被赋值为假(例如，)。

查看一瞬时快照，图400指示假设节点具有对x₁的赋值真(例如，x₁)， 而假设节点404具有对x₉的赋值假(例如，)。现在考虑被标记为ω₂边， 即，如以上所列出的约束子句换言之，它可读作“非x₁或 x₃或x₉”。然而，注意，在约束ω₂中，x₁作为来否定地出现，这意味着图 400中为真的赋值使得析取为假，并且如被否定地赋值的x₉也使得x₉析取为 假。但总约束ω₂必须为真，且能够使得约束子句ω₂为真的仅剩的方式是将 x₃赋值为真(例如，x₃)。这正是图400在节点410处通过将x₁赋值为真所指 示的。因此，基于输入节点402和404处的假设，以及相关联的约束ω₂，满足 约束ω₂的唯一方式是将x₃赋值为真。这是单项消解的应用。

继续查看其他节点，到节点412的边使用约束然而，在 节点402处的x₁被赋值为真，这使得满足约束ω₁的仅剩的可能性是将在节点 412处的x₂赋值为真。查看被标记为ω₃的边，约束子句只可通过将在节点414处的x₄赋值为真来满足。换言之，414的输入节点是分 别将x₃和x2赋值为真的410和412，从而使得满足ω₃的仅剩的可能方式是 将x₄赋值为真。

查看被标记为ω₄的边，约束子句只可通过将在节点 416处的x₅赋值为真来满足，因为输入x₁₀被赋值为假并且输入x₄被赋值为真。 被标记为ω₅的边使用约束子句该子句只可通过将在节点 418处的x₆赋值为真来满足，因为输入x₁₁被赋值为假并且输入x₄被赋值为真。 最后，被标记为ω₆的边使用约束子句其基于对在相应的节点 416和418处的x5和x6的赋值真而约束失败。

约束传播导致(L，K)演绎图400并且当到达最后一个节点420时，输出新 导出的约束(以不同的形式来编写的)。

其中κ(卡帕)表示“冲突”并且该约束是什么出错的报告。在此，输出 ω_C(κ(ω₆))指示x₁为真，x₉为假，x₁₀为假，并且x₁₁为假无法同时成立，必 须放弃其中之一以便进一步处理。这等价于正确形式的非x₁或x₉或x₁₀或x₁₁。 图5示出了用于处理从图4的支持图输出的冲突约束的新的图500。选择对以 上各项中的三个或四个的假设(例如，和)产生了新的图500以 及又一新导出的输出约束。

更具体而言，图500通过做出假设(丢弃早先假设中的一个)，即，将假 设节点502、504和506分别用作$⫬x_9@\{⫬x_9\},⫬x_{10}@\{⫬x_{10}\}$和来创建。 开始于这些假设并将该新导出的约束ω_C(κ(ω₆))应用于各边产生对在节点508处 的x₁的赋值假以满足约束ω_C(κ(ω₆))。

查看被标记为ω₇的边，引入了另一假设节点510(被赋值为x₁₂@{x₁₂))， 并且约束子句只可通过将在节点512处的x₇赋值为真来满 足，因为输入x₁被赋值为假并且输入x₁₂被赋值为真。

查看被标记为ω₈的边，约束子句只可通过将在节点514处 的x₈赋值为真来满足，因为输入x₁被赋值为假。现在考虑被标记为(ω₉的边， 约束子句无法使用当前输入(节点512、节点514和假设 节点516)来满足。因此，在节点518处输出的新导出的约束是演绎图500出了什么问题的报告。该约束导出过程继 续直到不存在冲突状态。

更一般而言，一旦获取了每一个并行解算机线程的解算机状态的支持图， 就可开始合并。尽管描述集中于成对合并，但合并可使用不止两个图来实现也 在考虑范围之内。状态合并是无锁的。换言之，实现并行性的一种常规方式涉 及线程处理。例如，在多个并行线程正在处理数据的情况下，最终期望合并这 些线程的结果。这样做的一种方式是通过第一线程简单地将其他线程锁定在某 一共享数据结构之外直到该第一线程完成其过程。因此，其他被锁在外的线程 对写入与已被写入的结果一致的结果负有责任。该常规体系结构至少是低效 的。所公开的体系结构避免了这一显式锁定机制。

如上所述，该算法提前一步并行地进行处理并且然后组合结果。换言之， 为了到达总结果，每一个代理都提前一步进行处理并组合单独的中间结果，并 且这继续直到到达总答案。另外，解决冲突处理并且该合并过程是无循环的。

如上所述，在解冲突(deconflict)处理中，在这些图中的一个或另一个中 可能放弃一个或多个假设。此外，期望对于关于放弃什么假设非常节约。通过 定义供所公开的体系结构使用的所有信息集(例如，假设、演绎、图，...)， 归约算法(此处也被称为redux)以放弃正在合并的两个图之间的尽可能少的 假设的方式来做出选择。回想在单个图的情况下，标识这些冲突的目的是标识 如果被放弃将具有尽可能小的后果的假设，而不是必须备份若干先前的假设， 这是对于一组支持图的目的。

现在将相同的技术应用于一对图，以无循环的方式合并这些图以使得如果 放弃一假设，则影响或丢失尽可能小。这可通过利用“贪婪”法或算法来解决。 换言之，该方法找出通过做出看上去在特定时刻是最佳的选择来最小化被放弃 的东西的容易的方式。可采用利用多得多的分析的更密集的算法；然而，在一 个实现中，该贪婪法足够了。

图6示出了准备并合并两个支持图的方法。在600，接收供处理的两个支 持图。在602，使用贪婪法来削减(或减少)这些图以便合并对应于相同的文 字的节点以减少或消除循环。在604，将支持图合并成合并图。在606，在需 要时通过传播约束来处理合并图以实现完整性。在608，在需要时处理合并图 以解决冲突。在610，输出表示无冲突的解算机状态的最终合并图。

在准备关于如何能够合并两个(L，K)演绎图的更详细的描述时，呈现以下 定义：如果G、G’是非循环的、L完整的(L，K)演绎图，则

C_G，G’是图G和G’所共有的假设集。

A_G是G的假设集。

D_G是G的推论集。

A_G，G’是G中作为G’的推论的假设集。

B_G，G’是G中未在G’中提到的假设集

A_G＝C_G，G’∪A_G，G’∪B_G，G’

A_G’＝C_G，G’∪A_G’，G∪B_G’，G

f_G：A_G→2^L-A_G-f_G是产生G中的假设的依赖项的函数。

$h_G:L-A_G\to 2^{A_G}-h_G$是产生G中的推论的前项的函数。

图7示出了用于成对合并过程的削减两个输入支持图的方法。在700，在 该特定实现中，根据被称为redux的函数来启动该过程。函数redux(G，G′)产生 如下定义的一对图(G₁，G₂)。在702，提供了第一定义：令l∈A_G，G’为一节点以 使得|f_G’(l)|(依赖项集的大小)至少与A_G，G’中的任何其他假设节点的选择一样 大。在704，提供了第二定义：令l′∈A_G’，G为一节点以使得|f_G’(l’)|至少与A_G’，G中的任何其他假设节点的选择一样大。在706，如果|f_G’(l)|比|f_G’(l’)|小，则颠倒 G和G′的角色。在708，选择l″∈h_G’(l)以使得|f_G’(l″)|与l″的任何其他选择 一样小。在710，将G″定义为缺少l″和任一节点l₂的G′的子图以使得l₂处于 |f_G’(l”)|中。在712，如果则退出redux，并返回对(G，G”)。 在714，如果非则调用redux(G，G”)。

最终，redux削减了这两个图以使得对应于相同的文字的节点能够在不害 怕循环的情况下合并。如下所示，redux在其试图放弃尽可能少的派生(derived) (非假设文字)的意义上以“贪婪的”方式削减。期望以最终实现尽可能多的并 行前向进展的方式来消减。然而，可以理解，可采用消减图以便在不害怕循环 的情况下合并的其他算法。

注意，合并图(再次称之为G)不再是L完整的，这可通过传播约束以使 其是L完整的来补救。合并图包含冲突的文字l和也是可能的，在这种情 况下，针对该图计算deconflict(G)，其产生无冲突的图。图8示出了处理合并 图的冲突的方法。在800，在该特定实现中，根据被称为deconflict的函数来 启动移除冲突。在802，选择l′∈h_G(l)以使得|f_G’(l’)|与任何其他这样的选择一 样小。在804，选择$l^{\prime \prime }\in h_G(⫬l)$以使得|f_G’(l”)|与任何其他这样的选择一样小。 在806，如果|f_G’(l’)|≤|f_G’(l”)|，则将l(否则是l′)选为将连同其所有依赖项一 起被删除的假设。在808，重复该过程直到消除所有冲突的节点。

redux和deconflict函数可通过安置merge函数来在SAT解算机中采用， 该merge函数首先对一对图应用redux，并且然后对结果应用deconflict。图9 示出了消减支持图并将其合并成顺序SAT解算机的最终合并的无冲突的图的 方法。在900，在顺序SAT解算机中启动图消减(例如，使用redux)和冲突 处理(例如，使用deconflict)。在902，顺序SAT解算机的内循环将一个新 的文字添加到L完整的、K一致的演绎图。在904，削减支持图以合并节点并 产生无循环处理。在906，传播约束以使得合并图L完整。在908，通过可任 选地添加一个学到的约束来提供无冲突的合并图(使用例如，函数deconflict)。 在910，在需要时重复该过程以输出解算机状态的合并的、无冲突的图。

图10示出了削减支持图并将其合并成并行SAT解算机的最终合并的、无 冲突的图的方法。在1000，在并行SAT解算机中启动图削减(例如，使用redux) 和冲突处理(例如，使用deconflict)。在1002，并行SAT解算机的内循环将 n个新的且不同的文字添加到L完整的、K一致的支持图的n个副本中的每一 个。在1004，削减这n个图以合并节点并产生无循环处理。在1006，在每一 个演绎图中传播约束以使得合并图L完整。在1008，通过可任选地添加学到 的约束来输出无冲突的合并图(使用例如，函数deconflict)。

图11示出了将本发明的解算机状态处理应用于多核处理系统1102的系统 1100的图。多核处理系统1102是共享处理器并行处理系统，其可由两者都在 同一管芯上制造的第一处理核1104(表示为核₁)和第二处理核1106(表示为 核₂)来促进。处理系统1002还可包括用于正在处理的计算线程的共享缓冲的 板载存储器1108。尽管被示为在同一管芯上，但存储器1108可位于该管芯的 外部并用于相同的目的。

为了支持每一个核(1104和1106)对共享线程的处理，提供了一对解算 机。例如，提供第一解算机1110(表示为解算机₁)和第二解算机1112(表示 为解算机₂)(两者都可以是例如CSP解算机)以便在处理器系统1102的多 个核(1104和1106)之间执行线程期间执行约束处理。

提供了用于根据所公开的本发明的成对的支持图处理的状态系统1114。 状态系统1114提供了对以支持图形式从相关联的并行化的解算机(1110和 1112)接收到的解算机状态(表示为解算机₁状态和解算机₂状态)的成对处 理。状态系统1114可包括上述用于实现支持图归约(或削减)、支持图合并、 冲突处理和变量赋值的薄记组件102、合并组件106、传播组件312和推断组 件314。

可以理解，状态系统1114可严格地用软件、严格地用硬件(例如，作为 ASIC-专用集成电路设备或现场可编程门阵列(FPGA))或作为硬件和软件 两者的组合来实现。或者，状态系统1114的组件(102、106、312和314)可 单独地作为硬件和/或软件的组合来实现。

图12示出了将根据本发明的解算机状态处理应用于多核多处理器系统的 系统1200的图。多核多处理器系统1200包括各自是共享存储器并行处理系统 的第一多核处理器系统1202和第二多核处理器系统1204。该第一处理器系统 1202包括第一处理核1206(表示为核₁)和第二处理核1208(表示为核₂)， 这两者在同一管芯上制造并且共享用于正在处理的计算线程的共享缓冲的共 享存储器1208。

该第二多核处理器系统1204包括第一处理核1212(表示为核₁)和第二 处理核1214(表示为核₂)，这两者被在同一管芯上制造并且共享用于正在处 理的计算线程的共享缓冲的共享存储器1216。

为了支持每一个核(1206和1208)对共享线程的处理，提供了相应的解 算机集。例如，提供第一解算机1218(表示为解算机₁)和第二解算机1220 (表示为解算机₂)(两者都可以是例如CSP解算机)以便在处理器系统1202 的多个核(1206和1208)之间执行线程期间执行约束处理。类似地，为了支 持每一个核(1212和1214)对共享线程的处理，提供了相应的解算机集。例 如，提供第三解算机1222(表示为解算机₃)和第四解算机1224(表示为解算 机₄)(两者都可以是例如CSP解算机)以便在处理器系统1204的多个核(1212 和1224)之间执行线程期间执行约束处理。

每一个解算机(1218、1220、1222和1224)将解算机状态传递给状态处 理系统1226。例如，将解算机状态(表示为S₁状态和S₂状态)从该第一处理 系统1202转发到状态系统1226并且将解算机状态(表示为S₃状态和S₄状态) 从该第二处理器系统1204转发到状态系统1226。

提供了用于根据所公开的本发明的成对的支持图处理的状态系统1226。 状态系统1226提供了对以支持图的形式从并行化的解算机(1218、1220、1222 和1224)接收到的解算机状态的成对处理。例如，在这些多核多处理器系统中， 线程计算处理可跨核(1206、1208、1212和1214)的任何组合来发生。例如， 处理可使用核1208、1212和1214来发生。因此，来自这三个核的状态应被传 递给状态系统1226以便根据所公开的算法来进行成对处理。为了对其进行支 持，状态系统1226可包括用于基于线程正在经历的状态处理来从每一个解算 机(1218、1220、1222和1224)中选择相关状态的选择组件1228。换言之， 无关状态将不会被选择以供支持图处理。然而，可以理解，状态处理现在也可 通过包括附加状态系统(未示出)以使得每一个处理器系统(1202或1204) 都具有一个专用状态系统来并行地执行。

如上所述，状态系统1226还可包括上述用于实现支持图归约(或削减)、 支持图合并、冲突处理和变量赋值的薄记组件102、合并组件106、传播组件 312和推断组件314。

另外，将会认识到，状态系统1226可严格地用软件、严格地用硬件(例 如，ASIC、FPGA)或作为硬件和软件两者的组合来实现。

状态系统(图11的1114和/或1226)还可被实现为用于安装到用于处理 解算机状态的计算系统中的独立软件和/或硬件可插入模块。例如，具有高速接 口和存储器(例如，非易失性或闪存)的卡可用作处理器子系统的合适的接口 以及用于解算机状态处理。或者，或与之组合，可安装根据所公开的本发明来 处理解算机状态的软件模块。

图13示出了将根据本发明的解算机状态处理应用于跨各单独计算系统的 解算机状态处理的系统1300的图。在此，第一计算系统1302是具有用于执行 程序和数据处理的系统处理器1304(以及单个核1306)的单处理器系统。第 二计算系统1308是具有用于执行程序和数据处理的多处理器子系统1310(以 及两个处理器1312和1314)的多处理器系统。这些系统(1302和1308)被设 置为在网络1316(或合适的高速接口)上进行通信并且进一步与图12的状态 系统1226进行通信以便进行解算机状态处理。如果一线程跨这两个系统(1302 和1308)处理，则类似于以上在图12中所提供的描述，解算机状态可跨这两 个系统处理。

图14示出了采用真值维护系统1402和推断引擎1404(使用学习和推理) 以便作为大型搜索空间中的问题解算机来应用的CSP解算机系统1400的图。 引擎1404探查各替换方案、做出选择并为了正确性分析选择。当发生冲突时， 真值维护系统帮助消除冲突并相应地更新其知识库以供将来使用。

如在本申请中所使用的，术语“组件”和“系统”旨在表示计算机相关的实 体，其可以是硬件、硬件和软件的组合、软件、或者执行中的软件。例如，组 件可以是但不限于，在处理器上运行的进程、处理器、硬盘驱动器、(光和/ 或磁存储介质的)多个存储驱动器、对象、可执行代码、执行的线程、程序、 和/或计算机。作为说明，运行在服务器上的应用程序和服务器都可以是组件。 一个或多个组件可以驻留在进程和/或执行的线程内，且组件可以位于一台计算 机内上/或分布在两台或更多的计算机之间。

现在参考图15，示出了可用于采用所公开的并行化的解算机状态体系结 构的计算系统1500的框图。为了提供用于其各方面的附加上下文，图15及以 下讨论旨在提供对其中可实现本发明的各方面的合适的计算系统1500的简要 概括描述。尽管以上描述是在可在一个或多个计算机上运行的计算机可执行指 令的一般上下文中进行的，但是本领域的技术人员将认识到，本发明也可结合 其它程序模块和/或作为硬件和软件的组合来实现。

一般而言，程序模块包括执行特定任务或实现特定抽象数据类型的例程、 程序、组件、数据结构等等。此外，本领域的技术人员可以理解，本发明的方 法可用其它计算机系统配置来实施，包括单处理器或多处理器计算机系统、小 型机、大型计算机、以及个人计算机、手持式计算设备、基于微处理器的或可 编程消费电子产品等，其每一个都可操作上耦合到一个或多个相关联的设备。

所示的本发明的各方面也可在其中某些任务由通过通信网络链接的远程 处理设备来执行的分布式计算环境中实施。在分布式计算环境中，程序模块可 以位于本地和远程存储器存储设备中。

计算机通常包括各种计算机可读介质。计算机可读介质可以是可由计算机 访问的任何可用介质，且包括易失性和非易失性介质、可移动和不可移动介质。 作为示例而非限制，计算机可读介质可以包括计算机存储介质和通信介质。计 算机存储介质包括以用于存储诸如计算机可读指令、数据结构、程序模块或其 它数据之类的信息的任意方法或技术实现的易失性和非易失性、可移动和不可 移动介质。计算机存储介质包括但不限于RAM、ROM、EEPROM、闪存或者 其它存储器技术、CD-ROM、数字视频盘(DVD)或其它光盘存储、磁带盒、 磁带、磁盘存储或其它磁存储设备、或可以用于存储所需信息并且可以由计算 机访问的任何其它介质。

再次参考图15，用于实现各方面的示例性计算系统1500包括计算机1502， 计算机1502包括处理单元1504、系统存储器1506和系统总线1508。系统总 线1508提供了用于包括，但不限于系统存储器1506的系统组件对处理单元 1504的接口。处理单元1504可以是各种市场上可购买到的处理器中的任意一 种。双微处理器和其它多处理器体系结构也可用作处理单元1504。

系统总线1508可以是若干种总线结构中的任一种，这些总线结构还可互 连到存储器总线(带有或没有存储器控制器)、外围总线、以及使用各类市场 上可购买到的总线体系结构中的任一种的局部总线。系统存储器1506包括只 读存储器(ROM)1510和随机存取存储器(RAM)1512。基本输入/输出系统 (BIOS)储存在诸如ROM、EPROM、EEPROM等非易失性存储器1510中， 其中BIOS包含帮助诸如在启动期间在计算机1502内的元件之间传输信息的基 本例程。RAM 1512还可包括诸如静态RAM等高速RAM来用于高速缓存数 据。

计算机1502还包括内置硬盘驱动器(HDD)1514(例如，EIDE、SATA)， 该内置硬盘驱动器1514还可被配置成在合适的机壳(未示出)中外部使用； 磁软盘驱动器(FDD)1516(例如，从可移动磁盘1518中读取或向其写入)； 以及光盘驱动器1520(例如，从CD-ROM盘1522中读取，或从诸如DVD等 其它高容量光学介质中读取或向其写入)。硬盘驱动器1514、磁盘驱动器1516 和光盘驱动器1520可分别通过硬盘驱动器接口1524、磁盘驱动器接口1526 和光盘驱动器接口1528连接到系统总线1508。用于外置驱动器实现的接口 1524包括通用串行总线(USB)和IEEE 1394接口技术中的至少一种或两者。 其它外部驱动器连接技术在本发明所考虑的范围之内。

驱动器及其相关联的计算机可读介质提供了对数据、数据结构、计算机可 执行指令等的非易失性存储。对于计算机1502，驱动器和介质容纳适当的数字 格式的任何数据的存储。尽管以上对计算机可读介质的描述涉及HDD、可移 动磁盘以及诸如CD或DVD等可移动光学介质，但是本领域的技术人员应当 理解，示例性操作环境中也可使用可由计算机读取的任何其它类型的介质，诸 如zip驱动器、磁带盒、闪存卡、盒式磁带等等，并且任何这样的介质可包含 用于执行所公开的发明的方法的计算机可执行指令。

多个程序模块可被存储在驱动器和RAM 1512中，包括操作系统1530、 一个或多个应用程序1532(例如，上述无锁CSP解算机处理系统)、其它程 序模块1534和程序数据1536。所有或部分操作系统、应用程序、模块和/或数 据也可被高速缓存在RAM 1512中。应该明白，本发明可以用各种市场上可购 得的操作系统或操作系统的组合来实施。

用户可以通过一个或多个有线/无线输入设备，例如键盘1538和诸如鼠标 1540等定点设备将命令和信息输入到计算机1502中。其它输入设备(未示出) 可包括话筒、IR遥控器、操纵杆、游戏手柄、指示笔、触摸屏等等。这些和其 它输入设备通常通过耦合到系统总线1508的输入设备接口1542连接到处理单 元1504，但也可通过其它接口连接，如并行端口、IEEE 1394串行端口、游戏 端口、USB端口、IR接口等等。

监视器1544或其它类型的显示设备也经由接口，诸如视频适配器1546 连接至系统总线1508。除了监视器1544之外，计算机通常包括诸如扬声器和 打印机等的其它外围输出设备(未示出)。

计算机1502可使用经由有线和/或无线通信至一个或多个远程计算机，诸 如远程计算机1548的逻辑连接在网络化环境中操作。远程计算机1548可以是 工作站、服务器计算机、路由器、个人计算机、便携式计算机、基于微处理器 的娱乐设备、对等设备或其它常见的网络节点，并且通常包括以上相对于计算 机1502描述的许多或所有元件，尽管为简明起见仅示出了存储器/存储设备 1550。所描绘的逻辑连接包括到局域网(LAN)1552和/或例如广域网(WAN) 1554等更大的网络的有线/无线连接。这一LAN和WAN联网环境常见于办公 室和公司，并且方便了诸如内联网等企业范围计算机网络，所有这些都可连接 到例如因特网等全球通信网络。

当在LAN网络环境中使用时，计算机1502通过有线和/或无线通信网络 接口或适配器1556连接到局域网1552。适配器1556可以方便到LAN 1552的 有线或无线通信，并且还可包括其上设置的用于与无线适配器1556通信的无 线接入点。

当在WAN网络环境中使用时，计算机1502可包括调制解调器1558，或 连接到WAN 1554上的通信服务器，或具有用于通过WAN 1554，诸如通过因 特网建立通信的其它装置。或为内置或为外置以及有线或无线设备的调制解调 器1558经由串行端口接口1542连接到系统总线1508。在网络化环境中，相对 于计算机1502所描述的程序模块或其部分可以存储在远程存储器/存储设备 1550中。应该理解，所示网络连接是示例性的，并且可以使用在计算机之间建 立通信链路的其它手段。

计算机1502可用于与操作上设置在无线通信中的任何无线设备或实体通 信，这些设备或实体例如有打印机、扫描仪、台式和/或便携式计算机、便携式 数据助理、通信卫星、与无线可检测标签相关联的任何一个设备或位置(例如， 公用电话亭、报亭、休息室)以及电话。这至少包括Wi-Fi和蓝牙TM无线技术。 由此，通信可以如对于常规网络那样是预定义结构，或者仅仅是至少两个设备 之间的自组织(ad hoc)通信。

现在参考图16，示出了可利用根据所公开的本发明的并行化的解算机处 理的示例性计算环境1600的示意性框图。系统1600包括一个或多个客户机 1602。客户机1602可以是硬件和/或软件(例如，线程、进程、计算设备)。 客户机1602可例如使用通过本发明而容纳cookie和/或相关联的上下文信息。

系统1600还包括一个或多个服务器1604。服务器1604也可以是硬件和/ 或软件(例如，线程、进程、计算设备)。服务器1604可以例如通过使用本 体系结构来容纳线程以执行变换。在客户机1602和服务器1604之间的一种可 能的通信能够以适合在支持并行化的解算机状态处理的两个或多个计算机进 程之间传输的数据分组的形式进行。数据分组可包括例如cookie和/或相关联 的上下文信息。系统1600包括可以用来使客户机1606和服务器1602之间通 信更容易的通信框架1604(例如，诸如因特网等全球通信网络)。

通信可经由有线(包括光纤)和/或无线技术来促进。客户机1602操作上 被连接到可以用来存储对客户机1602本地的信息(例如，cookie和/或相关联 的上下文信息)的一个或多个客户机数据存储1608。同样地，服务器1604可 在操作上连接到可以用来存储对服务器1604本地的信息的一个或多个服务器 数据存储1610。

上面描述的包括所公开的本发明的各示例。当然，描述每一个可以想到的 组件和/或方法的组合是不可能的，但本领域内的普通技术人员应该认识到，许 多其它组合和排列都是可能的。因此，本发明旨在涵盖所有这些落入所附权利 要求书的精神和范围内的更改、修改和变化。此外，就在说明书或权利要求书 中使用术语“包括”而言，这一术语旨在以与术语“包含”在被用作权利要求 书中的过渡词时所解释的相似的方式为包含性的。