Polynomial-time verifier for SAT

Occurrence list of a CNF formula to SAT is in NP if its verifier is polynomial-time

• Occurrence list of a CNF formula
• Witness lookup
• Clause check against a witness
• Formula check against a witness
• The SAT verifier
• Cost bound for witness lookup
• Lookup in the witness of an assignment
• Correctness of the witness clause check
• Cost bound for the witness clause check
• Correctness of the witness formula check
• Cost bound for the witness formula check
• Length of the occurrence list
• Variables of a formula occur in its occurrence list
• The literal count is at most the code length
• The SAT verifier rejects undecodable inputs
• The SAT verifier on a decodable input
• Declared time bound of the SAT verifier
• The SAT verifier has polynomial declared time
• The SAT verifier verifies SAT
• SAT is in NP if its verifier is polynomial-time

Stack alphabet of the SAT verifier to A clause has at most as many tokens as code bits

• Stack alphabet of the SAT verifier
• Reading a symbol as a name bit
• Tokens of a literal
• Tokens of a clause
• Token sequence of a CNF formula
• Table entries
• Closing marker of a table entry
• Symbols of a table entry
• Table stack of an entry list
• Occurrence table of a list of variables
• Occurrence table of a formula and a witness
• Live value of a name in a table
• Clause check against an occurrence table
• Tokenizer of the SAT verifier
• The binary code of natural numbers is injective
• Canonical binary names
• Table lookup agrees with the verifier's variable lookup
• The clause check on the occurrence table is the formula check
• The SAT verifier's answer through the occurrence table
• A clause has at most as many tokens as code bits

Token count is bounded by the encoding length to The lookup program

• Token count is bounded by the encoding length
• Stacks of the clause check
• Driver labels of the clause check
• Clause-check statements
• Configurations of the clause-check machine
• Calling the lookup
• The clause-check driver
• The clause-check driver with a lookup sub-program
• The lookup contract
• A literal's tokens on the token stack
• A clause's tokens on the token stack
• Literal loop of the clause check
• Clause loop of the clause check
• The clause check
• Stacks of the lookup machine
• Labels of the lookup machine
• Moving a symbol between stacks
• Moving a table marker between stacks
• Next label of the lookup scan
• The lookup program

Start label of the lookup machine to Reading a unary count

• Start label of the lookup machine
• Stack contents of the lookup machine
• A name bit reads as itself
• Initialization step of the lookup machine
• Restoring and stashing after a comparison in the lookup machine
• Serving a live table entry
• One scan step of the lookup
• The scan loop of the lookup machine
• The return loop of the lookup machine
• Correctness of the SAT-verifier lookup machine
• Stacks of the SAT tokenizer
• Labels of the SAT tokenizer
• Testing whether the top symbol is a given bit
• Instruction for reading a unary count
• The tokenizer program
• Start label of the SAT tokenizer
• Tokenizer stack contents
• Rejection of the SAT tokenizer within a step bound
• One step to rejection
• Reading a unary count

An unterminated unary count is rejected to Stack alphabets of the SAT verifier host

• An unterminated unary count is rejected
• Name-loop outcome
• Name-loop outcome from the start of a name
• Reading a name block
• Rejecting an unterminated name block
• Reading a polarity
• Tokenizer run on one literal
• Tokenizer rejects an undecodable literal
• Occurrence table of a nonempty list
• Reading the literals of a clause
• Tokenizer rejects undecodable literals
• Tokenizer run on one clause
• Tokenizer run on all clauses
• Tokenizer rejects undecodable clauses
• The tokenizer accepts when the formula stack is empty
• Accepting run of the SAT tokenizer
• Rejecting run
• Input alphabet of the SAT verifier host
• Stacks of the SAT verifier host
• Stack alphabets of the SAT verifier host

Phase-0 labels of the SAT verifier host to Program of the SAT verifier host

• Phase-0 labels of the SAT verifier host
• Labels of the SAT verifier host
• Host labels as a sum type
• Placement of the tokenizer's stacks in the host
• Stack embedding of the tokenizer into the host
• Placement of the lookup's stacks in the clause-check driver
• Stack embedding of the lookup into the clause-check driver
• Lookup labels in the clause-check driver
• The embedded lookup program
• Driver stacks in the SAT host
• Stack embedding of the clause-check driver into the host
• Placement of the filter's stacks in the host
• Stack embedding of the clause-length filter into the host
• Filter exits in the SAT verifier host
• Tokenizer labels in the host machine
• Driver labels in the SAT host
• Reading a formula bit in the SAT host
• Reading a witness bit in the SAT host
• Stacks emptied by the SAT verifier's cleanup
• Program of the SAT verifier host

The SAT verifier machine to SAT is in NP

• The SAT verifier machine
• Phase 0 of the SAT verifier host
• The tokenizer embeds in the SAT verifier host
• The embedded lookup meets the lookup contract
• The cleanup stacks are distinct
• Cleanup of the SAT host
• Name lengths in an occurrence table
• Initial stacks of the SAT verifier host
• Tokenizer stacks after phase 0
• Driver stacks after tokenization
• Step budget before the cleanup
• Cleanup phase of the SAT verifier host
• Answer of the SAT host
• Explicit step bound of the SAT verifier machine
• Initial configuration of the SAT verifier machine
• Step bound of the SAT verifier machine
• The TM2 SAT verifier
• The SAT host's answer is polynomial-time
• The SAT verifier is polynomial-time
• SAT is in NP

Cook–Levin theorem to Finiteness of the SAT verifier alphabet (moved alias)

• Cook–Levin theorem
• Answer of the SAT host with the three-literal filter
• 3SAT is in NP
• Token length bound for the SAT verifier (moved alias)
• Clause token length bound for the SAT verifier (moved alias)
• Finiteness of the SAT verifier alphabet (moved alias)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.