# On the maximal minimal cube lengths in distinct DNF tautologies

## TL;DR

This paper explores the maximum minimal clause length in certain DNF formulas with specific structural constraints, using SAT solvers to answer open questions and analyze symmetric cases.

## Contribution

It introduces a computational approach to determine maximal minimal clause lengths in constrained DNF formulas, extending previous theoretical work.

## Key findings

- Identified maximal minimal clause lengths for various DNF configurations
- Solved open questions from prior research using SAT solvers
- Analyzed the impact of symmetry constraints on DNF formulas

## Abstract

Inspired by a recent article by Anthony Zaleski and Doron Zeilberger, we investigate the question of determining the largest k for which there exists boolean formulas in disjunctive normal form (DNF) with n variables, none of whose conjunctions are `parallel', and such that all of them have at least k literals. Using a SAT solver, we answer some of the questions they left open. We also determine the corresponding numbers for DNFs obeying certain symmetries.