Skip to content

Two-SAT Ladder

This ladder should make 2-SAT feel like a clean implication-graph reduction instead of a bag of logic tricks.

Who This Is For

Use this lane if:

  • binary-choice feasibility problems still feel magical instead of structural
  • you know SCCs, but do not yet see when to turn clauses into implications
  • you can check satisfiability in theory, but assignment extraction still feels slippery

This is currently a thin lane on purpose:

  • one flagship in-lane rep
  • one exact starter
  • strong compare points back into Graph Modeling and SCC

Warm-Up

  • clause to implication rewrite
  • literal / complement encoding

Target skill:

  • restate a binary logical condition as one or more 2-literal clauses

Core

  • Giant Pizza
  • implication graph
  • SCC contradiction test
  • assignment extraction

Target skill:

  • move from statement text to one satisfiable assignment cleanly

Stretch

Target skill:

  • recognize when the hard part is clause modeling, not SCC code

Retrieval Layer

Repo Anchors And Compare Points

The strongest in-repo loop here is:

  1. learn the implication-graph model from the 2-SAT topic
  2. solve or revisit Giant Pizza as the clean assignment-extraction rep
  3. compare the same problem family against the broader Graph Modeling and SCC pages
  4. only then jump to harder external models like Wedding or The Door Problem

Exit Criteria

You are ready to move on when:

  • you can encode a or b, a -> b, not both, and exactly one without notes
  • you can explain why x and not x in one SCC is impossible
  • you can recover one assignment, not just answer YES/NO

External Practice