\input zb-basic
\input zb-ioport
\iteman{io-port 06057340}
\itemau{Xu, Yanyan; Chen, Wei; Su, Kaile; Zhang, Wenhui}
\itemti{Solving difficult SAT problems by using OBDDs and greedy clique decomposition.}
\itemso{Snoeyink, Jack (ed.) et al., Frontiers in algorithmics and algorithmic aspects in information and management. Joint international conference, FAW-AAIM 2012, Beijing, China, May 14--16, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-29699-4/pbk). Lecture Notes in Computer Science 7285, 259-268 (2012).}
\itemab
Summary: 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.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.1007/978-3-642-29700-7\_24}
\end