Picoso - A Parallel Interval Constraint Solver.
Natalia Kalinnik, Tobias Schubert, Erika Ábrahám, Ralf Wimmer, Bernd Becker · RWTH Publications (RWTH Aachen) · 2009
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 of workstation cluster as well as for multi-processor machines. To run several clients in parallel, an efficient work stealing mechanism has been integrated, dividing the overall search space into disjoint parts. Additionally, to prevent the clients from running into identical conflicts, information about conflicts in form of conflict clauses is exchanged among the clients. Performance measurements, using four clients to solve a number of benchmark problems, show that Picoso yields (almost) linear speedup compared to the sequential interval constraint solver iSAT, on which the clients of Picoso are based.