Cited By
View all- Jarvis PArbelaez A(2020)Cooperative Parallel SAT Local Search with Path RelinkingEvolutionary Computation in Combinatorial Optimization10.1007/978-3-030-43680-3_6(83-98)Online publication date: 15-Apr-2020
From sequential to parallel local search for SAT
Pages 157 - 168
Abstract
In the domain of propositional Satisfiability Problem (SAT), parallel portfolio-based algorithms have become a standard methodology for both complete and incomplete solvers. In this methodology several algorithms explore the search space in parallel, either independently or cooperatively with some communication between the solvers. We conducted a study of the scalability of several SAT solvers in different application domains (crafted, verification, quasigroups and random instances) when drastically increasing the number of cores in the portfolio, up to 512 cores. Our experiments show that on different problem families the behaviors of different solvers vary greatly. We present an empirical study that suggests that the best sequential solver is not necessary the one with the overall best parallel speedup.
References
[1]
Cook, S. A.: The Complexity of Theorem-Proving Procedures. In: Third Annual ACM Symposium on Theory of Computing, STOC 1971, pp. 151-158. ACM (1971)
[2]
Chrabakh, W., Wolski, R.: GridSAT: A System for Solving Satisfiability Problems Using a Computational Grid. Parallel Computing 32(9), 660-687 (2006)
[3]
Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: A Parallel SAT Solver. Journal on Satisfiability, Boolean Modeling and Computation, JSAT 6(4), 245-262 (2009)
[4]
Arbelaez, A., Hamadi, Y.: Improving Parallel Local Search for SAT. In: Coello Coello, C. A. (ed.) LION 2011. LNCS, vol. 6683, pp. 46-60. Springer, Heidelberg (2011)
[5]
Hoos, H., Stützle, T.: Stochastic Local Search: Foundations & Applications. Morgan Kaufmann Publishers Inc., San Francisco (2004)
[6]
Selman, B., Kautz, H. A., Cohen, B.: Noise Strategies for Improving Local Search. In: AAAI 1994, vol. 1, pp. 337-343 (July 1994)
[7]
McAllester, D. A., Selman, B., Kautz, H. A.: Evidence for Invariants in Local Search. In: AAAI 1997, pp. 321-326 (1997)
[8]
Thornton, J., Pham, D. N., Bain, S., Ferreira Jr., V.: Additive versus Multiplicative Clause Weighting for SAT. In: AAAI 2004, pp. 191-196 (July 2004)
[9]
Prestwich, S. D.: Random Walk with Continuously Smoothed Variable Weights. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 203-215. Springer, Heidelberg (2005)
[10]
Li, C.-M., Huang, W. Q.: Diversification and Determinism in Local Search for Satisfiability. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 158-172. Springer, Heidelberg (2005)
[11]
Balint, A., Fröhlich, A.: Improving Stochastic Local Search for SAT with a New Probability Distribution. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 10-15. Springer, Heidelberg (2010)
[12]
Shylo, O. V., Middelkoop, T., Pardalos, P. M.: Restart Strategies in Optimization: Parallel and Serial Cases. Parallel Computing 37(1), 60-68 (2011)
[13]
Pham, D. N., Gretton, C.: gNovelty+. In: Solver Description, SAT Competition 2007 (2007)
[14]
Roli, A.: Criticality and Parallelism in Structured SAT Instances. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 714-719. Springer, Heidelberg (2002)
[15]
Kroc, L., Sabharwal, A., Gomes, C. P., Selman, B.: Integrating Systematic and Local Search Paradigms: A New Strategy for MaxSAT. In: IJCAI 2009, pp. 544-551 (July 2009)
[16]
Arbeleaz, A., Codognet, P.: Massivelly Parallel Local Search for SAT. In: ICTAI 2012, Athens, Greece, pp. 57-64. IEEE Computer Society (November 2012)
[17]
Martins, R., Manquinho, V., Lynce, I.: An Overview of Parallel SAT Solving. Constraints 17, 304-347 (2012)
[18]
Tompkins, D. A. D., Hoos, H. H.:UBCSAT: An Implementation and Experimentation Environment for SLS Algorithms for SAT and MAX-SAT. In: Hoos, H. H., Mitchell, D. G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 306-320. Springer, Heidelberg (2005)
[19]
Achlioptas, D., Gomes, C. P., Kautz, H. A., Selman, B.: Generating satisfiable problem instances. In: AAAI 2000, pp. 256-261 (July 2000)
[20]
Clarke, E., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168-176. Springer, Heidelberg (2004)
[21]
Tompkins, D. A. D., Balint, A., Hoos, H. H.: Captain Jack: New Variable Selection Heuristics in Local Search for SAT. In: Sakallah, K. A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 302-316. Springer, Heidelberg (2011)
[22]
Gent, I. P., Walsh, T.: The SAT Phase Transition. In: ECAI 1994, pp. 105-109 (August 1994)
Recommendations
Stochastic local search for incremental SAT
The boolean satisfiability problem (SAT) is stated as follows: given a boolean formula in CNF, find a truth assignment that satisfies its clauses. In this paper, we present a general framework based on stochastic local search and the structure of the ...
Approximating Max NAE-k-SAT by anonymous local search
A clause is not-all-equal satisfied if it has at least one literal assigned with true and one literal assigned with false. Max NAE-SAT is given by a boolean variable set U and a clause set C, asks to find an assignment of U, such that the number of not-...
Massively Parallel Local Search for SAT
ICTAI '12: Proceedings of the 2012 IEEE 24th International Conference on Tools with Artificial Intelligence - Volume 01Parallel portfolio-based algorithms have become a standard methodology for both complete and incomplete solvers for SAT solving. In this methodology several algorithms explore the search space in parallel, either independently or cooperatively with some ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sponsors
- VIENUT: Vienna University of Technology
- Edinburgh Napier University, UK: Edinburgh Napier University, UK
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 03 April 2013
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 18 Dec 2024
Other Metrics
Citations
Cited By
View all- Jarvis PArbelaez A(2020)Cooperative Parallel SAT Local Search with Path RelinkingEvolutionary Computation in Combinatorial Optimization10.1007/978-3-030-43680-3_6(83-98)Online publication date: 15-Apr-2020