In this paper, we propose an OBDD-based algorithm called greedy clique decomposition, which is a new variable grouping heuristic method, to solve difficult SAT problems. We implement our algorithm and compare it with several state-of-art SAT solvers including Minisat, Ebddres and TTS. We show that with this new heuristic method, our implementation of an OBDD-based satisfiability solver can perform better for selected difficult SAT problems, whose conflict graphs possess a clique-like structure. © 2012 Springer-Verlag.
CITATION STYLE
Xu, Y., Chen, W., Su, K., & Zhang, W. (2012). Solving difficult SAT problems by using obdds and greedy clique decomposition. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7285 LNCS, pp. 259–268). https://doi.org/10.1007/978-3-642-29700-7_24
Mendeley helps you to discover research relevant for your work.