Parallel propositional satisfiability checking with distributed dynamic learning

被引：32

作者：

Blochinger, W ^{[1
]}

Sinz, C ^{[1
]}

Küchlin, W ^{[1
]}

机构：

[1] Univ Tubingen, Wilhelm Schickard Inst, Symbol Computat Grp, D-72076 Tubingen, Germany

来源：

PARALLEL COMPUTING | 2003年 / 29卷 / 07期

关键词：

parallel symbolic computation; parallel propositional satisfiability checking; distributed multithreading;

D O I：

10.1016/S0167-8191(03)00068-1

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：969 / 994

页数：26

共 36 条

[1]

Antoniu G, 2001, LECT NOTES COMPUT SC, V2026, P55

[2]

BAL HE, 1989, COMPUT SURV, V21, P261, DOI 10.1145/72551.72552

[3]

BIERE A, 1999, LECT NOTES COMPUTER, V1579

[4]

Blochinger W, 2000, PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED PROCESSING TECHNIQUES AND APPLICATIONS, VOLS I-V, P1627

[5] An object-oriented platform for distributed high-performance symbolic computation [J].

Blochinger, W ;

Küchlin, W ;

Ludwig, C ;

Weber, A .

MATHEMATICS AND COMPUTERS IN SIMULATION, 1999, 49 (03) :161-178

[6]

BLOCHINGER W, 2001, P INT PAR DISTR PROC, P90

[7]

BLUMOFE RD, 1994, AN S FDN CO, P356

[8]

BOEHM M, 1996, ANN MATH ARTIFICIAL, V17, P381

[9]

BRIAT J, 1997, P EUR 97 C PASS GERM, P590

[10] Solving large-scale QAP problems in parallel with the search library ZRAM [J].

Brungger, A ;

Marzetta, A ;

Clausen, J ;

Perregaard, M .

JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING, 1998, 50 (1-2) :157-169

← 1 2 3 4 →