Jan FEB OCT » 28 2008 2009 2010 3 captures 28 Feb 09 - 30 Oct 09

Close Help

Open problems

I offer here several open problems in areas of propositional logic, bounded arithmetic, complexity theory and in related model theory. They are by no means meant to represent all interesting open problems in the areas or even to sample them evenly. It is a collection of problems selected from those that were published in works that I (co-)authored, and that seem to me be interesting and possibly stimulating for further research. Their unifying theme (with few exceptions) are links to three interconnected main problems (just short of P/NP): lower bounds for EF, finite axiomatizability of bounded arithmetic, and provability of bounded (weak)PHP in bounded arithmetic. I have also included a couple of folklore problems (on F_d(MOD_p) and on conservativity in bounded arithmetic) to which papers that I (co-)authored contributed. I do not include problems already listed in

• P. Clote and J.Krajicek: "Open Problems", in: "Arithmetic, Proof Theory and Computational Complexity", eds. P. Clote and J. Krajicek, Oxford Press, (1993), pp.1-19.

References point to papers with original formulation; further literature and background can be found in them.

Friendly comments and solutions are most welcomed. The list should change in time (hopefully not only in the increasing manner).

Jan Krajicek
December 2000

The problems are divided into four sections: propositional logic, bounded arithmetic, complexity theory, and model theory, although there are many inter-relations.

Propositional logic

---

• F_d versus F_{d+1}

  Find a constant k such that for any d there is a sequence of tautologies of depth k that have polynomial size (or quasi-polynomial) proofs in depth d+1 Frege system F_{d+1} but requires exponential size F_d proofs.

  Origins/References:

  • J.Krajicek: "Lower Bounds to the Size of Constant-Depth Propositional Proofs", J. of Symbolic Logic, 59(1), (1994), pp.73-86.
  • Also see problem on p.243 of
    J. Krajicek: "Bounded arithmetic, propositional logic, and complexity theory", Encyclopedia of Mathematics and Its Applications, Vol.60, Cambridge University Press, Cambridge - New York - Melbourne, (1995), 343 p.

  Comments:

  Such tautologies are known if k may depend on d (for k:= d). This problem is also closely related to conservativity relations among bounded arithmetic theories.
  
  

  ---

  
  
  

• Ramsey theorem

  Let RAM_n be a set of clauses formed from atoms x_e, one for each possible edge e in a undirected graph on n vertices V, and having for each subset X of V of size log(n)/2 two clauses: \bigvee x_e and \bigvee \neg x_e, with e ranging over all possible edges inside X.
  RAM_n is unsatisfiable as by Ramsey theorem every graph contains a clique or an independent set of size at least log(n)/2.
  Do RAM_n have polynomial size (sub-exponential size) resolution refutations?

  Origins/References:

  J.Krajicek: "On the weak pigeonhole principle", Fundamenta Mathematicae, Vol.170(1-3), (2001), pp.123-140.

  Comments:

  P.Pudlak proved the corresponding Ramsey theorem in bounded arithmetic; from that it can be deduced that RAM_n do have F_3 polynomial size refutations (see my book). It is also known that RAM_n requires exponential size tree-like resolution proofs and n^{1/4} resolution width, and that there are connections to the problem (left open by Buss and Turan) whether WPHP^{n^2}_n is shortly provable in resolution.
  
  

  ---

  
  
  

• Tau formulas

  Let f be a honest polynomial time function (i.e., the lengths of arguments and of the corresponding values are polynomially related), and let \tau(f)_b, b a binary string, denotes a natural propositional formula expressing that b is outside the range of f. The formula has atoms for bits of a possible argument x and for bits of the computation of f(x) by (some canonical) circuit, and it says that if the computation is indeed a correct computation of f(x) then its output is different from b. The formula is tautology iff b is not in the range of f.
  Find f for which the formulas \tau(f)_b require superpolynomial size EF proofs for infinitely many b outside the range of f. Prove this at least under some plausible computational complexity theoretic conjecture.
  An interesting case is when f extends the inputs by one bit. A particularly interesting is the following example: Let G be (n+1) \times n 0-1 matrix chosen uniformly at random from all such matrices having exactly m = O(log n) ones in every row. Let g be a random boolean function with m inputs. Define f to be the function that from n bits computes n+1 bits as in Nisan-Wigderson generators set-up, using G and g. (Note that f is computable by polynomial size DNFs.) Is there any proof system that proves shortly the tau formulas for such "random" f?

  Origins/References:

  • J.Krajicek and P. Pudlak: "Some consequences of cryptographical conjectures for $S^1_2$ and $EF$", Information and Computation, Vol.140(1), (January 10, 1998), pp.82-94.
  • J.Krajicek: "On the weak pigeonhole principle", Fundamenta Mathematicae, Vol.170(1-3), (2001), pp.123-140.
  • J.Krajicek: "Tautologies from pseudo-random generators", Bulletin of Symbolic Logic, 7(2), (2001), pp.197-212.
  • M. Alekhnovich, E.Ben-Sasson, A.A.Razborov, and A.Wigderson, Pseudorandom generators in propositional proof complexity, preprint, (March 2000).
  • J.Krajicek: Nisan-Wigderson type functions are free for constant depth Frege systems, in preparation, 2000.

  Comments:

  Two special instances of this general problem are considered in the references: when f is the product of numbers greater than 1 (the formulas then express primeness), and when f is a pseudo-random number generator. The later case is related to provability of (the dual of) weak PHP in bounded arithmetic.
  
  

  ---

  
  
  

• F_d(MOD_p)

  F_d(MOD_p) is a Frege system of depth d in the DeMorgan language augmented by a connective MOD_p counting modulo p (of unbounded arity).
  Prove a superpolynomial lower bound for the system, at least when p is a prime.

  Origins/References:

  • see problems on p.267 and p.270 of
    J. Krajicek: "Bounded arithmetic, propositional logic, and complexity theory", Encyclopedia of Mathematics and Its Applications, Vol.60, Cambridge University Press, Cambridge - New York - Melbourne, (1995), 343 p.
  • S. Buss, R. Impagliazzo, J.Krajicek, P. Pudlak, A. A. Razborov and and J. Sgall: "Proof complexity in algebraic systems and bounded depth Frege systems with modular counting counting", Computational Complexity, 6(3), 1996/1997, pp.256-298.

  Comments:

  The strongest lower bound towards the problem is for a system combining polynomial calculus and constant depth Frege systems:
  • J.Krajicek: ``Lower bounds for a proof system with an exponential speed-up over constant-depth Frege systems and over polynomial calculus'', in: Eds. I.Privara, P. Ruzicka, 22nd Inter. Symp. Mathematical Foundations of Computer Science (Bratislava, August '97), Lecture Notes in Computer Science 1295, Springer-Verlag, (1997), pp.85-90.
  It is hoped that boolean complexity method of Razborov-Smolensky for the circuit class ACC[p] could be somehow adopted.
  
  

  ---

  
  
  

• Interpolation for R(2)

  Let R(2) be an extension of resolution allowing clauses formed not only from literals but also from conjunctions of two literals, and having some suitable rules to manipulate these clauses.
  Does the system R(2) have monotone feasible interpolation?

  Origins/References:

  • J.Krajicek: "Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic", J. of Symbolic Logic, 62(2), (1997), pp.457-486.
  • J.Krajicek: "On the weak pigeonhole principle", Fundamenta Mathematicae, Vol.170(1-3), (2001), pp.123-140.

  Comments:

  The affirmative answer implies exponential lower bound to the size of resolution proofs of the WPHP^{n^2}_n. The negative one would yield an optimal bound on feasible interpolation among subsystems of Frege systems.

  Solution:

  It was proved in
  • A.Atserias, M.L.Bonet and J.L.Esteban: "Lower bounds and separations on extensions of resolution", preprint (Jan. 2001)
  that R(2) has no monotone feasible interpolation.

  Further comments:

  What remains still is to prove a lower bound on R(2)-proofs of WPHP^{n^4}_n. Such bound implies a lower bound for R-proofs of Ramsey formulas. Atserias et.al. proved a lower bound for WPHP with O(n) in place of n^4, and Ran Raz recently (Jan.'01) proved a lower bound for R-proofs of WPHP^{\infty}_n.
  
  

  ---

  
  
  

• Relativization of principles

  Let A be a sentence in language L and let D be a new unary predicate symbol not in L. Denote by A^D the relativization of A to D.
  For which proof systems P it holds that if P admits short proofs of A then it also admits short proofs of A^D? In particular, does this hold for resolution?

  Origins/References:

  • J.Krajicek: Combinatorics of first order structures and propositional proof systems, preprint, July'01.

  Comments:

  It holds for any P simulating F (or admiting "counting"). The problem is also related to provability of WPHP in weak systems.

Bounded arithmetic

---

• Conservativity in bounded arithmetic

  Prove that T^i_2(alpha) is not \forall\Sigma^b_1(alpha)- (or even \forall\Pi^b_1(alpha)-) conservative over S^i_2(alpha), and give some conditional separation in the unrelativised case.
  In a first step characterise \Sigma^b_1- and \Sigma^b_2- consequences of T^2_2.

  Origins/References:

  • J.Krajicek: "Fragments of Bounded Arithmetic and Bounded Query Classes", Transactions of the AMS, 338(2), (1993), pp.587-598.
  • S. Buss and J.Krajicek: "An Application of Boolean Complexity to Separation Problems in Bounded Arithmetic", Proceedings of the London Mathematical Society, 69(3), (1994), pp.1-21.
  • M. Chiari and J.Krajicek: "Witnessing functions in bounded arithmetic and search problems", J. of Symbolic Logic, 63(3), (1998), pp. 1095-1115.
  • M.Chiari and J.Krajicek: "Lifting independence results in bounded arithmetic", Archive for Mathematical Logic, 38(2), (1999), pp.123-138.
  • R.Impagliazzo and J.Krajicek: A note on conservativity relations among bounded arithmetic theories, Mathematical Logic Quarterly, to app.

  Comments:

  It is known that T^i_2(alpha) is not \Sigma^b_i(alpha)-conservative over S^i_2(alpha), and a bit better information is known for i=2. A partial problem is: A \Sigma^b_2- principle MIN that every p-time linear ordering of [0,a] has the least element is provable in T^2_2. Does the principle axiomatizes (over S^1_2) all Sigma^b_2-consequences of T^2_2?
  F.Ferreira's paper "What are the \forall \Sigma^b_1-consequences of T^1_2 and T^2_2", Annals of Pure and Applied Logic, 75(1-2):79-88, (1995), offers a characterization of such conseqeunces of T^2_2, but apparently rather hard to use for some independence result.
  The situation is better understood without the smash function: T^{i+1}_1(alpha) is not Sigma^b_2(alpha) conservative over T^i_1(alpha), by the last reference.
  
  

  ---

  
  
  

• Counter-example function

  For a bipartite graph R \subseteq [0,u) \times [0,u) consider \exists\Pi^b_1 - statement CE(R,u):
  • either there is a sequence x_0, ..., x_k of elements < u such that for all y < u one of R(x_i, y) fails
  • or there is a sequence y_0, ..., y_k of elements < u such that for all x < u one of R(x, y_j) holds.
  This is true (by PHP) for k < log(u) + 1. Is the formula CE(R,u) provable in S_2(R)?

  Origins/References:

  • J.Krajicek: "Extensions of models of $PV$", in: Logic Colloquium'95, Eds. J.A.Makowsky and E.V.Ravve, ASL/Springer Series Lecture Notes in Logic, Vol.11, (1998), pp.104-114.

  Comments:

  This problem is relevant to constructions of models of PV with particular properties w.r.t. classes P, NP, coNP.
  
  

  ---

  
  
  

• EF lengths-of-proofs in PV

  Denote by (*) the Pi_2- statement that every tautology has an EF-proof.
  • Is there a model of S^1_2 satisfying (*) in which Exp fails?
  • Does every countable model of S^1_2 have a Delta^b_1-elementary extension to a model of S^1_2 in which (*) holds?
  • Is there a model of PV satisfying (*) and collection scheme B\Sigma_0 in which Exp fails?
  (Exp is the \Pi_2-statement that exponentiation is total.)

  Origins/References:

  • J.Krajicek and P. Pudlak: "Propositional Provability and Models of Weak Arithmetic", in: Computer Science Logic (Kaiserlautern, Oct. '89), E. Borger, H. Kleine Buning, M.M. Richter (eds.), LNCS 440, (1990), Springer-Verlag, pp. 193-210.

  Comments:

  It is proved in the reference that PV cannot prove super-polynomial lower bounds to the size of EF proofs. Solutions of the problems would allow to improve this independence result in various ways. (The affirmative answer to the 2nd implies one to the 1st.)

Complexity theory

---

• AC^0 cardinality:

  Is there a constant k such that whenever A and B are subsets of \{0,1\}^n that are computable by circuits of depth d and size S, then there is an injective mapping f of either A into B or vice versa such that the graph of f is computable by a circuit of depth d+k size at most S^k?
  The expected answer is in the negative and the following combinatorial example was proposed in the reference. AC^0-sets A and B(k), for k>0 a fixed number, will be sets of graphs on n vertices without loops. Set A consists of directed graphs that are vertex-disjoint unions of directed cycles. The set B(k) consists of undirected graphs that are vertex-disjoint unions of cycles, each cycle having one of k colours.
  
  • Is there an embedding of B(1) into $A$ with AC^0 definable graph?
  • Is there a bijection between B(2) and A with AC^0 definable graph?
  • Is there an embedding of A into B(k), any k>2, with AC^0 definable graph?

  Origins/References:

  The problem was informally proposed by M.Ajtai around 1990. It has been rediscovered and published in:
  
  J.Krajicek and T.Scanlon: "Combinatorics with definable sets: Euler characteristics and Grothendieck rings", Bulletin of Symbolic Logic, 3(3), (2000), pp.311-330.

  Comments:

  The general problem is clearly related to counting of polynomial time sets and using Toda's theorems one can answer the problem in the negative (even for f's with graphs in PH/poly), assuming that the polynomial time hierarchy PH does not collapse.
  
  

  ---

  
  
  

• Monotone protocols

  Real communication complexity of a problem is defined to be the minimal number of rounds two players need when the communication is as follows: each player announces a real number to a referee and the referee tells them how are the numbers ordered. Ordinary protocols are binary trees, as in the usual Karchmer-Wigderson boolean set-up.
  More general protocols are directed acyclic graphs with one root, out-degree at most 2, and with leaves labelled by answers to the problem. The players move along the edges from the root to a leaf, deciding where to go by a real communication as above. (There is further a technical condition called "consistency notion": the players must be able to decide, given a node in the protocol, if starting in that node and following their strategy they get a correct answer.) Let the protocol have size S (number of nodes) and communication complexity t: that is the real communication complexity of moving along the edges and deciding the consistency condition. (More details are in the references.)
  The protocol is monotone if the task it solves is the usual task of finding bit i such that player I's string u has i-th bit 1 while player II's string v has i-th bit 0.
  Problem: Give an exponential lower bound for size S of monotone protocols whose real communication complexity is t=log(S).

  Origins/References:

  • J.Krajicek; "Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic", J. of Symbolic Logic, 62(2), (1997), pp.457-486.
  • J.Krajicek: "Interpolation by a game", Mathematical Logic Quarterly, 44(40), (1998), pp.450-458.

  Comments:

  This problem is related to an approach towards feasible interpolation via communication complexity. Note that one can define similar generalized communication over any structure in place of the ordered real line (the players announce elements of the structure and the referee tells them is some basic relation holds for them or not). Can one prove lower bound for monotone protocols over a general structure?
  
  

  ---

  
  
  

• Counter-example computations

  An optimization problem is a binary p-time relation R(x,y) and a p-time function c(y), the task being: given x find a solution y, |y| \le |x|, with maximal possible cost c(y).
  A counter-example computation of an optimal solution proceeds in several rounds of a game/communication between an all-powerful Teacher and a p-time Student. Given x, Student produces y_0. If it is not optimal teacher replies with y_1 of a bigger cost. Student then produces another candidate y_2 using also y_1. If it is not optimal Teacher offers another counter-example y_3 with a bigger cost and Student uses it to compute his new candidate y_4, etc.
  Show that there are optimization problems that cannot be solved in this fashion in polynomially many rounds.

  Origins/References:

  • J.Krajicek, P. Pudlak, and J. Sgall: "Interactive Computations of Optimal Solutions", in: B. Rovan (ed.): Mathematical Foundations of Computer Science (B. Bystrica, August '90), Lecture Notes in Computer Science 452, Springer-Verlag, (1990), pp. 48-60.

  Comments:

  This notion of interactive computation is relevant to provability in bounded arithmetic. Several purely complexity-theoretic results are proved in the reference.
  
  

  ---

  
  
  

• Newsize of formulas

  Consider the following search problem. Given a 0-1 labelling \alpha of the edges of graph G with an odd number of vertices, find a vertex v for which the parity condition:
  e_1 \oplus \dots \oplus e_t = 1
  is violated (e_i's are the edges incident with v).
  We solve the problem using decision trees where at a node we ask about labels of edges incident with a vertex of G and the tree branches into 2^t subtrees depending on the labels. Denote by D(G) the minimal height of such a tree solving the search problem for all labellings of the edges of G.
  Define newsize(\psi) for DeMorgan formula \psi with atoms corresponding to edge labels to be the minimal number k such that there is a set W of k vertices such that the truth value of \psi can be determined knowing only the labels of the edges incident with a vertex from W.
  Find a type of constant degree graphs G and a space of random partial evaluations \rho of \alpha leaving \sim p \cdot n edges unlabelled and having with a high probability two properties:
  • D(G^{\rho}) = \Omega(p n)
  • newsize(\psi^{\rho}) = O(p^{1+\epsilon} \cdot newsize(\psi))
  where $\epsilon > 0$. We want this for p of the form n^{\delta - 1}.

  Origins/References:

  • "On Frege and Extended Frege Proof Systems", in: "Feasible Mathematics II", eds. P. Clote and J. Remmel, Birkhauser, (1995), pp. 284-319.
  • J.Krajicek: "Bounded arithmetic, propositional logic, and complexity theory", Encyclopedia of Mathematics and Its Applications, Vol. 60, Cambridge University Press, Cambridge - New York - Melbourne, (1995), 343 p.

  Comments:

  This is aimed at proving a modest but non-trivial lower bound for Frege proofs of Tseitin's tautologies.
  It is motivated by the method of Subbotovskaja which showed that the expected shrinking of a formula $\psi$ in atoms $x_1, \dots, x_n$ under random restrictions is by a factor O(p^{3/2}). We would need therefore a type of graphs G for which the decision complexity D(G) is \Omega(n) and such that the restricted graphs G^{\rho} are of the same type (which would yield condition 1.) and for which the shrinking of the formulas w.r.t. the "newsize" occurs with factor p^{1+\Omega(1)}. Expander-type graphs might be good candidates.

Model theory

---

• Euler structures

  An "Euler structure" is a first-order structure admitting an abstract Euler characteristic of definable sets (see the references). The values of such an abstract characteristic lie in a Grothendieck ring of the structure. Numerous problems were formulated in the references; some especially interesting are:
  • What is the relation between Grothendieck rings of elementarily equivalent structures?
  • Which fields admit nontrivial strong Euler characteristic?
  • Which fields admit nontrivial strong partially ordered Euler characteristic?
  • To what extent is the Grothendieck ring of a structure definable (perhaps in terms of some imaginary parameters associated to the structure)?
  • Describe all Euler characteristics with values in a finite field on pseudo-finite fields, or at least on ultraproducts of finite fields.

  Origins/References:

  • J.Krajicek: "Uniform families of polynomial equations over a finite field and structures admitting an Euler characteristic of definable sets", Proc. London Mathematical Society, 3(81), (2000), pp.257-284.
  • J.Krajicek and T. Scanlon: "Combinatorics with definable sets: Euler characteristics and Grothendieck rings", Bulletin of Symbolic Logic, 3(3), (2000), pp.311-330.

  Comments:

  Various partial results are reported in the references. This topic is also related to algebraic proof complexity (Nullstellensatz and polynomial calculus).
  The existence of Euler characteristic depends on validity of PHP in the structure for definable functions, and its various properties depend on validity of other counting principles.
  
  

  ---

  
  
  

• Combinatorics of a structure

  Fix L the language of directed graphs (one binary relation) with possible some constants. Let M be arbitrary structure (in some language). The combinatorics of M, Comb(M), is the set of all L-sentences that hold in all directed graphs definable in M.
  Are there some interesting structures of algebraic or geometric nature whose Comb(M) is recursively enumerable? Or some interesting classes C of such structures such that the intersection of all Comb(M) for M in C is r.e.?

  Origins/References:

  J.Krajicek: Combinatorics of first order structures and propositional proof systems preprint, (2001).

  Comments:

  This is related to an application of model theory in proof complexity.
  
  

  ---

  
  
  

• MST

  Prove the consistency of Modal Set Theory MST.

  Origins/References:

  • J.Krajicek: "A Possible Modal Formulation of Comprehension Scheme", Zeitchr. f. Mathematikal Logik u. Grundlagen d. Mathematik, Bd. 33(5), (1987), pp. 461-480.
    
    
  • J.Krajicek: "Some Results and Problems in the Modal Set Theory MST", Zeitschr. f. Mathematikal Logik u. Grundlagen d. Mathematik, Bd. 34(2), (1988), pp.123-134.

  Comments:

  Modal Set Theory MST is an intuitively very clean axiomatization of a set theory based on a modal version of unrestricted comprehension axioms as the only non-logical axioms. It interprets PA and proves the existence of an infinite set. It's non-trivial fragment is proved to be consistent.
  A proof of the consistency of the whole theory based on some "feasibility" interpretation of the modality would be very interesting.
  
  

  ---

  
  
  

• Lattice of chapters

  Construct explicit examples of length 1 intervals in the lattice of local interpretability types (Mycielski's lattice of chapters).

  Origins/References:

  • J.Krajicek: "Some Theorems on the Lattice of Local Interpretability Types", Zeitschr. f. Mathematikal Logik u. Grundlagen d. Mathematik, Bd. 31, (1985), pp. 449-460.
    
    
  • J.Mycielski, P.Pudlak and A.S.Stern: A lattice of chapters of mathematics (interpretations between theorems), Memoirs of the AMS, Vol.84, Nb.426, March 1990.

  Comments:

  Problems 6.2 and 6.3 in the first reference relate to this question and explain the motivation.

---

---

Acknowledgements

I am indebted to P. Pudlak (Prague) and N. Thapen (Oxford) for comments on some of the problems.