Cache Performance of SAT Solvers: a Case Study for Efficient Implementation of Algorithms
作者： Lintao Zhang , Sharad Malik
DOI: 10.1007/978-3-540-24605-3_22
关键词:
摘要: We experimentally evaluate the cache performance of different SAT solvers as a case study for efficient implementation algorithms. several Boolean Constraint Propagation (BCP) mechanisms and show their respective run time performances on selected benchmark instances. From experiments we conclude that friendly data structure is key element in solvers. also empirical miss rates modern based Davis-Logemann-Loveland (DLL) algorithm with learning non-chronological backtracking. recently developed are much more structures implementations compared predecessors.
springer.com
sci-hub.st 参考文章(20)
Chu Min Li, Anbulagan Anbulagan, Heuristics based on unit propagation for satisfiability problems international joint conference on artificial intelligence. pp. 366- 371 ,(1997)
Hantao Zhang, SATO: An Efficient Propositional Prover conference on automated deduction. pp. 272- 275 ,(1997) , 10.1007/3-540-63104-6_28
Per Bjesse, Tim Leonard, Abdel Mokkedem, Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers computer aided verification. pp. 454- 464 ,(2001) , 10.1007/3-540-44585-4_44
Larry D. Auton, James M. Crawford, Experimental results on the crossover point in satisfiability problems national conference on artificial intelligence. pp. 21- 27 ,(1993)
Bart Selman, Henry Kautz, Planning as satisfiability european conference on artificial intelligence. pp. 359- 363 ,(1992)
Armin Biere, Alessandro Cimatti, Edmund Clarke, Yunshan Zhu, Symbolic Model Checking without BDDs tools and algorithms for construction and analysis of systems. pp. 193- 207 ,(1999) , 10.1007/3-540-49059-0_14
Li Xiao, Xiaodong Zhang, Stefan A. Kubricht, Improving memory performance of sorting algorithms ACM Journal of Experimental Algorithms. ,vol. 5, pp. 3- ,(2000) , 10.1145/351827.384245
Anthony LaMarca, Richard Ladner, The influence of caches on the performance of heaps ACM Journal of Experimental Algorithmics. ,vol. 1, pp. 4- ,(1996) , 10.1145/235141.235145
Miroslav N Velev, Randal E Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors Journal of Symbolic Computation. ,vol. 35, pp. 73- 106 ,(2003) , 10.1016/S0747-7171(02)00091-3
David Eppstein, Fast hierarchical clustering and other applications of dynamic closest pairs ACM Journal of Experimental Algorithms. ,vol. 5, pp. 1- ,(2000) , 10.1145/351827.351829