Picoso - A Parallel Interval Constraint Solver.
作者： Natalia Kalinnik , Tobias Schubert , Erika Ábrahám , Ralf Wimmer , Bernd Becker
DOI:
关键词:
摘要: This paper describes the parallel interval constraint solver Picoso, which can decide (a subclass of) boolean combinations of linear and non-linear constraints. Picoso follows a master/client model based on message passing, making it suitable for any kind workstation cluster as well multi-processor machines. To run several clients in parallel, an efficient work stealing mechanism has been integrated, dividing overall search space into disjoint parts. Additionally, to prevent from running identical conflicts, information about conflicts form conflict clauses is exchanged among clients. Performance measurements, using four solve number benchmark problems, show that yields (almost) speedup compared sequential iSAT, are based.
参考文章(17)
Frédéric Benhamou, Laurent Granvilliers, Continuous and Interval Constraints Handbook of Constraint Programming. ,vol. 2, pp. 571- 603 ,(2006) , 10.1016/S1574-6526(06)80020-9
Edmund Clarke, Armin Biere, Richard Raimi, Yunshan Zhu, Bounded Model Checking Using Satisfiability Solving formal methods. ,vol. 19, pp. 7- 34 ,(2001) , 10.1023/A:1011276507260
Bernard Jurkowiak, Chu Min Li, Gil Utard, Parallelizing Satz Using Dynamic Workload Balancing Electronic Notes in Discrete Mathematics. ,vol. 9, pp. 174- 189 ,(2001) , 10.1016/S1571-0653(04)00321-X
Matthew Lewis, Tobias Schubert, Bernd Becker, Multithreaded SAT Solving asia and south pacific design automation conference. pp. 926- 931 ,(2007) , 10.1109/ASPDAC.2007.358108
Max Böhm, Ewald Speckenmeyer, A fast parallel SAT-solver — efficient workload balancing Annals of Mathematics and Artificial Intelligence. ,vol. 17, pp. 381- 400 ,(1996) , 10.1007/BF02127976
Donald Loveland, George Logemann, Martin Davis, A machine program for theorem-proving ,(2011)
William Gropp, Ewing Lusk, Nathan Doss, Anthony Skjellum, A high-performance, portable implementation of the MPI message passing interface standard parallel computing. ,vol. 22, pp. 789- 828 ,(1996) , 10.1016/0167-8191(96)00024-5
Martin Fränzle, Christian Herde, HySAT: An efficient proof engine for bounded model checking of hybrid systems formal methods. ,vol. 30, pp. 179- 198 ,(2007) , 10.1007/S10703-006-0031-0
HANTAO ZHANG, MARIA PAOLA BONACINA, JIEH HSIANG, PSATO: a distributed propositional prover and its application to quasigroup problems parallel symbolic computation. ,vol. 21, pp. 543- 560 ,(1996) , 10.1006/JSCO.1996.0030
Gilles Audemard, Marco Bozzano, Alessandro Cimatti, Roberto Sebastiani, Verifying Industrial Hybrid Systems with MathSAT Electronic Notes in Theoretical Computer Science. ,vol. 119, pp. 17- 32 ,(2005) , 10.1016/J.ENTCS.2004.12.022