Andrew Krapivin

Andrew Krapivin

CS PhD Student at CMU

The CNF Encoding Complexity of Boolean Functions

with Benjamin Przybocki and Bernardo Subercaseaux

STOC 2027 (under review)

arXiv Version

We investigate how compactly Boolean functions can be encoded as CNF formulas with auxiliary variables. We relate the number of clauses to the time and advice used by a nondeterministic computation, and apply this connection to obtain smaller encodings for \(k\)-CNF functions.