Presentation slides:

    Sam Buss
    Some Challenge Problems for Resolution and One Also for AC⁰-Frege
    or: Seeking Hard Instances for Constant Depth Frege
    Workshop: Art of SAT
    Shonan Village, Japan
    October 2, 2023.

    Download talk slides.

CNF generation software:
1. StConn - st-connectivity prinicple.
2. FmlaChain - Formula Equivalence Chain (FmlaEquivChain) and Formula Implication Chain (FmlaImplyChain) principles.

Related papers:
1. Polynomial-size Frege and Resolution Proofs of st-Connectivity
2. Short Refutations for the Equivalence Chain Principle for Constant-Depth Formulas (with Ramyaa).

Abstract: We discuss some attempts to find unsatisfiable CNFs that provide expenential separations between depth d Frege proofs and depth d+1 Frege proofs. The principles considered are (a) st-connectivity tautologies, (b)) formula equivalence (equivalence chain) tautologies, and (c)) formula implication (implication chain) tautologies,

In two cases, they were discovered to have polynomial size resolution refutations. These are suggested as challenge problems for SAT solvers. Part of this work is joint with Ramyaa.

Back to Sam Buss's publications page.