Lecture 6 in 6.892 Algorithmic Lower Bounds: Fun with Hardness Proofs (Spring 2019)

Lecture 6 Video [previous] [next] [completion form]

[+] Circuit SAT. Dual-rail logic vs. binary logic; Akari/Light Up, Minesweeper (consistency and inference); planar Circuit SAT; Candy Crush / Bejeweled

This lecture starts with a distinction between two key SAT reduction styles:

Dual-rail logic: variables + clauses (most proofs we've seen)
Binary logic: wires + splitters + clauses (crease pattern proof)
Circuit SAT: wires + splitters + universal gates

Then we will see a few proofs in the Circuit SAT style:

Akari / Light-Up (another Nikoli puzzle)
Minesweeper consistency
Minesweeper inference (which is actually coNP-complete)
Candy Crush and Bejeweled (actually from 3SAT)

Video Player is loading.

Current Time 0:00

Duration -:-

Loaded: 0%

Stream Type LIVE

Remaining Time -:-

Download Video: 360p, 720p

Handwritten notes, page 1/6 • [previous page] • [next page] • [PDF]
Video times: • 0:16–7:47

Handwritten notes, page 1/6 • [previous page] • [next page] • [PDF]

Slides, page 1/28 • [previous page] • [next page] • [PDF]
Video times: • 1:02–2:57

http://arxiv.org/abs/1203.1895

Slides, page 1/28 • [previous page] • [next page] • [PDF]

6.892 Algorithmic Lower Bounds: Fun with Hardness Proofs (Spring 2019)

Prof. Erik Demaine TAs: Jeffrey Bosboom, Jayson Lynch

Lecture 6 Video [previous] [next] [completion form]