Abstract
This paper considers the Diverse k Set problem in SAT, that is, the problem of efficiently generating a number of diverse solutions (satisfying assignments) given a propositional formula. We provide an extensive analysis of existing algorithms for this problem in a newly developed framework and propose new algorithms. While existing algorithms adapt modern SAT solvers to solve Diverse k Set by changing their polarity selection heuristic, our new algorithms adapt the variable ordering strategy as well. Our experimental results demonstrate that the proposed algorithms improve the diversification quality of the solutions on large industrial instances of Diverse k Set arising in SAT-based semiformal verification of hardware.
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
Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)
Agbaria, S., Carmi, D., Cohen, O., Korchemny, D., Lifshits, M., Nadel, A.: SAT-based semiformal verification of hardware. In: Bloem, R., Sharygina, N. (eds.) Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010), pp. 25–32 (October 2010)
Hebrard, E., Hnich, B., O’Sullivan, B., Walsh, T.: Finding diverse and similar solutions in constraint programming. In: Veloso, M.M., Kambhampati, S. (eds.) AAAI, pp. 372–377. AAAI Press / The MIT Press (2005)
Schreiber, Y.: Value-ordering heuristics: Search performance vs. Solution diversity. In: Cohen, D. (ed.) CP 2010. LNCS, vol. 6308, pp. 429–444. Springer, Heidelberg (2010)
Dechter, R., Kask, K., Bin, E., Emek, R.: Generating random solutions for constraint satisfaction problems. In: AAAI/IAAI, pp. 15–21 (2002)
Kitchen, N., Kuehlmann, A.: Stimulus generation for constrained random simulation. In: ICCAD, pp. 258–265 (2007)
Gomes, C.P., Sabharwal, A., Selman, B.: Near-uniform sampling of combinatorial spaces using XOR constraints. In: Schölkopf, B., Platt, J.C., Hoffman, T. (eds.) NIPS, pp. 481–488 (2006)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: DAC, pp. 530–535. ACM, New York (2001)
Silva, J.P.M., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers 48, 506–521 (1999)
Huang, J.: The effect of restarts on the efficiency of clause learning. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence, pp. 2318–2323 (2007)
Dershowitz, N., Hanna, Z., Nadel, A.: A clause-based heuristic for SAT solvers. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 46–60. Springer, Heidelberg (2005)
Frost, D., Dechter, R.: In search of the best constraint satisfaction search. In: AAAI, pp. 301–306 (1994)
Strichman, O.: Tuning SAT checkers for bounded model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 480–494. Springer, Heidelberg (2000)
Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 294–299. Springer, Heidelberg (2007)
Nadel, A.: Generating diverse solutions in SAT: Paper addendum (2011), http://www.cs.tau.ac.il/research/alexander.nadel/multiple_cex_addendum.pdf
Heule, M., van Maaren, H.: Look-ahead based SAT solvers [1], pp. 155–184
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nadel, A. (2011). Generating Diverse Solutions in SAT. In: Sakallah, K.A., Simon, L. (eds) Theory and Applications of Satisfiability Testing - SAT 2011. SAT 2011. Lecture Notes in Computer Science, vol 6695. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21581-0_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-21581-0_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21580-3
Online ISBN: 978-3-642-21581-0
eBook Packages: Computer ScienceComputer Science (R0)