Unsatisfiable (k,(4*2^k/k))-CNF formulas

TL;DR

This paper proves the existence of a specific class of unsatisfiable boolean formulas in conjunctive normal form, characterized by fixed clause size and variable occurrence limits, advancing understanding of formula satisfiability thresholds.

Contribution

It establishes the existence of unsatisfiable (k, 4*(2^k/k))-CNF formulas, a new bound in the study of formula satisfiability.

Findings

Existence of unsatisfiable (k, 4*(2^k/k))-CNF formulas

Advances understanding of satisfiability thresholds

Provides new bounds for clause-variable configurations

Abstract

A boolean formula in a conjuctive normal form is called a (k,s)-formula if every clause contains exactly k variables and every variable occurs in at most s clauses. We prove the existence of a (k, 4 * (2^k/k))-CNF formula which is unsatisfiable.