×

Simulating circuit-level simplifications on CNF. (English) Zbl 1267.94144

Summary: Boolean satisfiability (SAT) and its extensions have become a core technology in many application domains, such as planning and formal verification, and continue finding various new application domains today. The SAT-based approach divides into three steps: encoding, preprocessing, and search. It is often argued that by encoding arbitrary Boolean formulas in conjunctive normal form (CNF), structural properties of the original problem are not reflected in the CNF. This should result in the fact that CNF-level preprocessing and SAT solver techniques have an inherent disadvantage compared to related techniques applicable on the level of more structural SAT instance representations such as Boolean circuits. Motivated by this, various simplification techniques and intricate CNF encodings for circuit-level SAT instance representations have been proposed. On the other hand, based on the highly efficient CNF-level clause learning SAT solvers, there is also strong support for the claim that CNF is sufficient as an input format for SAT solvers. In this work we study the effect of CNF-level simplification techniques, focusing on SatElite-style variable elimination (VE) and what we call blocked clause elimination (BCE). We show that BCE is surprisingly effective both in theory and in practice on CNF formulas resulting from a standard CNF encoding for circuits: without explicit knowledge of the underlying circuit structure, it achieves the same level of simplification as a combination of circuit-level simplifications and previously suggested polarity-based CNF encodings. We also show that VE can achieve many of the same effects as BCE, but not all. On the other hand, it turns out that VE and BCE are indeed partially orthogonal techniques. We also study the practical effects of combining BCE and VE for reducing the size of formulas and on the running times of state-of-the-art SAT solvers. Furthermore, we address the problem of how to construct original witnesses to satisfiable CNF formulas when applying a combination of BCE and VE.

MSC:

94C10 Switching theory, application of Boolean algebra; Boolean functions (MSC2010)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Audemard, G., Katsirelos, G., Simon, L.: A restriction of extended resolution for clause learning SAT solvers. In: Fox, M., Poole, D. (eds.) Proceedings of the 24th AAAI Conference on Artificial Intelligence (AAAI 2010). AAAI Press (2010)
[2] Bacchus, F.: Enhancing Davis Putnam with extended binary clause reasoning. In: Proceedings of the 18th National Conference on Artificial Intelligence (AAAI 2002), pp. 613–619. AAAI Press (2002)
[3] Bacchus, F., Winter, J.: Effective preprocessing with hyper-resolution and equality reduction. In: Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT 2003). Lecture Notes in Computer Science, vol. 2919, pp. 341–355. Springer (2004) · Zbl 1204.68176
[4] Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., et al. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825–885. IOS Press
[5] Biere, A., Clarke, E.M., Raimi, R., Zhu, Y.: Verifiying safety properties of a power PC microprocessor using symbolic model checking without BDDs. In: Halbwachs, N., Peled, D., (eds.) Proceedings of the 11th International Conference on Computer Aided Verification (CAV 1999). Lecture Notes in Computer Science, vol. 1633, pp. 60–71. Springer (1999) · Zbl 1046.68578
[6] Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009) · Zbl 1183.68568
[7] Biere, A., Lonsing, F., Seidl, M.: Quantified blocked clause elimination. In: Proceedings of the 23nd International Conference on Automated Deduction (CADE-23). Lecture Notes in Computer Science. Springer (2011) · Zbl 1341.68181
[8] Boy de la Tour, T.: An optimality result for clause form translation. J. Symb. Comput. 14(4), 283–302 (1992) · Zbl 0772.68079 · doi:10.1016/0747-7171(92)90009-S
[9] Brafman, R.I.: A simplifier for propositional formulas with many binary clauses. IEEE Trans. Syst. Man Cybern., Part B 34(1), 52–59 (2004) · doi:10.1109/TSMCB.2002.805807
[10] Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009). Lecture Notes in Computer Science, vol. 5505, pp. 174–177. Springer (2009)
[11] Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT solver. In: Gupta, A., Malik, S. (eds.) Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008). Lecture Notes in Computer Science, vol. 5123, pp. 299–303. Springer (2008)
[12] Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT solver. In: Esparza, J., Majumdar, R. (eds.) Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2010). Lecture Notes in Computer Science, vol. 6015, pp. 150–153. Springer (2010)
[13] Chambers, B., Manolios, P., Vroon, D.: Faster SAT solving with better CNF generation. In: Proceedings of Design, Automation and Test in Europe (DATE 2009), pp. 1590–1595. IEEE (2009)
[14] Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960) · Zbl 0212.34203 · doi:10.1145/321033.321034
[15] de Moura, L.M., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008). Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer (2008)
[16] Drechsler, R., Junttila, T., Niemelä, I.: Non-clausal SAT and ATPG. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, chap. 21, pp. 655–694. IOS Press (2009)
[17] Dunham, B., Fridshal, R., Sward, G.: A heuristic program for proving elementary logical theorems. In: Proceedings of the International Conference on Information Processing (IFIP 1959), pp. 282–284 (1959) · Zbl 0115.35206
[18] Dunham, B., Wang, H.: Towards feasible solutions of the tautology problem. Ann. Math. Logic 10, 117–154 (1976) · Zbl 0349.02006 · doi:10.1016/0003-4843(76)90020-6
[19] Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) Proceedings of 8th International Conference on Theory and Applications of Satisfiability Testing (SAT 2005). Lecture Notes in Computer Science, vol. 3569, pp. 61–75. Springer (2005) · Zbl 1128.68463
[20] Eén, N., Mishchenko, A., Sörensson, N.: Applying logic synthesis for speeding up SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007). Lecture Notes in Computer Science, vol. 4501, pp. 272–286. Springer (2007) · Zbl 1214.68351
[21] Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007). Lecture Notes in Computer Science, vol. 4590, pp. 519–531. Springer (2007) · Zbl 1135.68472
[22] Gershman, R., Strichman, O.: Cost-effective hyper-resolution for preprocessing CNF formulas. In: Bacchus, F., Walsh, T. (eds.) Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT 2005). Lecture Notes in Computer Science, vol. 3569, pp. 423–429. Springer (2005) · Zbl 1128.68465
[23] Han, H., Somenzi, F.: Alembic: an efficient algorithm for CNF preprocessing. In: Proceedings of the 44rd Design Automation Conference (DAC 2007), pp. 582–587 (2007)
[24] Han, H., Somenzi, F.: On-the-fly clause improvement. In: Kullmann, O. (ed.) SAT. Lecture Notes in Computer Science, vol. 5584, pp. 209–222. Springer (2009)
[25] Heule, M.J.H., van Maaren, H.: Aligning CNF- and equivalence-reasoning. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2005 Selected Revised Papers. Lecture Notes in Computer Science, vol. 3542, pp. 145–156. Springer (2005) · Zbl 1122.68600
[26] Heule, M.J.H., Verwer, S.: Exact DFA identification using SAT solvers. In: Sempere, J.M., García, P. (eds.) Proceedings of the 10th International Colloquium on Grammatical Inference: Theoretical Results and Applications (ICGI 2010). Lecture Notes in Computer Science, vol. 6339, pp. 66–79 (2010) · Zbl 1291.68192
[27] Huang, J.: Extended clause learning. Artif. Intell. 174(15), 1277–1284 (2010) · Zbl 1210.68082 · doi:10.1016/j.artint.2010.07.008
[28] Jackson, P., Sheridan, D.: Clause form conversions for Boolean circuits. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004 Selected Revised Papers. Lecture Notes in Computer Science, vol. 3542, pp. 183–198. Springer (2005) · Zbl 1122.68603
[29] Järvisalo, M., Biere, A.: Reconstructing solutions after blocked clause elimination. In: Strichman, O., Szeider, S. (eds.) Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010). Lecture Notes in Computer Science, vol. 6175, pp. 340–345. Springer (2010) · Zbl 1306.68159
[30] Järvisalo, M., Biere, A., Heule, M.J.H.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2010). Lecture Notes in Computer Science, vol. 6015, pp. 129–144. Springer (2010) · Zbl 1284.03208
[31] Jha, S., Limaye, R., Seshia, S.A.: Beaver: Engineering an efficient SMT solver for bit-vector arithmetic. In: Bouajjani, A., Maler, O. (eds.) Proceedings of the 21st International Conference on Computer Aided Verification (CAV 2009). Lecture Notes in Computer Science, vol. 5643, pp. 668–674. Springer (2009)
[32] Jin, H., Somenzi, F.: An incremental algorithm to check satisfiability for bounded model checking. Electronic Notes in Theoretical Computer Science 119(2), 51–65 (2005) · doi:10.1016/j.entcs.2004.06.062
[33] Jussila, T., Biere, A.: Compressing BMC encodings with QBF. Electronic Notes in Theoretical Computer Science 174(3), 45–56 (2007) · doi:10.1016/j.entcs.2006.12.022
[34] Kautz, H.A., Ruan, Y., Achlioptas, D., Gomes, C.P., Selman, B., Stickel, M.E.: Balance and filtering in structured satisfiable problems. In: Nebel, B. (ed.) Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI 2001), pp. 351–358. Morgan Kaufmann (2001) · Zbl 0985.90509
[35] Kullmann, O.: New methods for 3-SAT decision and worst-case analysis. Theor. Comp. Sci. 223(1–2), 1–72 (1999) · Zbl 0930.68066 · doi:10.1016/S0304-3975(98)00017-6
[36] Kullmann, O.: On a generalization of extended resolution. Discrete Appl. Math. 96–97, 149–176 (1999) · Zbl 0941.68126 · doi:10.1016/S0166-218X(99)00037-2
[37] Le Berre, D.: Exploiting the real power of unit propagation lookahead. Electronic Notes in Discrete Mathematics 9, 59–80 (2001) · Zbl 0990.90538 · doi:10.1016/S1571-0653(04)00314-2
[38] Li, C.M., Wei, W., Zhang, H.: Combining adaptive noise and look-ahead in local search for SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007). Lecture Notes in Computer Science, pp. 121–133. Springer (2007) · Zbl 1214.68362
[39] Lynce, I., Marques-Silva, J.: The interaction between simplification and search in propositional satisfiability. In: CP’01 Workshop on Modeling and Problem Formulation (2001) · Zbl 1067.68650
[40] Manolios, P., Vroon, D.: Efficient circuit to CNF conversion. In: Marques-Silva, J., Sakallah, K.A. (eds.) Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007). Lecture Notes in Computer Science, vol. 4501, pp. 4–9. Springer (2007)
[41] Mishchenko, A., Chatterjee, S., Brayton, R.K.: DAG-aware AIG rewriting: a fresh look at combinational logic synthesis. In: Sentovich, E. (ed.) Proceedings of the 43rd Design Automation Conference (DAC 2006), pp. 532–535. ACM (2006)
[42] Ostrowski, R., Grégoire, É., Mazure, B., Sais, L.: Recovering and exploiting structural knowledge from CNF formulas. In: Hentenryck, P.V. (ed.) Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming (CP 2002). Lecture Notes in Computer Science, vol. 2470, pp. 185–199. Springer (2002)
[43] Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2(3), 293–304 (1986) · Zbl 0636.68119 · doi:10.1016/S0747-7171(86)80028-1
[44] Purdom, P.W.: Solving satisfiability with less searching. IEEE Trans. Pattern Anal. Mach. Intell. 6(4), 510–513 (1984) · Zbl 0545.68052 · doi:10.1109/TPAMI.1984.4767555
[45] Subbarayan, S., Pradhan, D.K.: NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004 Selected Revised Papers. Lecture Notes in Computer Science, vol. 3542, pp. 276–291. Springer (2005) · Zbl 1122.68618
[46] Tompkins, D.A., Hoos, H.H.: UBCSAT: an implementation and experimentation environment for SLS algorithms for SAT & MAX-SAT. In: Online Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT 2004) (2004) · Zbl 1122.68620
[47] Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning 2: Classical Papers on Computational Logic 1967–1970, pp. 466–483. Springer (1983)
[48] Van Gelder, A.: Toward leaner binary-clause reasoning in a satisfiability solver. Ann. Math. Artif. Intell. 43(1), 239–253 (2005) · Zbl 1099.68097
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.