{
  "id": "1212.1789",
  "version": "v2",
  "published": "2012-12-08T13:23:20.000Z",
  "updated": "2013-07-18T08:42:35.000Z",
  "title": "On the computational complexity of finding hard tautologies",
  "authors": [
    "Jan Krajicek"
  ],
  "doi": "10.1112/blms/bdt071",
  "categories": [
    "math.LO",
    "cs.CC"
  ],
  "abstract": "It is well-known (cf. K.-Pudl\\'ak 1989) that a polynomial time algorithm finding tautologies hard for a propositional proof system $P$ exists iff $P$ is not optimal. Such an algorithm takes $1^{(k)}$ and outputs a tautology $\\tau_k$ of size at least $k$ such that $P$ is not p-bounded on the set of all $\\tau_k$'s. We consider two more general search problems involving finding a hard formula, {\\bf Cert} and {\\bf Find}, motivated by two hypothetical situations: that one can prove that $\\np \\neq co\\np$ and that no optimal proof system exists. In {\\bf Cert} one is asked to find a witness that a given non-deterministic circuit with $k$ inputs does not define $TAUT \\cap \\kk$. In {\\bf Find}, given $1^{(k)}$ and a tautology $\\alpha$ of size at most $k^{c_0}$, one should output a size $k$ tautology $\\beta$ that has no size $k^{c_1}$ $P$-proof from substitution instances of $\\alpha$. We shall prove, assuming the existence of an exponentially hard one-way permutation, that {\\bf Cert} cannot be solved by a time $2^{O(k)}$ algorithm. Using a stronger hypothesis about the proof complexity of Nisan-Wigderson generator we show that both problems {\\bf Cert} and {\\bf Find} are actually only partially defined for infinitely many $k$ (i.e. there are inputs corresponding to $k$ for which the problem has no solution). The results are based on interpreting the Nisan-Wigderson generator as a proof system.",
  "revisions": [
    {
      "version": "v2",
      "updated": "2013-07-18T08:42:35.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03F20",
      "68Q15"
    ],
    "keywords": [
      "finding hard tautologies",
      "computational complexity",
      "proof system",
      "time algorithm finding tautologies hard",
      "polynomial time algorithm finding tautologies"
    ],
    "tags": [
      "journal article"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 0,
      "language": "en",
      "license": "arXiv",
      "status": "editable",
      "adsabs": "2012arXiv1212.1789K"
    }
  }
}