zbMATH — the first resource for mathematics

On the maximal minimal cube lengths in distinct DNF tautologies. (English) Zbl 1449.05018
Summary: Inspired by a recent article by A. Zaleski and D. Zeilberger [“Boolean function analogs of covering systems”, Preprint, arXiv:1801.05097], we investigate the question of determining the largest $$k$$ for which there exist Boolean formulas in disjunctive normal form (DNF) with $$n$$ variables, which are tautologies, whose conjunctions have distinct sets of variables, and such that all the conjunctions have at leastkliterals. Using a SAT solver, we answer the question for some sizes which Zaleski and Zeilberger [loc. cit.] left open. We also determine the corresponding numbers for DNFs obeying certain symmetries.
MSC:
 05A15 Exact enumeration problems, generating functions 68W30 Symbolic computation and algebraic computation
Software:
CaDiCaL; Lingeling; Plingeling; Treengeling; YalSAT
Full Text:
References:
 [1] M. Artin,Algebra, Prentice Hall, New Jersey, 1991. [2] A. Biere, CaDiCaL, lingeling, plingeling, treengeling, YalSAT entering the SAT competition 2017,Proceedings of SAT Competition 2017 - Solver and Benchmark Descriptions, 2017. [3] A. Biere, M. Heule, H. Van Maaren, T. Walsh (Eds.),Handbook of Satisfiability,Vol. 185 of Frontiers in Artificial Intelligence and Applications, IOS Press, Amsterdam, 2009. · Zbl 1183.68568 [4] J, Chen, A new SAT encoding of the at-most-one constraint,Proceedings of the Tenth International Workshop of Constraint Modelling and Reformulation, 2010. [5] P. Erd˝os, On integers of the form2k+pand some related problems,Summa Brasil. Math.2(1950) 113-123. [6] A. M. Frisch, P. A. Giannaros, SAT encodings of the at-most-kconstraint: some old, some new, some fast, some slow,Proceedings of the Tenth International Workshop of Constraint Modelling and Reformulation, 2010. [7] D. E. Knuth,The Art of Computer Programming,Vol. 4, Fascicle 6: Satisfiability, Addison-Wesley, Boston, 2015. [8] K. A. Sakallah, Symmetry and satisfiability, In: A. Biere, M. Heule, H. Van Maaren, T. Walsh (Eds.),Handbook of Satisfiability,Vol. 185 of Frontiers in Artificial Intelligence and Applications, IOS Press, Amsterdam, 2009. [9] A.
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.