Nonogram

AbbreviationNonogram instances#✓fully proved

A nonogram instance is a pair \((R, C)\) of finite lists, the row clues \(R\) and the column clues \(C\), where each clue is a finite list of natural numbers.

abbrev NonogramInstance := List (List ℕ) × List (List ℕ)

Used by 2

Used byThe NONOGRAM decision problem · Feasible nonogram instances

DefinitionOne step of the run-length computation#✓fully proved

For a Boolean \(b\) and a pair \((k, R)\) of a natural number \(k\) and a finite list \(R\) of natural numbers, the step returns \((k + 1, R)\) if \(b\) is true. If \(b\) is false it returns \((0, R)\) when \(k = 0\), and \((0, R')\) when \(k > 0\), where \(R'\) is the list \(R\) with \(k\) prepended.

Here \(k\) is the length of the current run of true cells and \(R\) is the list of completed runs.

def RunsStep (b : Bool) (acc : ℕ × List ℕ) : ℕ × List ℕ :=
  if b then (acc.1 + 1, acc.2) else (0, if acc.1 = 0 then acc.2 else acc.1 :: acc.2)

Used by 1

Used byRun lengths of a row

DefinitionRun lengths of a row#✓fully proved

For a finite list \(l\) of Booleans, the runs of \(l\) are its maximal blocks of consecutive true entries. The run list of \(l\) is the list of the lengths of these blocks, in order from left to right; it is empty when \(l\) has no true entry.

def Runs (l : List Bool) : List ℕ :=
  let acc := l.foldr RunsStep (0, [])
  if acc.1 = 0 then acc.2 else acc.1 :: acc.2

Uses 1 · Used by 1

Statement usesOne step of the run-length computation

Used byFeasible nonogram instances

DefinitionFeasible nonogram instances#✓fully proved

A nonogram instance with row clues \(R_0, \dots, R_{m-1}\) and column clues \(C_0, \dots, C_{n-1}\) is feasible when there is a picture, a list of \(m\) rows of Booleans each of length \(n\), such that for every \(r < m\) the run list of row \(r\) equals \(R_r\), and for every \(c < n\) the run list of column \(c\), read from row \(0\) to row \(m - 1\), equals \(C_c\).

def NonogramFeasible
    (i : NonogramInstance) : Prop :=
  ∃ picture : List (List Bool), picture.length = i.1.length ∧
    (∀ row ∈ picture, row.length = i.2.length) ∧
    (∀ r < i.1.length, Runs (picture.getD r []) = i.1.getD r []) ∧
    ∀ c < i.2.length, Runs ((List.range picture.length).map
      (fun r => (picture.getD r []).getD c false)) = i.2.getD c []

Uses 2 · Used by 1

Statement usesNonogram instances · Run lengths of a row

Used byThe NONOGRAM decision problem

DefinitionThe NONOGRAM decision problem#✓fully proved

NONOGRAM is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of nonogram instances, to a feasible nonogram instance. Bitstrings that do not decode to an instance are rejected.

noncomputable def nonogramDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := NonogramInstance) x with
  | some i => decide (NonogramFeasible i)
  | none => false

Uses 11 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Feasible nonogram instances · Nonogram instances · Decision problems

Used byNONOGRAM is NP-complete

TheoremNONOGRAM is NP-complete#●ready to prove

The NONOGRAM decision problem belongs to NP, and every decision problem in NP reduces to NONOGRAM by a polynomial-time many-one reduction.

public theorem_wanted nonogram_npComplete :
    nonogramDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.NP →
          Cslib.CookLevin.PolyManyOneRed L nonogramDec

Sources

• N. Ueda and T. Nagao, "NP-completeness results for nonogram via parsimonious reductions" (1996).

Uses 5

Statement usesPolynomial-time many-one reduction · The NONOGRAM decision problem · Complexity classes · Decision problems · The complexity class NP

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.