Sharing Information in Parallel Search with Search Space Partitioning
In this paper we propose a new approach to share information among the computation units of an iterative search partitioning parallel SAT solver by approximating validity. Experimental results show the streh of the approach, against both existing sharing
- PDF / 211,163 Bytes
- 7 Pages / 439.37 x 666.142 pts Page_size
- 10 Downloads / 216 Views
Abstract. In this paper we propose a new approach to share information among the computation units of an iterative search partitioning parallel SAT solver by approximating validity. Experimental results show the streh of the approach, against both existing sharing techniques and absence of sharing. With the improved clause sharing, out of 600 instances we could solve 13 more than previous sharing techniques.
1
Introduction
Search problems arise from various domains, ranging from small logic puzzles over scheduling problems like railway scheduling [1], to large job shop scheduling problems [2]. As long as the answers need not to be optimal, these problems can be translated into a constraint satisfaction problem [3], or into satisfiability testing (SAT) [4]. SAT approach is often successful, e.g. scheduling railway trains has been improved by a speedup up to 10000 compared to the state-of-the-art domain specific solver [1]. With the advent of parallel architectures, the interest moved towards parallel SAT solvers [5–7]. Most relevant parallel SAT solvers can be divided in two families: portfolio solvers, where several sequential solvers compete each other over the same formula, and iterative partitioning, where each solver is assigned a partition of the original problem and partitions are created iteratively. Portfolio solvers received much attention from the community, leading to enhancements by means of sharing according to some filter heuristics [5], or by controlling the diversification and intensification among the solvers [8]. The same cannot be said for iterative partitioning: for a grid implementation of the parallel solver, only a study on how to divide the search space [9] and on limited sharing has been done [10]. As for portfolio solvers [5,11], Hyv¨ arinen et.al report that in average even this limited sharing results in a speedup. In this paper we present an improved clause sharing mechanism for the iterative partitioning approach. Our evaluation reveals interesting insights: first, sharing clauses introduces almost no overhead in computation. Furthermore, the performance of the overall search is increased. One of the reasons for this improved behavior is that the number Davide Lanti was supported by the European Master’s Program in Computational Logic (EMCL). G. Nicosia and P. Pardalos (Eds.): LION 7, LNCS 7997, pp. 52–58, 2013. c Springer-Verlag Berlin Heidelberg 2013 DOI: 10.1007/978-3-642-44973-4 6,
Sharing Information in Parallel Search
53
of shared clauses increases, strengthening the cooperation among the parallel running solvers. Finally, the approach scales with more cores, that is crucial as increasingly parallel architectures become available. After giving some preliminaries on SAT solving in Sect. 2, we present our new clause sharing approach in Sect. 3. An empirical evaluation is performed in Sect. 4, and finally we draw conclusions in Sect. 5.
2
Preliminaries
Let V be a finite set of Boolean variables. The set of literals V ∪ {x | x ∈ V } consists of positive and negative Boolean variab
Data Loading...
