Lax Lean Archive

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

2-SAT Is in P

Lax117284.TwoSatInP · concepts/Lax117284/TwoSatInP.lean · lax-117284

proven

Loading review…

Community review

Flags

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

No flags have been submitted.

    Community review

    Flag this concept

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

    No source line selected.

    Natural Language Statement

    Theorem

    The language 2-SAT lies in P\mathrm{P}: a deterministic Turing machine decides membership within a polynomial number of steps, in the sense of the archive's class of lax−434930lax-434930.

    Concept map
    7 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax117284.TwoSatCNF
    2
    3/-!
    4---
    5title: 2-SAT Is in P
    6type: theorem
    7---
    8The language 2-SAT lies in P\mathrm{P}: a deterministic Turing machine decides membership
    9within a polynomial number of steps, in the sense of the archive's class of `lax-434930`.
    10
    11# Formalization Notes
    12
    13This is the word RAM bound of this submission, transferred. The program that decides the
    14language on the zeros and ones of the word runs in time polynomial in the length of the word,
    15with all values polynomially bounded, so it is a polynomial-time word RAM computation in the
    16sense of `lax-759944`, and that submission's equivalence gives a polynomial-time Turing machine
    17over the encoding of the bits; two fixed translations, from a binary word to the encoding of its
    18bits and back to a single output bit, complete the machine the class asks for.
    19-/
    20
    21namespace Lax117284.TwoSatInP
    22
    23open Lax434930.PolynomialTime Lax117284.TwoSatCNF
    24
    25/-- **2-SAT ∈ P.** -/
    26axiom twoSAT_mem_P : TwoSAT ∈ P
    27
    28end Lax117284.TwoSatInP
    29
    Show Proof
    Formalization Notes

    This is the word RAM bound of this submission, transferred. The program that decides the language on the zeros and ones of the word runs in time polynomial in the length of the word, with all values polynomially bounded, so it is a polynomial-time word RAM computation in the sense of lax−759944lax-759944, and that submission's equivalence gives a polynomial-time Turing machine over the encoding of the bits; two fixed translations, from a binary word to the encoding of its bits and back to a single output bit, complete the machine the class asks for.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…