Parallel propositional satisfiability checking with distributed dynamic learning
Parallel propositional satisfiability checking with distributed dynamic learning
复制标题
DOI：
10.1016/s0167-8191(03)00068-1
复制
发表时间：
2003-07-01
影响因子：
1.4
通讯作者：
Küchlin, W
中科院分区：
文献类型：
--
作者：
Blochinger, W;Sinz, C;Küchlin, W
我们从符号计算领域解决了一种算法的并行化和分布式执行：带动态学习的命题可满足性(SAT)检验。我们的并行编程模型是针对核心SAT考试过程的严格多线程，并辅之以实现分布式动态学习过程的移动代理。单个线程处理动态创建的子问题，而移动代理收集和分发在学习过程中获得的相关知识。该并行算法运行在我们的并行系统平台分布式面向对象线程系统之上，为我们在高度异构性的分布式系统中的并行编程模型提供了支持。我们给出了性能测量，评估了我们的方法在不同应用领域的性能收益，具有实际意义。(C)2003 Elsevier Science B.V.保留所有权利。
We address the parallelization and distributed execution of an algorithm from the area of symbolic computation: propositional satisfiability (SAT) checking with dynamic learning. Our parallel programming models are strict multithreading for the core SAT checking procedure, complemented by mobile agents realizing a distributed dynamic learning process. Individual threads treat dynamically created subproblems, while mobile agents collect and distribute pertinent knowledge obtained during the learning process. The parallel algorithm runs on top of our parallel system platform Distributed Object-Oriented Threads System, which provides support for our parallel programming models in highly heterogeneous distributed systems. We present performance measurements evaluating the performance gains by our approach in different application domains with practical significance. (C) 2003 Elsevier Science B.V. All rights reserved.