×

Recognition of nested gates in CNF formulas. (English) Zbl 1471.68246

Heule, Marijn (ed.) et al., Theory and applications of satisfiability testing – SAT 2015. 18th international conference, Austin, TX, USA, September 24–27, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9340, 255-271 (2015).
Summary: We present a new algorithm to efficiently extract information about nested functional dependencies between variables of a formula in CNF. Our algorithm uses the relation between gate encodings and blocked sets in CNF formulas. Our notion of “gate” emphasizes this relation. The presented algorithm is central to our new tool, cnf2aig, that produces equisatisfiable and-inverter-graphs (AIGs) from CNF formulas. We compare the novel algorithm to earlier approaches and show that the produced AIG are generally more succinct and use less input variables. As the gate-detection is related to the structure of input formulas, we furthermore analyze the gate-detection before and after applying preprocessing techniques.
For the entire collection see [Zbl 1323.68009].

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Balint, A., Manthey, N.: Boosting the performance of SLS and CDCL solvers by preprocessor tuning. In: Berre, D.L. (ed.) POS 2013. EPiC Series, vol. 29, pp. 1–14. EasyChair (2014)
[2] Balyo, T., Fröhlich, A., Heule, M.J.H., Biere, A.: Everything you always wanted to know about blocked sets (but were afraid to ask). In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 317–332. Springer, Heidelberg (2014) · Zbl 1423.68435 · doi:10.1007/978-3-319-09284-3_24
[3] Biere, A., Le Berre, D., Lonca, E., Manthey, N.: Detecting cardinality constraints in CNF. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 285–301. Springer, Heidelberg (2014). http://dx.doi.org/10.1007/978-3-319-09284-3_22 · Zbl 1423.68437 · doi:10.1007/978-3-319-09284-3_22
[4] Bjesse, P., Kukula, J.H., 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) · Zbl 1204.68104 · doi:10.1007/978-3-540-24605-3_24
[5] Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003) · Zbl 1325.68145 · doi:10.1145/876638.876643
[6] Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7(3), 201–215 (1960). http://doi.acm.org/10.1145/321033.321034 · Zbl 0212.34203 · doi:10.1145/321033.321034
[7] Dixon, H.E., Ginsberg, M.L., Luks, E.M., Parkes, A.J.: Generalizing Boolean satisfiability II: Theory (2011). CoRR abs/1109.2134 · Zbl 1080.68660
[8] Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005). http://dx.doi.org/10.1007/11499107_5 · Zbl 1128.68463 · doi:10.1007/11499107_5
[9] Falke, S., Merz, F., Sinz, C.: LLBMC: improved bounded model checking of C programs using LLVM (competition contribution). In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 623–626. Springer, Heidelberg (2013) · Zbl 06194869 · doi:10.1007/978-3-642-36742-7_48
[10] Fu, Z., Malik, S.: Extracting logic circuit structure from conjunctive normal form descriptions. In: 20th International Conference on VLSI Design (VLSI Design 2007), Sixth International Conference on Embedded Systems (ICES 2007), January 6–10, 2007, Bangalore, India. pp. 37–42 (2007) · doi:10.1109/VLSID.2007.81
[11] Fu, Z., Yu, Y., Malik, S.: Considering circuit observability don’t cares in CNF satisfiability. In: 2005 Design, Automation and Test in Europe Conference and Exposition (DATE 2005), March 7–11, 2005, Munich, Germany, pp. 1108–1113 (2005)
[12] Heule, M.J.H., Biere, A.: Blocked clause decomposition. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 423–438. Springer, Heidelberg (2013). http://dx.doi.org/10.1007/978-3-642-45221-5_29 · Zbl 1407.68451 · doi:10.1007/978-3-642-45221-5_29
[13] Iser, M., Sinz, C., Taghdiri, M.: Minimizing models for tseitin-encoded SAT instances. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 224–232. Springer, Heidelberg (2013) · Zbl 1390.68574 · doi:10.1007/978-3-642-39071-5_17
[14] Iser, M., Taghdiri, M., Sinz, C.: Optimizing MiniSAT variable orderings for the relational model finder kodkod (poster presentation). In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 483–484. Springer, Heidelberg (2012) · doi:10.1007/978-3-642-31612-8_46
[15] Järvisalo, M., Biere, A., Heule, M.J.H.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 129–144. Springer, Heidelberg (2010) · Zbl 1284.03208 · doi:10.1007/978-3-642-12002-2_10
[16] Järvisalo, M., Biere, A., Heule, M.J.H.: Simulating circuit-level simplifications on cnf. Journal of Automated Reasoning 49(4), 583–619 (2012) · Zbl 1267.94144 · doi:10.1007/s10817-011-9239-9
[17] Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property verification. IEEE Trans. on CAD of Integrated Circuits and Systems 21(12), 1377–1394 (2002) · Zbl 05448668 · doi:10.1109/TCAD.2002.804386
[18] Manthey, N.: Coprocessor 2.0 – a flexible CNF simplifier. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 436–441. Springer, Heidelberg (2012). http://dx.doi.org/10.1007/978-3-642-31612-8_34 · Zbl 06197773 · doi:10.1007/978-3-642-31612-8_34
[19] Manthey, N.: Extended resolution in modern SAT solving. In: Joint Automated Reasoning Workshop and Deduktionstreffen (2014)
[20] Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of boolean formulas. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC. LNCS, vol. 7857, pp. 102–117. Springer, Heidelberg (2013). http://dx.doi.org/10.1007/978-3-642-39611-3_14 · Zbl 06232564 · doi:10.1007/978-3-642-39611-3_14
[21] Mihal, A., Teig, S.: A constraint satisfaction approach for programmable logic detailed placement. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 208–223. Springer, Heidelberg (2013) · Zbl 1390.68604 · doi:10.1007/978-3-642-39071-5_16
[22] Grégoire, R.O.É., Saïs, L.: Recovering and exploiting structural knowledge from CNF formulas. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, p. 185. Springer, Heidelberg (2002)
[23] 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
[24] Rintanen, J.: Engineering efficient planners with SAT. In: ECAI, pp. 684–689 (2012)
[25] Sinz, C.: Visualizing SAT instances and runs of the DPLL algorithm. J. Autom. Reasoning 39(2), 219–243 (2007) · Zbl 1129.68502 · doi:10.1007/s10817-007-9074-1
[26] Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007) · Zbl 1186.68304 · doi:10.1007/978-3-540-71209-1_49
[27] Boy de la Tour, T.: An optimality result for clause form translation. J. Symb. Comput. 14(4), 283–301 (1992) · Zbl 0772.68079 · doi:10.1016/0747-7171(92)90009-S
[28] Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, pp. 115–125 (1970) · doi:10.1007/978-1-4899-5327-8_25
[29] Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: IJCAI, pp. 1173–1178 (2003)
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.