Read-Once Branching Programs as Proof Lines
summary
Defines semantic refutations whose proof lines are read-once branching programs (deterministic, nondeterministic, ordered OBDDs) and shows concrete simulations and limits: OBDD conjunction and projection simulate resolution and refute linear systems and the pigeonhole principle in polynomial size, but particular variable orders make CliqueColoring exponential via Krajíček/Segerlind permutations. Proves exponential lower bounds for read-once nondeterministic BPs on perfect‑matching and Tseitin on expanders and shows NP-hard to automatize OBDD+weakening via a CNF transformation. Open: lower bounds for unrestricted read‑once BP semantic refutations.
AI-written summary · about
chapters (9)
- 0:00Start
- 2:40On lower bounds for semantic proof systems
- 5:09Reasoning by decision trees. Prop. Semantic calculus of decision trees is polynomially equivalent to Resolution.
- 8:14Branching programs
- 21:33Hardness of automation
- 23:411-BP(A)
- 27:49OBDD-based SAT algorithms
- 29:25Hard formulas for 1-NBP(^,3) SAT algorithms
- 31:05Open questions