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).
The problems are divided into four sections:
propositional logic,
bounded arithmetic,
complexity theory, and
model theory,
although there are many inter-relations.
-
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:
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:
Comments:
It holds for any P simulating F (or admiting "counting").
The problem
is also related to provability of WPHP in weak systems.
-
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.)
-
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.
-
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:
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.