Abstract
This paper presents a new technique to derive an initial static variable ordering for efficient SAT search. Our approach not only exploits variable activity and connectivity information simultaneously, but it also analyzes how tightly the variables are related to each other. For this purpose, a new metric is proposed – the degree of correlation among pairs of variables. Variable activity and correlation information is modeled (implicitly) as a weighted graph. A topological analysis of this graph generates an order for SAT search. Also, the effect of decision-assignments on clause-variable dependencies is taken into account during this analysis. An algorithm called ACCORD (ACtivity – CORrelation – ORDering) is proposed for this purpose. Using efficient implementations of the above, experiments are conducted over a wide range of benchmarks. The results demonstrate that: (i) the variable order generated by our approach significantly improves the performance of SAT solvers; (ii) time to derive this order is a fraction of the overall solving time. As a result, our approach delivers faster performance as compared to contemporary approaches.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Silva, J.P.M.: The Impact of Branching Heuristics in Propositional Satisfiability Algorithms. In: Portuguese Conf. on Artificial Intelligence (1999)
Moskewicz, M., Madigan, C., Zhao, L., Malik, S.: CHAFF: Engineering and Efficient SAT Solver. In: Proc. Design Automation Conference, June 2001, pp. 530–535 (2001)
Goldberg, E., Novikov, Y.: BerkMin: A Fast and Robust Sat-Solver. In: DATE, pp. 142–149 (2002)
Marques-Silva, J., Sakallah, K.A.: GRASP - A New Search Algorithm for Satisfiability. In: ICCAD 1996, November 1996, pp. 220–227 (1996)
Dechter, R., Pearl, J.: Network-based Heuristics for Constraint-Satisfaction Problems. Artificial Intelligence 34, 1–38 (1987)
Amir, E., McIlraith, S.: Solving Satisfiability using Decomposition and the Most Constrained Subproblem. In: LICS workshop on Theory and Applications of Satisfiability Testing, SAT 2001 (2001)
Bjesse, P., Kukula, J., Damiano, R., Stanion, T., Zhu, Y.: Guiding SAT Diagnosis with Tree Decompositions. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 315–329. Springer, Heidelberg (2004)
Gupta, A., Yang, Z., Ashar, P., Zhang, L., Malik, S.: Partition-based Decision Heuristics for Image Computation using SAT and BDDs. In: Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design (ICCAD), pp. 286–292. IEEE Press, Los Alamitos (2001)
Aloul, F., Markov, I., Sakallah, K.: Mince: A static global variable-ordering for sat and bdd. In: International Workshop on Logic and Synthesis, University of Michigan (June 2001)
Huang, J., Darwiche, A.: A structure-based variable ordering heuristic for SAT. In: Proceedings of the 18th International Joint Conference on Artificial Intelligence (IJCAI), August 2003, pp. 1167–1172 (2003)
Aloul, F.A., Markov, I.L., Sakallah, K.A.: FORCE: A Fast and Easy-To-Implement Variable-Ordering Heuristic. In: Proceedings of the 13th ACM Great Lakes symposium on VLSI, pp. 116–119 (2003)
Durairaj, V., Kalla, P.: Guiding CNF-SAT Search via Efficient Constraint Partitioning. In: ICCAD, pp. 498–501 (2004)
Prim, R.C.: Shortest connection networks and some generalizations. The Bell System Technical Journal 36, 1389–1401 (1957)
Eén, N., Sörensson, N.: An Extensible SAT Solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Velev, M.: Sat benchmarks for high-level microprocessor validation, http://www.cs.cmu.edu/~mvelev
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Durairaj, V., Kalla, P. (2005). Variable Ordering for Efficient SAT Search by Analyzing Constraint-Variable Dependencies. In: Bacchus, F., Walsh, T. (eds) Theory and Applications of Satisfiability Testing. SAT 2005. Lecture Notes in Computer Science, vol 3569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11499107_33
Download citation
DOI: https://doi.org/10.1007/11499107_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26276-3
Online ISBN: 978-3-540-31679-4
eBook Packages: Computer ScienceComputer Science (R0)