Supercritical space-width trade-offs for resolution

• We show that there are CNF formulas which can be refuted in resolution in both small space and small width, but for which any small-width resolution proof must have space exceeding by far the linear worst-case upper bound. This significantly strengthens the space-width trade-offs in [Ben- Sasson 2009], and provides one more example of trade-offs in the "supercritical" regime above worst case recently identified by [Razborov 2016]. We obtain our results by using Razborov's new hardness condensation technique and combining it with the space lower bounds in [Ben-Sasson and Nordström 2008].

Ämnesord

NATURVETENSKAP  -- Data- och informationsvetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences (hsv//eng)

Nyckelord

Proof complexity

Resolution

Space

Supercritical

Trade-offs

Width

Automata theory

Commerce

Optical resolving power

Trade off

Economic and social effects

Publikations- och innehållstyp

ref (ämneskategori)

kon (ämneskategori)