×

zbMATH — the first resource for mathematics

On conversions from CNF to ANF. (English) Zbl 1432.68600
Summary: In this paper we discuss conversion methods from the conjunctive normal form (CNF) to the algebraic normal form (ANF) of a Boolean function. Whereas the reverse conversion has been studied before, the CNF to ANF conversion has been achieved predominantly via a standard method which tends to produce many polynomials of high degree. Based on a block-building mechanism, we design a new blockwise algorithm for the CNF to ANF conversion which is geared towards producing fewer and lower degree polynomials. In particular, we look for as many linear polynomials as possible in the converted system and check that our algorithm finds them. As an application, we suggest a new algebraic extension of the resolution calculus which is tailored to the output of the standard CNF to ANF conversion algorithm. Experiments show that the ANF produced by our algorithm outperforms the standard conversion in “real life” examples originating from cryptographic attacks, and that our algebraic resolution algorithm solves some SAT instances which are notoriously hard for SAT solvers.
MSC:
68W30 Symbolic computation and algebraic computation
06E30 Boolean functions
13P10 Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases)
68R07 Computational aspects of satisfiability
94D10 Boolean functions
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Asahiro, Y.; Iwama, K.; Miyano, E., Random generation of test instances with controlled attributes, (Johnson, D.; Trick, M., Cliques, Coloring, and Satisfiability. Cliques, Coloring, and Satisfiability, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26 (1996), American Mathematical Society: American Mathematical Society Providence), 377-394 · Zbl 0864.90089
[2] Audemard, G.; Simon, L., Glucose in the SAT 2014 Competition, (Belov, A.; Diepol, D.; Heule, M. J.; Järvisalo, M., SAT Competition 2014: Solver and Benchmark Descriptions (2014), Univ. of Helsinki), 31-32
[3] Bard, G., Algebraic Cryptanalysis (2009), Springer-Verlag: Springer-Verlag Berlin · Zbl 1183.94019
[4] Bard, G. V.; Courtois, N. T.; Jefferson, C., Efficient methods for conversion and solution of sparse systems of low-degree multivariate polynomials over GF(2) via SAT-solvers (2007), Cryptology ePrint Archive, Report 2007/024
[5] Baumgartner, P.; Massacci, F., The taming of the (X)OR, (Lloyd, J.; Dahl, V.; Furbach, U.; Kerber, M.; Lau, K.-K.; Palamidessi, C.; Pereira, L. M.; Sagiv, Y.; Stuckey, P. J., Computational Logic. Computational Logic, CL 2000. Computational Logic. Computational Logic, CL 2000, LNCS, vol. 1861 (2000), Springer-Verlag: Springer-Verlag Berlin), 508-522 · Zbl 0983.68174
[6] Bebel, J.; Yuen, H., Hard SAT instances based on factoring, (Belov, A.; Diepol, D.; Heule, M. J.; Järvisalo, M., SAT Competition 2013: Solver and Benchmark Descriptions (2013), Univ. of Helsinki), 102
[7] Bosma, W.; Cannon, J.; Playoust, C., The Magma algebra system. I. The user language, J. Symb. Comput., 24, 235-265 (1997) · Zbl 0898.68039
[8] Brickenstein, M., Boolean Gröbner Bases: Theory, Algorithms and Applications (2010), Logos Verlag: Logos Verlag Berlin · Zbl 1205.13001
[9] Brickenstein, M.; Dreyer, A., PolyBoRi: a framework for Gröbner basis computations with Boolean polynomials, J. Symb. Comput., 44, 1326-1345 (2009) · Zbl 1186.68571
[10] Büning, H. K.; Lettmann, T., Propositional Logic: Deduction and Algorithms, Cambridge Tracts in Theor. Comp. Sci., vol. 48 (1999), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0957.03001
[11] Burchard, J.; Gay, M.; Messeng Ekossono, A. S.; Horáček, J.; Becker, B.; Schubert, T.; Kreuzer, M.; Polian, I., AutoFault: towards automatic construction of algebraic fault attacks, (Fault Diagnosis and Tolerance in Cryptography. Fault Diagnosis and Tolerance in Cryptography, FDTC 2017 (2017), IEEE), 65-72
[12] Choo, D.; Soos, M.; Chai, K. M.A.; Meel, K. S., BOSPHORUS: bridging ANF and CNF solvers (2018)
[13] Condrat, C.; Kalla, P., A Gröbner basis approach to CNF-formulae preprocessing, (Grumberg, O.; Huth, M., Tools and Algorithms for the Construction and Analysis of Systems. Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 4424 (2007), Springer-Verlag: Springer-Verlag Berlin), 618-631 · Zbl 1186.68576
[14] Courtois, N. T.; Patarin, J., About the XL algorithm over GF(2), (Joye, M., Topics in Cryptology. Topics in Cryptology, CT-RSA 2003. Topics in Cryptology. Topics in Cryptology, CT-RSA 2003, LNCS, vol. 2612 (2003), Springer-Verlag: Springer-Verlag Berlin), 141-157 · Zbl 1039.94511
[15] Courtois, N. T.; Sepehrdad, P.; Sušil, P.; Vaudenay, S., ElimLin algorithm revisited, (Canteaut, A., Fast Software Encryption. Fast Software Encryption, LNCS, vol. 7549 (2012), Springer-Verlag: Springer-Verlag Berlin), 306-325 · Zbl 1282.94039
[16] Dreyer, A.; Nguyen, T. H., Improving Gröbner-based clause learning for SAT solving industrial sized Boolean problems, (Young Researcher Symposium (YRS) (2013), Fraunhofer ITWM: Fraunhofer ITWM Kaiserslautern), 72-77
[17] Eén, N.; Sörensson, N., MiniSat: a SAT solver with conflict-clause minimization (2005)
[18] Faugère, J.-C., FGb: a library for computing Gröbner bases, (Fukuda, K.; Hoeven, J.v.d.; Joswig, M.; Takayama, N., Mathematical Software. Mathematical Software, ICMS 2010. Mathematical Software. Mathematical Software, ICMS 2010, LNCS, vol. 6327 (2010), Springer-Verlag: Springer-Verlag Berlin), 84-87 · Zbl 1294.68156
[19] Gay, M.; Burchard, J.; Horáček, J.; Messeng Ekossono, A. S.; Schubert, T.; Becker, B.; Kreuzer, M.; Polian, I., Small scale AES toolbox: algebraic and propositional formulas, circuit-implementations and fault equations, (Conf. on Trustworthy Manufacturing and Utilization of Secure Devices. Conf. on Trustworthy Manufacturing and Utilization of Secure Devices, TRUDEVICE 2016, Barcelona (2016))
[20] Horáček, J.; Burchard, J.; Becker, B.; Kreuzer, M., Integrating algebraic and SAT solvers, (Blömer, J.; Kotsireas, I. S.; Kutsia, T.; Simos, D. E., Mathematical Aspects of Computer and Information Sciences. Mathematical Aspects of Computer and Information Sciences, LNCS, vol. 10693 (2017), Springer International Publishing: Springer International Publishing Cham), 147-162 · Zbl 07036049
[21] Horáček, J.; Kreuzer, M., Refutation of products of linear polynomials, (Bigatti, A. M.; Brain, M., 3th International Workshop on Satisfiability Checking and Symbolic Computation. 3th International Workshop on Satisfiability Checking and Symbolic Computation, SC-square, Oxford (2018))
[22] Horáček, J.; Kreuzer, M.; Messeng Ekossono, A. S., Computing Boolean border bases, (18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC (2016), IEEE: IEEE Timisoara), 465-472
[23] Hsiang, J., Refutational theorem proving using term-rewriting systems, Artif. Intell., 25, 255-300 (1985) · Zbl 0558.68072
[24] Itsykson, D.; Sokolov, D., Lower bounds for splittings by linear combinations, (Csuhaj-Varjú, E.; Dietzfelbinger, M.; Ésik, Z., Mathematical Foundations of Computer Science 2014. Mathematical Foundations of Computer Science 2014, LNCS, vol. 8635 (2014), Springer-Verlag: Springer-Verlag Berlin), 372-383 · Zbl 1427.68123
[25] Jovanovic, P.; Kreuzer, M., Algebraic attacks using SAT-solvers, Groups Complex. Cryptol., 2, 247-259 (2010) · Zbl 1213.13043
[26] Kapur, D.; Narendran, P., An equational approach to theorem proving in first-order predicate calculus, (Joshi, A., Proc. of the 9th Int. Joint Conf. on Artificial Intelligence, vol. 2. Proc. of the 9th Int. Joint Conf. on Artificial Intelligence, vol. 2, IJCAI’85 (1985), Morgan Kaufmann Publ.: Morgan Kaufmann Publ. San Francisco), 1146-1153
[27] Kreuzer, M.; Robbiano, L., Computational Commutative Algebra 1 (2000), Springer-Verlag: Springer-Verlag Heidelberg · Zbl 0956.13008
[28] Laitinen, T.; Junttila, T.; Niemelä, I., Conflict-driven xor-clause learning (extended version) (2014)
[29] Lauria, M.; Elffers, J.; Nordström, J.; Vinyals, M., Cnfgen: a generator of crafted benchmarks, (Gaspers, S.; Walsh, T., Theory and Applications of Satisfiability Testing. Theory and Applications of Satisfiability Testing, SAT 2017. Theory and Applications of Satisfiability Testing. Theory and Applications of Satisfiability Testing, SAT 2017, LNCS, vol. 10491 (2017), Springer-Verlag: Springer-Verlag Cham), 464-473 · Zbl 06807244
[30] Marques-Silva, J., Algebraic simplification techniques for propositional satisfiability, (Dechter, R., Principles and Practice of Constraint Programming. Principles and Practice of Constraint Programming, CP 2000. Principles and Practice of Constraint Programming. Principles and Practice of Constraint Programming, CP 2000, LNCS, vol. 1894 (2000), Springer-Verlag: Springer-Verlag Berlin), 537-542 · Zbl 1044.68781
[31] Nordström, J., On the interplay between proof complexity and SAT solving, ACM SIGLOG News, 2, 19-44 (2015)
[32] Perry, J. E., Combinatorial Criteria for Gröbner Bases (2005), North Carolina State University, Ph.D. thesis
[33] Raz, R.; Tzameret, I., Resolution over linear equations and multilinear proofs, Ann. Pure Appl. Logic, 155, 194-224 (2008) · Zbl 1161.03034
[34] Schubert, T.; Reimer, S., antom (2016)
[35] Soos, M., Enhanced Gaussian elimination in DPLL-based SAT solvers, (Berre, D. L., Pragmatics of SAT Workshop. Pragmatics of SAT Workshop, POS 10. Pragmatics of SAT Workshop. Pragmatics of SAT Workshop, POS 10, EPiC Series in Computing. Edinburgh (2010)), 2-14
[36] Soos, M., CryptoMiniSat SAT solver v5.0.1 (2016)
[37] ApCoCoA: applied computations in commutative algebra (2013)
[38] The Sage Developers, SageMath, the Sage Mathematics Software System (Version 7.5.1) (2017)
[39] Zengler, C.; Küchlin, W., Extending clause learning of SAT solvers with Boolean Gröbner bases, (Gerdt, V. P.; Koepf, W.; Mayr, E. W.; Vorozhtsov, E. V., Computer Algebra in Scientific Computing. Computer Algebra in Scientific Computing, LNCS, vol. 6244 (2010), Springer-Verlag: Springer-Verlag Berlin), 293-302 · Zbl 1290.68141
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.