Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

A Simplified NP-Complete Satisfiability Problem

lax-345332·formalized by Yuval Itzhaki @yuvalyitz · Claude·created ·GitHub @e5915ce·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this submission may be incorrect.

No flags have been submitted.

    Community review

    Flag this submission

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    Abstract

    (3,4)-SAT is satisfiability restricted to formulas in which every clause has exactly three literals and every variable occurs at most four times. Tovey (1984) proved that it is NP-hard. This submission states that theorem: every language in NP has a polynomial-time many-one reduction to (3,4)-SAT, on the CNF encoding and the Turing machines of the archive's Cook–Levin theorem.

    The reduction is from unrestricted satisfiability. Every literal occurrence receives a fresh variable; a clause is chained through link variables into clauses of at most three literals; a cycle of implications forces the copies of one variable to agree; and every short clause is filled with the negation of a fresh variable that Tovey's thirteen-clause gadget forces to be true.

    The correctness of the reduction is proved. Its polynomial running time is stated and not proved: the one statement of this submission that remains open.

    Concepts

    Concept map
    9 concepts
    100%
    Proven claimOpen claimDefinitionThis submissionOther submissionA → B: B builds on A

    Proofs

    Proof networkview on GitHub

    100%
    assumptions conclusionProven claimOpen claimStatement 1, 2, … of a claim with several statementsClaim from this submission / another submissionProof — open large view for details
    Proof list

    Lean sources for these proofs: proofs/ on GitHub

    Proof code is not displayed; the archive records each proof's checked relationship between claims.

    Related submissions

    Submission map

    100%
    This submissionOther submissionA → B: B's concepts build on A

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-345332,
  author = {Yuval Itzhaki and Claude},
  title = {A Simplified NP-Complete Satisfiability Problem},
  year = {2026},
  howpublished = {Lax Archive, lax-345332},
  url = {https://laxarchive.org/lax-345332/},
  note = {draft},
}

    References

    1. Craig A. Tovey. A simplified NP-complete satisfiability problem. Discrete Applied Mathematics 8(1):85–89, 1984. doi:10.1016/0166-218X(84)90081-7

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…