CTL* and mu-calculus it is well known that the modal $\mu$-calculus is one of the most expressive temporal logics for expressing properties of trees/graphs, and that CTL* is strictly less expressive than the $\mu$-calculus.

Here I would like to ask for an example of $\mu$-calculus formula, as simple as possible, that is not expressible in CTL*, and hopefully for an explaination of its meaning (fixed-point formulas quickly become unreadable).
Any good reference for a "concrete" simple example would also be great!

Thank you in advance

Take a path property that is not first-order expressible, e.g.
$$\nu x.p\wedge\Diamond\Diamond x$$
which says that there exists a path where the atomic proposition $p$ holds at every even position, and any valuation can be used on odd positions.


Finding a finite model I know that the question "does a first order formula $\phi$ have a model" is undecidable in general.

Could anyone give me a link or a book which give the answer for finite models. If I have a first order formula $\phi$, is it decidable whether $\phi$ has a finite model? I am pretty sure that the question is well known, but I do not even know where to begin the search for an answer. (For example, I would have expected it to be in Libkin's "Elements of finite model theory", but it seems that I can not find it.)

The second part of my question is: Are there known restrictions such that the problem is decidable?

For example, the problem may become decidable for first-order formula with only monadic predicates. Or when we have monadic predicate plus a successor relation. But I cannot imagine an algorithm to decide if there exists a (finite) model over those restrictions.

The first part of your question is answered by Trakhtenbrot's Theorem.
The second part is quite a large question indeed.  Depending on the relational structure you're working on, multiple solutions can be given.  For instance, if you're interested in formal languages, MSO over word structures corresponds to regular languages, and the matching logic (see this) corresponds to CFL, and thus have their satisfiability problem decidable.

You should have a look at Chapter 14 of Libkin, where nice segments of FO are proven to have a decidable satisfiability problem, according to the amount of quantifier alternations allowed.


Efficient all pair bottleneck computation for a tree Consider a weighted tree $T = (V,E)$. The bottleneck weight for a pair of vertices $v_1,v_2 \in V$ is the highest weight of the edges on the unique path from $v_1$ to $v_2$ (if $v_1 = v_2$ it is 0). Clearly, using a simple graph traversal from a given node we can find the bottleneck weight from that node to all other nodes in $\mathcal O(|V|)$ time, so we can find all $V^2$ bottleneck weights in $\mathcal O(|V|^2)$ time.

I am interested in the situation where $V$ is large, and we are not interested in finding bottlenecks for all pairs $(v_1,v_2)$, but nonetheless for an (also large) number of pairs $Q$ (the letter $Q$ stands for queries).

I am wondering whether it is possible to do some preprocessing in less than $\mathcal O(|V|^2)$ time -- in particular, in $\mathcal O(|V|\log|V|)$ -- so that we produce some search mechanism, which will then produce a bottleneck weight for $(v_1,v_2)$ in $\mathcal O(\log |V|)$ time. Then we can produce the answer to all queries in $\mathcal O(|V|\log |V| + Q\log|V|)$.

Note that there are $\mathcal O(|V|)$ edges, and thus also that many possible answers to a query. Hence, a balanced decision tree whose leaves are the edge weights, which takes pairs of vertices and decides the highest weight edge between them -- if such a tree exists -- would do the job.

One attempt to build the tree was as follows: recursively split the original tree by removing the highest weight edge. Assign the nodes of the tree indices so that both resulting trees have indices in a contiguous range. Then make a node in the decision tree, which when given two vertices decides whether they lie in the same of the two ranges; if not, this search tree node represents the highest weight edge between the vertices; if so, continue in either of the children of the search tree node.

Unfortunately, this construction fails as the decision tree need not be balanced. Consider, for example, the tree which is just a simple path with ever decreasing weights along the path. Balancing the tree does not seem to be an option, as the decision procedures created by the balancing operations grow too fast (traversing the tree would take too long).

Any suggestions or insights are welcome.

You can even get $O(|V|)$ time if the edge weights are sorted. See the following paper:

Erik D. Demaine, Gad Landau, and Oren Weimann, “On Cartesian Trees and Range Minimum Queries”, in Proceedings of the 36th International Colloquium on Automata, Languages and Programming (ICALP 2009), Lecture Notes in Computer Science, volume 5555, Rhodes, Greece, July 5–12, 2009, pages 341–353.


Does the Category of CPOs have omega^op limits? In "Domains and Lambdi Calculi" by Amadio and Curien, in the section on solving recursive domain equations (section 7), they give sufficient conditions on a cpo-enriched category so that the category of embedding-projection pairs has $\omega$-colimits. Specifically they say it is sufficient for the category to have $\omega^{op}$-limits.

They then have a theorem that the category of CPOs has all $\omega^{op}$ limits, but the proof is incomplete and I don't see how it could be completed.

To be clear in their book the category CPO has as objects directed complete partial orders with a least element and as maps continuous (not neccesarily strict!) functions.

Their proof proceeds as follows. Given a diagram ${D_n,f_n}_{n\in\omega}$ ($f_n : D_{n+1} \to D_n)$, their proposed limit is
$$D = \{ \alpha : \Pi_{n\in\omega} D_n | \forall n, f_n(\alpha_{n+1}) = \alpha_{n} \}$$

with the pointwise ordering.
This is definitely the product of that diagram in DCPO, but I don't see why $D$ must have a least element. In particular, you can't pick $\alpha_n = \bot_n \in D_n$ since the functions $f_n$ are not assumed to be strict.

However, restricting to strict continuous functions is all they need anyway because embedding-projection pairs of CPOs are strict anyway (embedding because it's a left adjoint, projection because it's a retract of the embedding). However this doesn't seem quite right either because for example a right adjoint wouldn't necessarily have to be strict, so it seems less general.

So to summarize

Is there a way to prove $D$ is a CPO or a concrete counterexample?
If it's not, what is the right way to "fix" to their formula for solving recursive domain equations? Specifically, we do want to limit the construction to a category of CPOs since they have the bottom elements needed for recursive domain equations, but restricting to limits of strict functions seems stronger than necessary (though sufficient for my needs for now).

I know I could go back through Wand and Plotkin and Pitts and probably find the answers to (3) there, but it would be nice to have a succinct general construction like in their book chapter. Specifically I would like a reference that includes Pitt's minimal invariants work (otherwise Abramsky-Jung is probably sufficient).

Here's an attempt (please check!).

We have that $\bot_D = d$, where

$$
d_i = \bigsqcup^{D_i} \{\bot_i,f_i(\bot_{i+1}),f_i(f_{i+1}(\bot_{i+2})),\ldots\}
$$

By construction (and monotonicity), the above is the supremum of an $\omega$-chain inside $D_i$, so $d_i$ is well defined.

It is an element of $D$ since, by continuity,

$$
\begin{array}{ll}
& f_i(d_{i+1}) \\
= & f_i(\bigsqcup^{D_{i+1}} \{\bot_{i+1},f_{i+1}(\bot_{i+2}),f_{i+1}(f_{i+2}(\bot_{i+3})),\ldots\}) \\
= & \bigsqcup^{D_{i}} \{f_i(\bot_{i+1}),f_i(f_{i+1}(\bot_{i+2})),f_i(f_{i+1}(f_{i+2}(\bot_{i+3}))),\ldots\} \\
= & \bigsqcup^{D_{i}} \{\bot_i, f_i(\bot_{i+1}),f_i(f_{i+1}(\bot_{i+2})),f_i(f_{i+1}(f_{i+2}(\bot_{i+3}))),\ldots\} \\
= & d_i
\end{array}
$$

To prove that $d$ is the bottom, we take any $x \in D$, and we observe

$$
\begin{array}{ll}
& d_i \sqsubseteq x_i \\
\Leftarrow & \forall k\geq i.\ f_i \circ \cdots \circ f_k(\bot_{k+1}) \sqsubseteq x_i \\
\Leftarrow & \forall k\geq i.\ f_i \circ \cdots \circ f_k(\bot_{k+1}) \sqsubseteq f_i \circ \cdots \circ f_k (x_{k+1})\\
\Leftarrow & \forall k\geq i.\ \bot_{k+1} \sqsubseteq x_{k+1}\\
\Leftarrow & {\sf true}
\end{array}
$$


Emptiness of PDA without constructing the corresponding CFG The emptiness problem for Context free Grammars(CFG) is well studied. The same holds for the equivalence problem between Pushdown Automata (PDA) and CFGs.

Therefore, given a PDA, the straightforward way to decide whether the language it accepts is empty is to convert the PDA into a CFG and then use the known algorithm to decide emptiness of the corresponding CFG.

I am wondering whether there exists some algorithm to directly check emptiness of the language of the PDA without going through the conversion to a context free grammar.

Quick Answer: Yes, there is a really lovely algorithm that solves non-emptiness for pushdown automata that does not involve constructing the equivalent CFG.

Possible Drawback: Correct me if I am wrong, but it doesn't appear to be more efficient than the approach where you convert to a CFG.

Basic Idea: It can be viewed as a sort of dynamic programming algorithm where you solve reachability without ever constructing the possibly exponential length paths that you need to consider.

You start with a state diagram for a Pushdown Automata. Let's call a transition that doesn't manipulate the stack a resting transition. You proceed with a series of stages.

Start of Stage: You combine all compatible push and resting transitions. Next, you combine all compatible pop and resting transitions. Then, you combine all compatible pairs of resting transitions with each other.  Finally, you combine all compatible push and pop transitions.  Now, you throw in all of the new transitions into the state diagram.  End of Stage.

You go through stage after stage repeating this process.  There are only so many possible transitions.  Eventually, you either get a transition that leads from the start state to a final state or you must run out of possible transitions to add.  At this point, you know whether the automata's language is empty or not.

Question: Can you provide me with any books or papers that give a good exposition of this algorithm?  Whenever I searched for it several years ago, it seemed that this algorithm is unpopular or not well known.  I personally really like it.

Thanks for asking the question!  I really appreciate it and I hope this helps a little bit.  Have a nice day!  :)


Some nuances on Group and Subgroup Isomorphism? (1) Is it known Group Isomorphism is in $\mathsf{coNP}$ and is the conjecture so? Is there a good reference for $\mathsf{coNP}$-ness in similar situations?

(2) Is subgroup isomorphism $\mathsf{NP\text-complete}$?

(3) Is there an explicit relation between group cardinality and number of generators and bit size of generators that is used in the presentation of the group? For instance if the group has cardinality $2^{\log^cn}$ is there a bound on size and number of generators?

(1) In terms of structural complexity classes (as opposed to just upper bounds on deterministic time), for general Group Isomorphism, the known upper bounds are essentially the same as for Graph Isomorphism, namely $\mathsf{coAM} \cap \mathsf{SZK}$. However, Arvind and Toran showed that Solvable Group Isomorphism is in $\mathsf{NP} \cap \mathsf{coNP}$ under a relatively benign derandomization assumption (in particular, weaker than that currently needed to show Graph Isomorphism is in $\mathsf{coNP}$). Although this isn't general Group Isomorphism, as solvable groups are widely believed to contain the hardest cases of Group Isomorphism, this is "pretty close." As it is conjecture that $\mathsf{coAM} = \mathsf{coNP}$, it is also conjectured that Group Isomorphism is in $\mathsf{coNP}$. In the Cayley table model, many people believe that Group Isomorphism is even in $\mathsf{P}$.

(2) Subgroup Isomorphism in the Cayley table model is unlikely to be $\mathsf{NP}$-complete, as it has a quasi-polynomial time algorithm. Namely, $H$ has at most $\log_2|H|$ generators; try all possible mappings of these generators into $G$ to see if any gives an injection. This takes time $|G|^{\log_2|H| + O(1)}$.

(3) Every finite group has a generating set of size at most $\log_2|G|$ (simple exercise). For the rest of this part of the question, it really depends on how the group is presented. However, note that how the group is given as input - e.g. Cayley table, generating permutations, generating matrices, generators-and-relations, black-box - also has a significant effect on the complexity of the corresponding algorithms. It is known that there are $n^{\Theta(\log^2 n)}$ groups of order $\leq n$, so by counting, groups of order $\leq n$ in general need $\Theta(\log^3 n)$ bits to describe. It is an open question whether there is always a presentation with generators-and-relations of poly-logarithmic size.


Isomorphism Problems with Unknown Single-Exponential Algorithms Isomorphism problems come in several variants:

Group isomorphism can be solved in time $n^{O(\log n)}$
Graph isomorphism can be solved in time $n^{\log^{O(1)} n}$
Isomorphism of linear codes can be solved in time $2^{O(n)}$ ...

Where for each $n$ we assume that an isomorphism is a permutation of the set $\{1,...,n\}$. Is there a well studied variant of isomorphism problem that is known to be solvable in time $2^{O(n\log n)}$ but not in time $2^{O(n)}$?

Obs: Note that $n!\cdot n^{O(1)} = 2^{O(n\log n)}$ is roughly the time necessary to test all permutations.

A. Permutational isomorphism (aka conjugacy) of permutation groups. Input: Two lists of permutations $\pi_1, \dotsc, \pi_k, \rho_1, \dotsc, \rho_l$ Decide: Is there a permutation $\gamma$ such that $\gamma\langle \pi_1, \dotsc, \pi_k \rangle \gamma^{-1} = \langle \rho_1, \dotsc, \rho_\ell\rangle$, where $\langle \dotsc \rangle$ denotes the subgroup generated by $\dotsc$. The best known running time is $2^{O(n)}|G|$ (Babai-Codenotti-Qiao, freely available version), where the permutations are permutations on $n$ elements and $G = \langle \pi_1, \dotsc, \pi_k \rangle$. Note that $|G|$ can be as large as $n!$, so in the worst case this is $2^{O(n \log n)}$ time. Running time $2^{O(n)}$ (independent of $|G|$) is still open.

B. Group code equivalence for any group other than prime cyclic. For a group $G$, a $G$-code of length $n$ is a subgroup of $G^n$, specified by a generating set. Two such $G$-codes are equivalent if they become equal (as subgroups) after applying a permutation on the $n$ coordinates. For $G = \mathbb{Z}/p\mathbb{Z}$, this is the same as linear code equivalence and can be solved in $2^{O(n)}$ time (Babai; see Babai-Codenotti-G.-Qiao or Codenotti's freely available thesis). However, it is still open even if $G$ is a cyclic $p$-group of non-prime order, such as $\mathbb{Z}/p^2\mathbb{Z}$. Also, even doing the case of cyclic $p$-groups in time $2^{O(n)}$ (with operations in $G$ at unit cost) would have an application (see Observation 7.8 G.-Qiao).


Algorithm for extensional equality in combinator calculus I'm dealing with combinator calculus, using the $S$ and $K$ combinators as a basis. Sometimes my code generates expressions that define equivalent functions, such as
$$
(S\, K\, K) \qquad\text{and}\qquad (S\, K\, (S\, (S\, S)\, K )),
$$
which both represent the identity function, but one of them is needlessly more complicated than the other.

"Extensional equality" is the terminology used when we consider two expressions to be equal if they represent the same function in this way. I would like to know whether there is an algorithm to determine whether two expressions are in fact extensionally equal. That is, can I determine in general whether two expressions represent the same mapping?

I suspect the answer might be "no", since it feels like this is the sort of thing that should be undecidable. On the other hand, it's straightforward to determine in the case above, since the expressions $(S\, K\, K)\, x$ and $(S\, K\, (S\, (S\, S)\, K ))\, x$ both evaluate to $x$, and I'm new enough to this stuff not to trust my intuition that this can't be generalised.

I note that there is a similar question about programs in general rather than the combinator calculus, which seems to confirm my intuition that this is undecidable. There is also plenty of discussion of this issue in the context of the (untyped) lambda calculus, in which $\eta$-conversion plays a pivotal role. However, I would like to know specifically how to think about this in terms of combinator calculus.

Equality of terms in the combinator calculus is undecidable. We can encode the natural numbers as Church numerals and then show that every recursive function is represented, see for instance section 1.3.1 of Jaap van Oosten's book. I don't have any other books with me right now, but am sure almost any book on this topic will have the result, Barendregt's book surely does.

For your purposes it might be useful enough to apply a simple heuristic that will cover sufficiently many cases. You could do exactly what you suggest: see if two terms applied to a variable reduce to the same term (but you need to give up after a while).


Given a domain, how do we build a language whose denotation is the domain? Say we have an arbitrary domain $D$ with a countable basis $B$. Now, how do i build a "language" whose "denotation" lives in the domain?
My understanding is that Dana Scott initially built domains to get a model of typed lambda calculus. Then, people bgan studing domains in their own right. So if I know that something forms a domain, can I "extract computation" / "extract a language" out of it?
Perhaps said differently, does every domain $D$ [with more conditions as necessary] always come equipped with the structure of a closed cartesian category?

As it turns out, the OP is interested in the specific case of the interval domain. Martín Escardó's PhD thesis "PCF extended with real numbers: a domain-theoretic approach to higher-order exact real number computation" extends the programming language PCF with a datatype of reals whose denotation is the interval domain.


Quantum annealing vs adiabatic quantum computation I had this impression that quantum annealing is an optimization technique which may or may not produce exact solutions. On the other hand adiabatic quantum computation always gives exact solutions when it gives a solution. But this D-Wave report says as follows:

  D-Wave processors compute by piggybacking on quantum annealing. A
  quantum annealing processor can be operated as a universal quantum
  computer. In this regime of operation, the computational model is
  referred to as adiabatic quantum computation (AQC), which can be
  thought of as the long-time limit of quantum annealing.

Should I think that adiabatic quantum computation is an application of quantum annealing?

Adiabatic quantum computing (AQC) is a computational model (as Peter said in the comments). Compare AQC with other models of computation such as:

circuit-based quantum computing (CBQC)
Adleman-Lipton model (a model for computing using DNA)
Turing machine model (a model where computations are done with symbols on a tape)

One can devise algorithms using the AQC model, such as this algorithm for factoring integers: http://arxiv.org/abs/1411.6758.

Quantum annealing is a physical process which attempts to implement such algorithms. Start with a set of quantum states, and a time-dependent Hamiltonian $H(t)$ such that the ground state of $H(t_F)$ at a final time $t_F$, encodes the solution to your problem. Let the states evolve according to $H(t)$, and hope that in the end one of the candidate states ends up in the ground state of $H(t_F)$.

If you're lucky enough to have a qubit that starts in the ground state of $H(0)$, and $H(0)$ evolves into $H(t_F)$ slowly enough, then according to the "adiabatic theorem", the qubit always remains in the ground state of $H(t)$ for all $t$, and you are guaranteed to get the right answer which is encoded in the ground state of $H(t_F)$. This is what the AQC model has in mind, but since it is experimentally difficult to start in the ground state, we sometimes try to implement AQC algorithms using quantum annealing, which unfortunately might not end up in the ground state.


Can we recover integers $a_i$ from the sum $a_0 + a_1e+a_2e^2+\cdots+a_ne^n$? Since $e$ is transcendental, the function $f:\mathbb Z_{\geq 0}^{n+1}\to \mathbb R$ is injective,
$$ f(\underset{\text{Integers}\ \geq\ 0}{\underbrace{a_0,a_1,\ldots, a_n}}) = a_0 + a_1e+a_2e^2+\cdots a_ne^n$$
Since $f$ is injective, in principle, the numbers $a_i$ can be deduced given the output of $f$.
And since the numbers $a_i$ are non-negative, any interval of the real numbers intersects the codomain of $f$ on only finitely many points.$^*$
I'm wondering whether, in practice, the integer coefficients $a_i$ can be recovered from the value of $f$. Does it suffice to have only polynomially many (in $n$) bits of $f$? (i.e., polynomial in $n$). And can this be done in polynomial time?
There is an exponential-time algorithm, namely: Simply enumerate all $a$ for which $f(a)\leq t$ for a given target value $t$. In fact, in my application I know that $a_0+a_1+\cdots +a_n = 2^n$, so the enumeration is quite simple.

I have the same question for
$$g(a_0,a_1,\ldots, a_n) = \sum_{k=0}^ne^{\frac{i\pi}{p}k}a_k$$
In my application, I can choose $p$, e.g., a prime with $2n<p$, so that the contributions all lie in the north-east region of the complex plane.
$^*$ (Thanks to Emil Jerabek for pointing out that, without that constraint, $f$ cannot be computed from finitely many bits).

This is impossible. No finite number of bits of $f(a_0,\dots,a_n)$ suffices to determine any of $a_0,\dots,a_n$; in fact, any nondegenerate real interval contains the values $f(a_0,\dots,a_n)$ for infinitely many vectors $(a_0,\dots,a_n)\in\mathbb Z^{n+1}$, and this holds even you fix all but two of the $a_0,\dots,a_n$ in advance.


Why does most cryptography depend on large prime number pairs, as opposed to other problems? Most current cryptography methods depend on the difficulty of factoring numbers that are the product of two large prime numbers. As I understand it, that is difficult only as long as the method used to generate the large primes cannot be used as a shortcut to factoring the resulting composite number (and that factoring large numbers itself is difficult).

It looks like mathematicians find better shortcuts from time to time, and encryption systems have to be upgraded periodically as a result. (There's also the possibility that quantum computing will eventually make factorization a much easier problem, but that's not going to catch anyone by surprise if the technology catches up with the theory.)

Some other problems are proven to be difficult. Two examples that come to mind are variations on the knapsack problem, and the traveling salesman problem.

I know that Merkle–Hellman has been broken, that Nasako–Murakami remains secure, and that knapsack problems may be resistant to quantum computing. (Thanks, Wikipedia.) I found nothing about using the traveling salesman problem for cryptography.

So, why do pairs of large primes seem to rule cryptography?

Is it simply because the it is currently easy to generate pairs of large primes that are easy to multiply but difficult to factor?
Is it because factoring pairs of large primes is proven to be difficult to a predictable degree that is good enough?
Are pairs of large primes useful in a way other than difficulty, such as the property of working for both encryption and cryptographic signing?
Is the problem of generating problem sets for each of the other problem types that are difficult enough for the cryptographic purpose itself too difficult to be practical?
Are the properties of other problem types insufficiently studied to be trusted?
Other.

Boaz Barak addressed this in a blog post

My takeaway from his post (roughly speaking) is that we only know how to design cryptographic primitives using computational problems that have some amount of structure, which we exploit. With no structure, we don't know what to do.  With too much structure, the problem becomes efficiently computable (thus useless for cryptographic purposes). It seems that the amount of structure has to be just right.


Edge-partitioning into rainbow triangles I'm wondering if the following problem is NP-hard.

  Input: $G = (V,E)$ a simple graph, and a coloring $f : E \to \{1,2,3\}$ of the edges
  ($f$ does not verify any specific property).

  Question: is it possible to partition $E$ into $|E|/3$ triangles,
  such that each triangle has one edge of each color?

I know that without the colors the problem of "edge partitioning" a graph into
$K_n$, $n \geq 3$ is NP-hard
(see The NP-Completeness of Some Edge-Partition Problems)
but with the colors I don't know.

I would also be interested in a result for edge partitioniong into rainbow $K_c$, with $c$ a constant. Of course, in this case the problem becomes:

  Input: $G = (V,E)$ a simple graph, and a coloring $f : E \to \{1,\ldots,c(c-1)/2\}$ of the edges ($f$ does not verify any specific property).

  Question: is it possible to partition $E$ into $|E|/(c(c-1)/2)$ $K_c$'s,
  such that each clique $K_c$ has one edge of each color?

I followed the link in the question, and the reduction there actually produces graphs whose edges have a natural coloring such that each $K_n$ present in the graph is a "rainbow $K_n$" (has exactly one edge of each color). In other words, we can easily adjust the reduction in that paper so that it reduces to your problem instead of reducing to the partition into $K_n$s problem: simply assign each edge a color according to this natural coloring and then the graph can be partitioned into "rainbow $K_n$s" if and only if it could be partitioned into $K_n$s at all.

The basic structure of the reduction in that paper can be accomplished with the following 3 steps:

Create many copies of a particular graph $H_{n,p}$.
Identify certain pieces of some copies of $H_{n,p}$ with each other (i.e. merge vertices/edges between multiple different copies of $H_{n,p}$).
Remove certain vertices/edges from some copies.

The graph $H_{n,p}$ has as its vertices the set of length-$n$ vectors modulo $p$ for which the components add to $0$ mod $p$. The edges connect every two vertices that differ in only two components with differences of $+1$ and $-1$ in those two components.

I propose the following coloring for this graph: assign a color to each edge according to its direction. If $x$ and $y$ are adjacent vertices, then $x-y$ is a vector with $n-2$ components equal to $0$, one component equal to $1$ and one component equal to $-1$. In other words, for every edge $(x, y)$ there are ${n \choose 2}$ options for which components of $x-y$ are non-zero. If we assign a unique color to each of these options then we have a coloring for all the edges such that every edge in the same direction has the same color. It is pretty easy to verify that no two edges in a $K_n$ in $H_{n,p}$ are in the same direction. Therefore every $K_n$ in $H_{n,p}$ is a rainbow $K_n$ under this coloring.

When we follow the reduction, we use this coloring for every copy of $H_{n,p}$. Therefore at the end of step 1 in the list above, every $K_n$ in the graph is a rainbow $K_n$.

In step 2 of the above list, we identify some vertices/edges with each other. In particular, in the reduction we always identify a $K_n$ with another $K_n$. But in this situation (where all the $K_n$s are from a copy of $H_{n,p}$), every $K_n$ is either a translation of the "standard $K_n$" which the paper calls $K$ or a translation of $-K$. Therefore, we are either identifying two parallel $K_n$s or two $K_n$s that are "flips" of each other. In either case, the edges that are identified across the two $K_n$s are parallel and are therefore the same color. For example, see Figure 2 in the paper; edges that are identified are always parallel. Thus, since we never try to identify two edges of different colors, the coloring at the end of step 1 in the above list can be naturally extended into a coloring at the end of step 2. Identifying certain vertices/edges together doesn't create any new $K_n$s, so it is still the case at the end of this step that every $K_n$ is a rainbow $K_n$.

Finally in step 3 we remove some vertices/edges, which also doesn't create any new $K_n$s. Thus, we have our desired property: under the coloring I provided, every $K_n$ in the graph generated by this reduction is a rainbow $K_n$.


Is it enough to sort for polynomially many 0-1 sequences for a sorting network? The 0-1 principle says that if a sorting network works for all 0-1 sequences, then it works for any set of numbers.
Is there an $S\subset \{0,1\}^n$ such that if a network sorts every 0-1 sequence from S, then it sorts every 0-1 sequence and the size of $S$ is polynomial in $n$?

For example, if $S$ consists of all sequences where there are at most $2$ runs (intervals) of 1's, then is there a sorting network N and a sequence that is not ordered by N if all members of $S$ are ordered by N?

Answer: As can be seen from the answer and the comments to it, the answer is that for every unsorted string there is a sorting network that sorts every other string.
A simple proof for this is the following.
Let the string $s=s_1\ldots s_n$ be such that $s_i=0$ for ever $i<k$ and $s_k=1$.
Since $s$ is unsorted, after sorting $s_k$ should be $0$.
Compare $k$ with every $i$ for which $s_i=1$.
Then compare every pair $(i,j)$ such that $i\ne k$ and $j\ne k$ many times.
This leaves the whole string sorted, except possibly for $s_k$, which is unsorted for $s$, and for certain other strings that have more $1$'s than $s$.
Now compare $s_k$ for $i=n$ downto $1$ except for the place where $s_k$ should go in $s$.
This will sort everything but $s$.

Update: I wonder what happens if we restrict the depth of the network to $O(\log n)$.

It seems not.  Ian Parberry makes reference to a paper by Chung and Ravikumar, where they supposedly give a recursive construction of a sorting network that sorts every bitstring but one, and further deduce that the problem of verifying a sorting network is $co$-$NP$ complete.  I can't find the original paper right away, but certainly it matches (my) intuition.

Edit to add: It is actually very easy to find such a network that misses exactly one string.  The string to be missed will be $(1,0,\ldots,0)$.  Now you just want a circuit that sorts the last $n-1$ bits, then sorts the first $n-1$ bits.  This circuit will sort anything with at least two $1$s, will obviously sort the all-zero string, and will sort any string starting with $0$.


What kind of theoretical object corresponds to a C++ concept? I am lacking a background in theoretical computer science but I would have liked to understand to what kind of theoretical objects C++ concepts corresponds to. Basically, C++ concepts allow to define a set of types that satisfy a list of constraints. So, from a theoretical standpoint, what C++ concepts correspond, or roughly correspond (and in that case what are the differences), to?

From a programming language theory perspective, as opposed to the computability perspective other answers and comments have offered, C++ templates combined with concepts correspond to bounded polymorphism or constrained genericity. Concepts themselves correspond to the constraints or bounds placed on a type.

A template is type-level function, parameterised by type that are constrained by a concept to implement a particular interface. When the template is applied to a type satisfying that concept, a new type results.

Templates+concepts are analogous to generics in Java, Scala or Eiffel. They differ from templates in earlier C++ because they allow constraints on the type parameters to be specified and checked, whereas C++ templates did not allow that. The benefit is better static checking that the program after applying the template will be well typed.

A good reference is Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press, Chapter 26: Bounded quantification.


Do algorithms for solving parity games ignore other possible strategies for player V after finding one? Solving parity games (from a "start" node) relies on the existence of a history-free winning strategy for player 0 (V) or 1 (R). Whether there is more than one such strategy is probably never discovered, is it? Are there algorithms to keep searching even after discovering one appropriate strategy, i.e. searching for more than one (say all possible) strategies?

Parity games can be reduced to discounted payoff games. See, e.g.,

Marcin Jurdziński (1998). Deciding the winner in parity games is in UP ∩ co-UP. Information Processing Letters 68:3 119-124.

As explained in that paper (and first observed by Zwick and Paterson, I believe), there are min/max optimality equations for discounted payoff games with a unique solution that assigns a "value" to each state. From these values, it is easy to read off all optimal strategies of the players.

Discounted payoff games can in turn can be solved as a P-matrix Linear Complementarity Problem (LCP), where the reduction uses the optimality equations and from a solution to the LCP one could again read off all optimal strategies. See,

Marcin Jurdziński and Rahul Savani (2008). A simple P-matrix linear complementarity problem for discounted games. Computability in Europe (CiE), 283-293.

Now in the following paper a discrete strategy improvement algorithm for parity games is given that essentially defines and uses optimality equations.

Jens Vöge and Marcin Jurdziński (2000). A Discrete Strategy Improvement Algorithm for Solving Parity Games. Computer-aided Verification (CAV).

It's very possible you could read off all strategies from a "solution" to those optimality equations, e.g., obtained via their algorithms - but, I am not sure.


The simple proof of uniqueness of solution for The tower of Hanoi problem The problem of Tower of Hanoi is a typical example of recursion method.
Could anyone show me the (simple) proof of

(1) the smallest number of moves of the solution is 2^n-1

(2) the uniqeness of the optimal solution (the solution with the smallest number of moves)

(I found (1) in the Concrete Math of Knuth, is there any other proof ?)

Without knowing the proof you mention or being very formal, I'd go for the combined one below.

With induction: For the case $n=1$, it is easy to see that you need at least one step to do anything and if you enumerate the possible steps you'll get that there is precisely one step that moves the tower to the right place.

For the case $n=m+1$, for some $m\ge 1$, looking at the bottom stone it is clear that it can only be moved after all others are moved elsewhere first. To move the bottom stone there are two options, one of which puts it where it needs to be in the end, but in both cases it can only move if the target "site" is empty. This leaves only one place for all the other stones to be, and by the rules of the game they have to be in order and thus form a tower. This means the top has to be moved as a whole from one place to another. So in both cases the smallest number of moves is the smallest number of moves to move the top (of size $m$) completely, which is $2^m-1$ and unique by induction, plus $1$ for the bottom stone, giving $2^m$ so far.

Now we are left with two cases. For the one where the bottom stone is already in place, we have a tower of size m elsewhere that needs to be moved on top of it. Moving the bottom stone itself either gives use a previous state or the same state as the following case and these paths can therefore not be minimal. To move the top we know, again by induction, that the smallest number of moves is $2^m-1$ and that the moves are unique. The total number of moves in this case therefore is $2^m+2^m-1=2^{(m+1)}-1=2^n-1$.

In the other case we know that we still have to move the bottom stone to the right place and in fact we can easily see that the current case is effectively the same as the situation before the bottom stone was moved there (but after the top was moved). The last move being superfluous means this path cannot lead to a minimal number of moves. This leaves the previous case as the only suitable case.


Finding even cycle in directed graphs Given a directed graph, we want to decide whether it contains a directed cycle of even length. This 1997 paper by YUSTER and ZWICK states that the problem is not known to be in $P$ nor is it known to be $NP$-complete.

  Is there any recent result that resolves the complexity of the even cycle problem in directed graphs?

Yes, a polynomial time algorithm was first given in:

Neil Robertson, P. D. Seymour, Robin Thomas. "Permanents, Pfaffian orientations, and even directed circuits." Annals of Mathematics 150.3 (1999): 929-975. arXiv

edit: Actually, according to the acknowledgements section of the above paper, the result was first obtained by McCuaig who later published it as:

William McCuaig. "Pólya's Permanent Problem." Electr. J. Comb. 11(1) (2004) http://www.combinatorics.org/ojs/index.php/eljc/article/view/v11i1r79


Does every online algorithm has an offline counterpart? According to the wikipedia page for Online algorithms, it states:

  "Not every online algorithm has an offline counterpart."

At the time of asking this question there is no citation for this claim.
How it possible to not have an offline counterpart? What is an example of an  algorithm that is online only?

This statement seems false to be because of the notion of competitive ratio that is used to analyze virtually all online algorithms. Heuristically the competitive ratio measures how well the online algorithm performs on a sequence of inputs versus an adversary that knows the sequence in advance. In particular, the adversary is solving an offline problem.

If you look at any of the online problems that are studied, they all use the competitive ratio as a benchmark. To back up this claim, look at the abstracts of any paper in a well known journal (such as SODA 18: https://archive.siam.org/meetings/da18/da18_abstracts.pdf) and search for abstracts that study online algorithms. They all use some type of competitive ratio in their analysis.


Exhausting Simulator of Zero-Knowledge Protocols in the Random Oracle Model In a paper titled "On Deniability in the Common Reference String and Random Oracle Model," Rafael Pass writes:

  We note that when proving security according to the standard zero-knowledge definition in the RO [Random Oracle] model, the simulator has two advantages over a plain model simulator, namely,

  The simulator can see what values parties query the oracle on.
  The simulator can answer these queries in whatever way it chooses as long as the answers "look" OK.

The first technique, namely the ability to "monitor" queries to the RO, is very common in all papers referring to the concept of zero-knowledge in the RO model.

Now, consider the definition of black-box zero-knowledge (PPT stands for probabilistic, polynomial-time Turing machine):

$\exists$ a PPT simulator $S$, such that $\forall$ (possibly cheating) PPT verifier $V^*$, $\forall$ common input $x\in L$, and $\forall$ randomness $r$, the following are indistinguishable:

the view of $V^*$ while interacting with the prover $P$ on input $x$ and using randomness $r$;
the output of $S$ on inputs $x$ and $r$, when $S$ is given black-box access to $V^*$.

Here, I want to exhibit a cheating verifier $V'$, whose job is to exhaust any simulator which tries to monitor RO queries:

Let $S$ be the simulator guaranteed by the existential quantifier in the definition of black-box zero-knowledge, and let $q(|x|)$ be a polynomial which upper-bounds the running time of $S$ on input $x$. Assume that $S$ tries to monitor the queries of $V^*$ to the RO.

Now, consider a cheating $V'$, which first queries the RO for $q(|x|)+1$ times (on arbitrary inputs of its choice), and then acts arbitrarily maliciously.

Obviously, $V'$ exhausts the simulator $S$. A simple way for $S$ is to reject such malicious behavior, yet that way, a distinguisher can easily distinguish the real interaction from the simulated one. (Since in the real interaction, the prover $P$ cannot monitor $V'$'s queries, and thus won't reject based on the mere fact that $V'$ is querying too much.)

  What is the workaround for the above problem?

Edit:

A good source for studying ZK in the RO model is:

Martin Gagné, A Study of the Random Oracle Model, Ph.D. Thesis, University of California, Davis, 2008, 109 pages. Available on ProQuest: http://gradworks.umi.com/33/36/3336254.html

Particularly, it gives definitions of black-box ZK in the RO Model in section 3.3 (page 20), attributed to Yung and Zhao:

Moti Yung and Yunlei Zhao. Interactive Zero-Knowledge with Restricted Random Oracles.  In Theory of Cryptography - TCC 2006, LNCS 3876, pp. 21-40, 2006.

There is a question of why one would want to define black-box ZK in the random oracle model.
There are at least two reasons why people suggested the definition of black-box zero knowledge:

1) For a positive result, when you say that a simulator is "black-box zero knowledge" it automatically gives you a nice bound on its running time (i.e., $poly(|x|) \cdot time(V*)$ as opposed to $poly(time(V*))$) and it also may be useful to know that the simulator doesn't "look at the guts' of $V*$ and doesn't care if $V*$ is implemented using RAM, circuit, etc... While a random-oracle model simulator may be efficient, it's obviously not black-box, because it's supposed to somehow look at the execution of $V*$ and understand from it when $V*$ is evaluating a hash function. For this reason, there is a sense in which it doesn't make sense to say that a random-oracle model simulator is "black-box".

2) For a negative result, people use "black-box simulator" to capture a large class of proof techniques. In this case you can define black-box simulator also in the random oracle model and the definition that makes sense is what David said. In fact, for a negative result even not in the random oracle model, it's best if the result holds even if you allow the simulator $poly(time(V*))$ running time. Indeed, although it's not always stated, the negative results I'm aware of all have this property, since the cheating verifier $V*$ is typically a fixed polynomial algorithm that runs some pseudorandom functions, while the simulator can have any polynomial running time.


Complete axiomatization of relation algebras without ${}^-$ and $\top$ I'm working on a more thorough algebraic treatment of delta modeling. Briefly, deltas are syntactic entities that can modify products (as in 'software products'). They actually represent relations on products, so that they could be both partially defined and non-deterministic.

I've been looking into relation algebras. For obvious reasons they seemed like a good place to start.

A relation algebra is a structure $(S, \vee, \wedge, {}^-, \bot, \top, \cdot, \epsilon, {}^\smallsmile)$ with disjunction, conjunction, negation, an empty element, a complete element, composition, a neutral element and converse. Semantically they correspond to the relation operations $(2^{P^2}, \cup, \cap, {}^{\mathsf C}, \varnothing, P^2, \circ, \mathrm{id}_P, {}^{-1})$.

But this is more expressiveness than I need. If I could just remove negation $^-$ and the complete element $\top$, the operations that remain have sensible interpretations for delta modeling. Moreover, it seems that in contrast to $^-$ and $\top$, the operations that remain are in a sense 'constructive' (though I'm not sure the term is apt here), since their meaning does not depend on the description of the full set of products $P$.

Has the structure $(S, \vee, \wedge, \bot, \cdot, \epsilon, {}^\smallsmile)$ been studied? Is there a complete axiomatization for it (with respect to the behavior of the corresponding relation operations)? Does it have a decidable theory?

Edit: I've discovered the work of Hajnal Andréka and Szabolcs Mikulás. In particular the article entitled Axiomatizability of positive algebras of binary relations (a PDF version can be found with Google).

This article seems to summarize some of the results I need. If I understand correctly, the exact structure I describe is not finitely axiomatizable, but it will be if I also remove either $\wedge$, $\cdot$ or ${}^\smallsmile$. Moreover, any signature without that combination, but with $\cdot$ and either $\vee$ or $\wedge$, is finitely axiomatizable.

However, I'm not well-versed enough yet in abstract algebra to write up a coherent answer myself. For example, I don't understand why the presence of $\vee$ or $\wedge$ is required. If I omit both, aren't we simply in monoid territory? And I also still don't know about a decidable theory.

So I would still appreciate it if someone with more experience could write up an answer, preferably one that is easier to understand for the layman than the above cited article.

The equational theory of the signature $S=\{\vee,\wedge,.,\epsilon,^\smile\}$ is decidable. See this paper by Andréka and Bredikhin.
The idea is to associate to every term $t$ over $S$ a graph $G_t$. Then Andréka and Bredikhin show that two terms $t$ and $u$ are equivalent iff there is a graph homomorphism from $G_t$ to $G_u$ and a graph homomorphism from $G_u$ to $G_t$. Testing graph homomorphism between finite graphs is decidable, hence the equational theory is also decidable.
The equational theory of $S$ is not finitely axiomatizable, due to the paper of Andréka and Mikulas you have cited. However, contrarily to what is claimed in this paper, the restrictions of the signature to, say, $\{., \cap, \epsilon\}$ is not finitely axiomatizable, as shown in this paper.


What podcast should everybody listen to? This list was inspired by the lists:

What are the popular science books that inspire TCS?
What Books Should Everyone Read?
What papers should everyone read?
What videos should everybody watch?

I don't know if there are a lot of podcasts about Theoretical Computer Science, but if you have something that is relevant to that list it will be very good.

Simons Institute for the Theory of Computing:
https://www.youtube.com/user/SimonsInstitute/featured
Institute for Advanced Study:
https://www.youtube.com/user/videosfromIAS/featured
Prinston TCS:
https://www.youtube.com/channel/UCyGLYDvZ5BD5oYCIVv995HA/featured
Stanford Computer Science Theory:
https://www.youtube.com/user/StanfordCSTheory/featured
Innovations in theoretical computer science 2020:
https://www.youtube.com/watch?v=LBEzB8M6F5A&t=137s
DIMACS:
https://www.youtube.com/channel/UCTKhyhoEPYyjU9PFW99A6Qw


Comparing the Kolmogorov complexity of theories Chaitin's incompleteness theorem says no sufficiently strong theory of arithmetic can prove $K(s) > L$ where $K(s)$ is the Kolmogorov complexity of string $s$ and $L$ is a sufficiently large constant. $L$ is sufficiently large if it is larger than the size in bits of a proof checking machine (PCM). A PCM for theory $T$ takes a string encoded as an integer as input and outputs a 1 if the string is a valid proof in the language of $T$.

Assume that $L(T) > |PCM_T|$ for theory $T$ is an upper bound for the complexity of $T$. Consider the following hierarchy of theories: Let the base theory be Robinson arithmetic ($Q$). Augment $Q$ with increasingly stronger axioms of polynomial bounded induction. Let $Q^*$ be the theory of theorems provable with $Q$ and any of these bounded induction axioms. Assume we can define $L(Q)$ and $L({Q^*})$ by defining PCM's for each theory.

I want to consider an enhanced proof checking machine (EPCM) for $Q^*$. This EPCM takes a string as input just like an ECM and has a second input which defines the rank and level of a sub-theory of $Q^*$. If the input string is a valid proof in $Q^*$ the EPCM then goes through the steps of the proof to determine the highest rank and level of induction used. This EPCM then writes a 1 if the input sentence is a valid proof in the specified sub-theory of $Q^*$.

Is the enhanced proof checker I describe feasible? If so, would the size of this EPCM be an upper bound not just for the complexity of $Q^*$, but also an upper bound on the complexity of any sub-theory of $Q^*$?

Is it reasonable to say there is a constant upper bound on the complexity of $Q^*$ and all of its sub-theories?

This question was inpired by Nelson's failed proof of the inconsistency of arithmetic. I didn't point this out earlier because some people find that proof disturbing. My motivation is to ask an interesting question. CSTheory seems to be the right forum for this question. The complexity of $Q^*$ and all of its sub-theories is either bounded by a constant or unbounded. Either answer leads to more questions.

If the complexity of the sub-theories is unbounded we can ask questions like what is the weakest sub-theory of $Q^*$ more complex than $Q^*$? Or more complex than PA and ZFC? Thinking about this question has already shown me there is a severe limit on how much a theory can prove about the Kolmogorov complexity of strings. If $Q^*$ is consistent then none of its sub-theories can prove $K(s) > L(Q^*)$ for any string. This means even really strong sub-theories can't prove there are more complex strings than some much weaker sub-theory where the weaker theory is more complex than $Q^*$.

I'll try and give an answer to this question, and try to clear up some confusion as to the exact form of the question.

The first point I want to make: the $L$ in the statement of Chaitin's constant is indeed a function of $T$. In the absolute sense, it is monotonic in the expressiveness of $T$: if $L(T)$ is the smallest natural number for which
$$T\not\vdash K(s)\geq L(T)$$
for any string $s$, then if $T'$ is a consistent theory stronger than $T$ ($T\vdash\varphi$ implies $T'\vdash\varphi$ for any arithmetic sentence $\varphi$) then $L(T')\geq L(T)$. The argument is very simple: if there exists $s$ such that $T\vdash K(s)\geq L$ then $T'\vdash K(s)\geq L$ by hypothesis.

However, this is only true if $L(T)$ is the absolute Chaitin constant. In particular, if $T'$ proves $\mathrm{Con}(T)$, then
$$ T'\vdash \exists L\forall s\ \lceil T\not\vdash K(\overline{s})\geq \overline{L}\rceil $$

by internalizing Chaitin's argument. However, a concrete $l$ for which

$$ T'\vdash\forall s\ \lceil T\not\vdash K(\overline{s})\geq\overline{l}\rceil$$

will in general not be equal to $L(T)$. In particular it may be much larger, generally proportional to the size of the proof of $\mathrm{Con}(T)$ in $T'$. This can easily be seen in the proof of the theorem itself, which crucially relies on the consistency of $T$.

So while $Q^*$ can prove consistency of the system with bounded induction, the length of these proofs gets longer the closer you get to $Q^*$ in expressiveness (one way to understand the incompleteness theorems is that the length becomes infinite when you reach $Q^*$, thus it has no finite proof of consistency in $Q^*$ itself). Thus the same applies to the various upper bounds on the internal $L(T)$s $Q^*$ can describe for each sub-theory.

So here is the short answer to your question: $L(T)$ is bounded uniformly for all subtheories of $Q^*$, but $Q^*$ itself cannot show that this bound holds for all such sub-theories. This was the crucial mistake Nelson made (buried under several layers of formalism) and that Tao pointed out here.


Encoding quadratic constraints in a constraint satisfaction problem into SAT It seems like most constraint satisfaction problems can be posed in terms of SAT.

The question is two fold:

How can any CSP with quadratic constraints be framed as a
satisfiability instance
Is there an algorithm which performs this
transformation.

This of course depends on the type of satisfaction problems you are trying you encode in SAT. Assuming the general case, where your problem falls into the class of problems that can be handled by some existing encoding techniques (a review of some techniques can be found in [1]), some techniques are specific to support encoding quadratic constraints (and arithmetic operations such as multiplication, in general):

1) Some of the approaches for encoding quadratic constraints, as well as other form of constraints that involve arithmetic operations, into SAT include encoding techniques often referred to as 'bit blasting' or such as the ones based on sparse encoding:

Bit blasting is a commonly used decision procedure for bit-vector arithmetic. Essentially, the idea is to represent bit-vector terms with vector of Boolean variables and emit constraints on the bits of those vectors depending on the constants and operations used in the formula, where arithmetic operations are encoded as "circuits", which effectively put constraints for every bit of the resulting vector. (More information about this technique can be found e.g. in [2]).
Sparse encoding (of integers) is an approach, interestingly different from bit blasting, which avoids using circuits by trying to precompute possible integer values and using guards in the encoding to designate when can a term hold a specific value (depending on the structure of the constraint and possible starting values). Such a technique might be superior to bit blasting for cases of considering smaller integer domains. (More details and the discussion about benefits of using this approach is presented in [3].)

2) There exist different ways of leveraging techniques such as bit blasting and sparse encoding for the purpose of encoding different (CSP) problems into SAT, while some of the mentioned literature directly suggests plausible algorithms: a standard approach for a translating algorithm is described in [2], while the algorithm that relies on sparse encoding is implemented in a software synthesizer Sketch, and described in detail through examples in [4].

[1] Walsh, Toby. "Sat v csp." International Conference on Principles and Practice of Constraint Programming. Springer Berlin Heidelberg, 2000.

[2] Kroening, Daniel, and Ofer Strichman. Decision procedures: an algorithmic point of view. Springer Science & Business Media, 2008.

[3] Solar-Lezama, Armando. Program synthesis by sketching.

[4] Solar-Lezama, Armando. "Program sketching." International Journal on Software Tools for Technology Transfer 15.5-6 (2013): 475-495.


On $\#P\subseteq FP^{\Sigma_{f(n)}^P}$? Is it known that permanent of a $0/1$ $n\times n$ matrix $M$ is computable in polynomial or randomized polynomial time with access to a ${\Sigma_{(\log n)^c}^P}$ oracle where $0<c$ holds and $\Sigma_{f(n)}^P$ means the number of alternations is $f(n)$?
If not known what is the consequence if it is possible to do so?

This is very unlikely to hold, but (as usual) impossible to rule out using current techniques, as we can’t even prove $\mathit{PSPACE}\ne P$.

However, we can at least show that no relativizing argument proves such an inclusion, i.e., there are oracles $X$ such that randomized polynomial-time with a $(\Sigma^P_{(\log n)^c})^X$ oracle does not include $\#P^X$. Better yet, there are oracles where it does not even include $\oplus P^X$ (which is included in $P^{\#P^X}$): otherwise, there would exist $O((\log\log n)^c)$-depth quasipolynomial-size unbounded fan-in circuits that approximate parity with error, say, $1/4$, contradicting Håstad’s theorem.


Can such a matrix exist? During my work i came up with the following problem:

I am trying to find an $n \times n$ $(0,1)$-matrix $M$, for any $n > 3$, with the following properties:

The determinant of $M$ is even.
For any non-empty subsets $I,J\subseteq\{1,2,3\}$ with $|I| = |J|$, the submatrix $M^I_J$ has odd determinant if and only if $I=J$.

Here $M^I_J$ denotes the submatrix of $M$ created by removing the rows with indices in $I$ and the columns with indices in $J$.

So far, I tried to find such a matrix via random sampling but I am only able to find a matrix that has all properties except the first one, i.e., the matrix always has an odd determinant. I tried various dimensions and different input/output sets without any success. So this makes me think:

Is that there is a dependency among the requirements, which prevents them from being simultaneously true?

or

Is it possible that such a matrix exists and can someone give me an example?

Thanks,
Etsch

No such matrix exists.

The Desnanot-Jacobi identity says that for $i \neq j$,
$$
\det M_{ij}^{ij} \det M = \det M_i^i \det M_j^j -\det M_i^j \det M_j^i
$$
so using this, we get
$$
\det M_{12}^{12} \det M = \det M_{1}^{1} \det M_{2}^{2} - \det M_{1}^{2} \det M_{2}^{1}
$$
But your requirements force the left-hand-side to be 0 (mod 2) and the right-hand-side to be 1 (mod 2), showing they are incompatible.


Subgraph isomorphism with a tree If we have a large (directed) graph $G$ and a smaller rooted tree $H$, what is the best known complexity for finding subgraphs of $G$ isomorphic to $H$?  I am aware of results for subtree isomorphism where both $G$ and $H$ are trees and also where $G$ is planar or has bounded treewidth (and others) but not for this graph and tree case.

The question whether any fixed graph $H$ is an (induced) subgraph of $G$ is a first-order definable property, i.e., for every $H$ there is a formula $\varphi_H$ ($\psi_H$) such that $H$ is an (induced) subgraph of $G$ if and only if $G \models \varphi_H$ ($G\models\psi_H$).

It was formerly known that the model-checking problem is fixed-parameter tractable on classes of graphs that (locally) exclude a minor and on classes of (locally) bounded expansion. Recently, Grohe, Kreutzer and S. anounced an even more general meta-theorem, stating that every first-order property can be decided in almost linear time on nowhere dense classes of graphs.

For your question this implies the following. Let $H$ be a fixed rooted tree. Then it can be decided in linear time whether $H$ is an (induced) subgraph of an input (directed or undirected) graph $G$ if $G$ is planar, or more generally is from a class that excludes a minor or from a class of bounded expansion. The problem can be decided in almost linear time if $G$ is from a class that locally excludes a minor or from a class of locally bounded expansion or most generally, $G$ is from a nowhere dense class of graphs.


Which interesting theorems in TCS rely on the Axiom of Choice? (Or alternatively, the Axiom of Determinacy?) Mathematicians sometimes worry about the Axiom of Choice (AC) and Axiom of Determinancy (AD).

Axiom of Choice: Given any collection ${\cal C}$ of nonempty sets, there is a function $f$ that, given a set $S$ in ${\cal C}$, returns a member of $S$.

Axiom of Determinacy: Let $S$ be a set of infinitely long bit strings. Alice and Bob play a game where Alice picks a 1st bit $b_1$, Bob picks a 2nd bit $b_2$, and so on, until an infinite string $x = b_1 b_2 \cdots $ is constructed. Alice wins the game if $x \in S$, Bob wins the game if $x \not \in S$. The assumption is that for every $S$, there is a winning strategy for one of the players. (For example, if $S$ consists only of the all-ones string, Bob can win in finitely many moves.)

It is known that these two axioms are inconsistent with each other. (Think about it, or go here.)

Other mathematicians pay little or no attention to the use of these axioms in a proof. They would seem to be almost irrelevant to theoretical computer science, since we believe that we work mostly with finite objects. However, because TCS defines computational decision problems to be infinite bit strings, and we measure (for example) the time complexity of an algorithm as an asymptotic function over the naturals, there is always a possibility that the usage of one of these axioms could creep into some proofs.

What is the most striking example in TCS that you know where one of these axioms are required? (Do you know any examples?)

Just to foreshadow a bit, note that a diagonalization argument (over the set of all Turing machines, say) is not an application of the Axiom of Choice. Although the language that a Turing machine defines is an infinite bit string, each Turing machine has a finite description, so we really don't require a choice function for infinitely many infinite sets here.

(I put a lot of tags because I have no idea where the examples will come from.)

Any arithmetical statement provable in ZFC is provable in ZF, and hence does not "need" the axiom of choice.  By an "arithmetical" statement I mean a statement in the first-order language of arithmetic, meaning that it can be stated using only quantifiers over natural numbers ("for all natural numbers x" or "there exists a natural number x"), without quantifying over sets of natural numbers.  At first glance it might seem very restrictive to forbid quantification over sets of integers; however, finite sets of integers can be "encoded" using a single integer, so it's O.K. to quantify over finite sets of integers.

Virtually any statement of interest in TCS can, with perhaps a bit of finagling, be phrased as an arithmetical statement, and so doesn't need the axiom of choice.  For example, $P\ne NP$ looks at first glance like an assertion about infinite sets of integers, but can be rephrased as, "for every polynomial-time Turing machine, there exists a SAT instance that it gets wrong," which is an arithmetical statement.  Thus my answer to Ryan's question is, "There aren't any that I know of."

But wait, you may say, what about arithmetical statements whose proof requires something like Koenig's lemma or Kruskal's tree theorem?  Don't these require a weak form of the axiom of choice?  The answer is that it depends on exactly how you state the result in question.  For example, if you state the graph minor theorem in the form, "given any infinite set of unlabeled graphs, there must exist two of them such that one is a minor of the other," then some amount of choice is needed to march through your infinite set of data, picking out vertices, subgraphs, etc. [EDIT: I made a mistake here. As Emil Jeřábek explains, the  graph minor theorem—or at least the most natural statement of it in the absence of AC—is provable in ZF.  But modulo this mistake, what I say below is still essentially correct.] However, if instead you write down a particular encoding by natural numbers of the minor relation on labeled finite graphs, and phrase the graph minor theorem as a statement about this particular partial order, then the statement becomes arithmetical and doesn't require AC in the proof.

Most people feel that the "combinatorial essence" of the graph minor theorem is already captured by the version that fixes a particular encoding, and that the need to invoke AC to label everything, in the event that you're presented with the general set-theoretic version of the problem, is sort of an irrelevant artifact of a decision to use set theory rather than arithmetic as one's logical foundation.  If you feel the same way, then the graph minor theorem doesn't require AC.  (See also this post by Ali Enayat to the Foundations of Mathematics mailing list, written in response to a similar question that I once had.)

The example of the chromatic number of the plane is similarly a matter of interpretation.  There are various questions you can ask that turn out to be equivalent if you assume AC, but which are distinct questions if you don't assume AC.  From a TCS point of view, the combinatorial heart of the question is the colorability of finite subgraphs of the plane, and the fact that you can then (if you want) use a compactness argument (this is where AC comes in) to conclude something about the chromatic number of the whole plane is amusing, but of somewhat tangential interest.  So I don't think this is a really good example.

I think ultimately you may have more luck asking whether there are any TCS questions that require large cardinal axioms for their resolution (rather than AC).  Work of Harvey Friedman has shown that certain finitary statements in graph theory can require large cardinal axioms (or at least the 1-consistency of such axioms).  Friedman's examples so far are slightly artificial, but I wouldn't be surprised to see similar examples cropping up "naturally" in TCS within our lifetimes.


machine learning for code and compiler optimization? I am looking into ML for generating more efficient code (i.e. compile time and run time heuristics). I have a phd (compilers, hpc), but very little ML experience.

I would appreciate any references to existing work.

More importantly, which Machine Learning techniques should i be exploring ?

each data sample is a code + test run + performance data
large number of data samples, with correct labeling
large number of parameters to modify
any sample can be rerun with any parameters (and get correct labeling)
large amount of cpu to run and re run samples

And also some of my very suspect assumptions...

much of the code is already locally-optimal (basic compiler optimization)
some of the parameters are "high level concepts" e.g. replace array with linked list. (so a small parameter change will have varied effects)
the desired improvement is bounded (a xK improvement is "good enough", K is well known)
the parameters are sparse i.e. mostly zero (i suspect that most code is basically good, and there are relatively few beneficial changes)

Any pointers to set me on my way would be appreciated

Genetic Programming (GP) has been used to modify source code for performance improvement.

e.g. Evolutionary Improvement of Programs

(This is close to my PhD topic, would be very interested to hear your approach)


Why don't we use larger classes to study determinism vs non-determinism? In a previous question about time hierarchy, I've learned that equalities between two classes can be propagated to more complex classes and inequalities can be propagated to less complex classes, with arguments using padding.

Therefore, a question comes to mind. Why do we study a question about different types of computation (or resources) in the smallest (closed) class possible?

Most researchers believe that $P \neq NP$. This distinction of classes wouldn't be between classes that use the same type of resource. Therefore, one might think of this inequality as a universal rule: Nondeterminism is a more powerful resource. Therefore, although an inequality, it could be propagated upwards via exploiting the different nature of the two resources.So, one could expect that $EXP \neq NEXP$ too. If one proved this relation or any other similar inequality, it would translate to $P \neq NP$.

My argument could maybe become clear in terms of physics. Newton would have a hard time understanding universal gravity by examining rocks (apples?) instead of celestial bodies. The larger object offers more details in its study, giving a more precise model of its behavior and allowing to ignore small-scale phenomena that might be irrelevant.

Of course, there is the risk that in larger objects there is a different behavior, in our case that the extra power of non-determinism wouldn't be enough in larger classes. What if after all, $P \neq NP$ is proven? Should we start working on $EXP \neq NEXP$ the next day?

Do you consider this approach problematic? Do you know of research that uses larger classes than polynomial to distinguish the two types of computation?

The issue may be a bit cleaner with $E=Dtime(2^{O(n)})$ and $NE=Ntime(2^{O(n)})$.
The easiest way to think about these classes is that they are the same as $P$ and $NP$ but restricted to unary languages. That is, all inputs are of the form $1^k$.

That is, the language $L$ is in $E$ if and only if the language $U_L = \{ 1^x : x\in L \}$ is in $P$ (identifying strings with numbers using binary representation), and similarly $NE$ is isomorphic to unary $NP$.

So, trying to separate $NE$ from $E$ is just like trying not just to separate $P$ from $NP$, but actually do it using a unary language. No reason it should make your life even conceptually easier.


Complexity of a subset sum variant Given integers $a_1, \ldots, a_n, b \in \mathbb{N}$. What is the complexity of the following problem
$$
\exists x_1, \ldots, x_n \in \mathbb{N} \text{ such that } a_1x_1 + \ldots a_nx_n = b?
$$
I can't find this subset-sum variant in the literature.

Here are some references, not a self-contained answer to the question.  For self-contained answers, see other people’s answers and comments.

Assuming that symbol ℕ in the question denotes the set of nonnegative integers, your problem is called the feasibility version of the change-making problem.  Chapter 5 of Martello and Toth [MT90] states that it is NP-complete, attributing the result to Lueker [Lue75].  I have not checked the report [Lue75].

Even if symbol ℕ in the question denotes the set of positive integers, the problem is still NP-complete because the nonnegative version can be easily reduced to the positive version.

References

[Lue75] G. S. Lueker.  Two NP-complete problems in nonnegative integer programming.  Report No. 178, Computer Science Laboratory, Princeton University, 1975.

[MT90] Silvano Martello and Paolo Toth.  Knapsack Problems: Algorithms and Computer Implementations, Wiley, 1990.  http://www.or.deis.unibo.it/knapsack.html


Confusion about a formal definition of PRAM consistency I am reading the paper "Consistency in Non-Transactional Distributed Storage Systems" by Paolo Viotti and Marko Vukolić. The authors provide a comprehensive survey of various consistency semantics based on the notions of history, abstract execution, and the $vis$ (visibility) and $ar$ (arbitration) relations, following Burckhardt (book).

I have some difficulty in understanding the definition of PRAM consistency (wiki). Informally, PRAM requires all processes see memory writes from one process in the order they were issued from the process. Writes from different processes may be seen in a different order on different processes.

In this paper (page 10), the authors define PRAM consistency by requiring the visibility relation ($vis$) to be a superset of session order ($so$; aka, program order). Formally,
$$\text{PRAM} \triangleq so \subseteq vis.$$

Consider the history below, where $w(x)0$ denotes a write of $0$ to $x$ and $r(x)0$ a read of $0$ from $x$.

This history does not satisfy PRAM consistency, because the only serial view of process $p_1$ is $w(x)0, w(x)1, r(x)1, r(x)0$ which is invalid.

However, according to the definition above, $r(x)1$ can be justified by the serial view of $w(x)1, r(x)1$, since the visibility set of $r(x)1$ is $vis^{-1}(r(x)1) = \{w(x)1\}$. Similarly, $r(x)0$ can be justified by the serial view of $r(x)1, w(x)0, r(x)0$, since the visible set of $r(x)0$ is $vis^{-1}(r(x)0) = \{w(x)0, r(x)1\}$.

To make $w(x)1$ visible to $r(x)0$, we require $(vis;so) \subseteq vis$. Therefore, in my opinion, PRAM should be defined as
$$\text{PRAM} \triangleq so \subseteq vis \land (vis;so) \subseteq vis.$$
(By the way, I think the predicate $RVal(\mathcal{F})$ is also needed.)

What is wrong with my arguments above?

When they define PRAM (page 11 of the arxiv preprint)
they actually state that vis is a partial order (in particular, transitive):

  We define PRAM consistency by requiring the visibility partial order to be a superset of session
  order:
  $$\text{PRAM} \triangleq so \subseteq vis.$$

Thus, the offending arrow in your diagram, from $w(x)0$ to $r(x)0$, is superfluous, as it is in the transitive closure of the other vis arrows.
So the $w(x)1$ write is already visible at the time when you would do $r(x)0$, so that read does not occur.


Complexity of advice language? Let $L$ be a language in P/poly.  There is then a deterministic polynomial-time Turing machine $M$ with polynomial-sized advice that decides $L$.  Consider the language $A(M)$ of all advice strings given to $M$ for instances in $L$.

  Is $A(M)$ in P/poly?

Edit 2: For $A(M)$ I am envisaging a specific, unique advice language; the existence of some advice language is guaranteed by the definition of $L$, so for $A(M)$ pick any such language, such as the lexicographically smallest.  Note that $A(M)$ is not necessarily decidable.

A handwaving (non-)argument for believing this goes something like this.  Every unary language is in P/poly, since a single bit of advice is enough to indicate whether the input is in the language or not.  In some sense advice languages are "sparsifications" of their associated languages; the advice language $A(M)$ contains a sparser representation of some of the information contained in language $L$, tweaked for the specific machine $M$.  (The advice language could be exponentially sparser, if every string is an instance of the problem, but for sparse languages the advice language may actually be polynomially denser.)  So it would seem to make sense that sparsifications of languages in P/poly could also be in this class.

Moreover, is there a general relationship between the complexity of $L$ and that of $A(M)$?

These seem like basic questions, so pointers to relevant literature would be appreciated if these are well-known.  A counterexample for the handwaving above would also be useful!

Edit: removed a sentence that wasn't even wrong, and based on the comments from Robin and Tsuyoshi, redefined the advice language to depend on $M$ only, as $M$ already depends on $L$.

Edit 3: I think Hrushikesh captured the essential problem here, so I am accepting the answer; Tsuyoshi also said essentially the same thing in a comment.  In short, $A(M)$ can be arbitrary.  Any language can be fed as advice to $M$ by waiting until the input instances of the decision problem are large enough for the next piece of advice to be within the polynomial bound.  This also means that I should really have asked the question in terms of a decision problem (where there are both YES and NO instances), not a language, to avoid the case where there are only finitely many YES instances.

Rigorous and probably more correct version at the bottom.

I don't think so. Consider the case where A(L,M) consists of advice strings of even length. To decide if x is in L, the machine M gets advice yz where y and z are strings of equal length. M discards z and decides membership of x in L only depending on y. Let y be of length n, and let z range over some arbitrary subset S of strings of length n.

In such a case, A(L,M) cannot be in P/Poly since given a string yz, the machine has to test membership of z in S. But since the advice is of length poly(n), the machine cannot work correctly for every S by counting argument.

Another more rigorous version:

Let L be the trivial language containing all strings. The machine M ignores its advice and accepts every input. The task is now to construct the set of advice strings A(M) which cannot be in P/Poly subject to the constraint that strings in L of length $n$ get advice of length $O(poly(n))$.

For every length $i$, let $S_i \subseteq {0,1}^i$. Let $S = \cup_i S_i$. Construct a mapping $f: S \rightarrow Z^+$ such that $|s| \leq f(s)$. The mapping just enumerates the strings in $S$ in non-decreasing order of length. The string $s$ serves as advice to M for strings of length $f(s)$.

By choosing $S_i$ to be of superpolynomial description size (can be done because of counting arguments), we get that $S$ (which is also $A(M)$) lies outside P/Poly.


Efficient concatenation of DFAs? There is theoretical evidence that the naive cartesian-product construction for the intersection of DFAs is "the best we can do". What about the concatenation of two DFAs? The trivial construction involves converting each DFA into an NFA, adding an epsilon-transition and determinizing the resulting NFA. Can we do better? Is there a known bound on the size of the minimal concatenation DFA (in terms of the sizes of the "prefix" and "suffix" DFAs)?

Yes - it is known that there exist DFA's of $m$ and $n$ states, respectively, such that the minimal DFA for the concatenation of the corresponding languages has $m*2^n - 2^{n-1}$ states, which matches the known upper bound.

This was first observed by Maslov in 1970, and rediscovered by Yu, Zhuang, and K. Salomaa in their paper, "The state complexities of some basic operations on regular languages", TCS 125 (1994), 315-328.


What is $DTIME(n^a)^{DTIME(n^b)}$? This might be embarrassing, but it turned out I don't know what is $DTIME(n^a)^{DTIME(n^b)}$. It is between $DTIME(n^{ab})$ and $DTIME(n^{a(b+1)})$ but where?

Update: There are three possible ways to define oracle machines.

1, They have an oracle tape, which they can read (see wikipedia).

2, They have an oracle tape, from which they can pose questions (see Arora-Barak book).

3, Same as two, but after each question the tape is erased (I could swear I heard this too).

I had 2 in mind, as the most common (?) definition.
In case of 3 it is easy to prove that the answer is $DTIME(n^{ab})$ (see Kristoffer's answer).
In case of 1, I am not even sure that the bounds I claim hold, but maybe it is not hard to prove, I have no clue about this version.

Update: I have realized that the number of tapes changes the power, so it is best to forget this question...

It seems your upper bound can be improved as follows: On input $x$ of length $n$, let $y_1,\dots,y_m$ be the oracle queries. Note that $|y_1|+\dots+|y_m| \leq c_1n^a$. The time to simulate the oracle machine to answer query $y_i$ is $c_2|y_i|^b$. Note now that $c_2(|y_1|^b+\dots+|y_m|^b) \leq c_2 (|y_1|+\dots+|y_m|)^b \leq c_2(c_1n^a)b = c_1c_2n^{ab}$. Thus the time to simulate the computation without the oracle is $c_1n^a + c_1c_2n^{ab} = O(n^{ab})$, which matches your lower bound.


Data-structure for functions of independent sets Suppose I have a graph $G$, with nodes $\{1,2,\ldots,n\}$, subsets of nodes $\{b_1,\ldots,b_k\}$ and functions $\{f_1,\ldots,f_k\}$ where $f_i$ maps independent subsets of $b_i$ to reals. The operation on $f$ is setting or getting all values in "canonical order", ie, $\langle f(\emptyset),f(\{1\}),f(\{2\}),f(\{3\}),f(\{1,2\}),\ldots \rangle$.

What is a way to do this more efficiently than with an array of size $2^{|b_i|}$ for $f_i$? This comes up when counting independent sets on graphs

I wanted to post a comment, but with no "karma" it seems impossible... What about using dictionaries (hashmap, depending on the language you use) to store the values of your $f_i$ ? This way you don't have to know beforehand the size of the memory you will need, and gettin a function's value is not too slow.


P vs. NP in a logic with a random oracle Choose a random oracle $f : \{0,1\}^\ast \to \{0,1\}$, and define the logic $ZFC^f$ by adding a fresh symbol $g$, an axiom that $g$ has the correct type, and one axiom $g(s) = f(s)$ for each $s \in \{0,1\}^\ast$.  This is a countably infinite set of axioms since $f$ is not a symbol in $ZFC^f$.

Within $ZFC^f$ we can define $g$-oracle Turing machines in the standard way, for example by using a second tape for the input to $g$ and letting the machine branch on the value of $g$ on the second tape.  We then have the complexity classes $P^g$, $NP^g$, etc.  Since $f$ was chosen at random in the metalogic, $P^g \ne NP^g$ is true with probability 1.

Question 1: Is $P^g = NP^g$ independent over $ZFC^f$?

The proof seems immediate: any finite proof in $ZFC^f$ can interrogate at most finitely many values of $g$.  However, I am not confident the definitions are sensible.

Question 2: Is there a good reference exploring this type of logic + random oracle construction?

Yes on Question 1 (assuming ZFC is consistent). You don't need $f$ to be random exactly, any $f$ will do. And for the proof you need to also use the fact that there is an oracle $h$ with NP$^h=$P$^h$.


Logical framework vs type theory What is the difference between logical framework and type theory? Both of them have types, terms, and are based on dependently typed lambda calculus.

We have Edinburg LF which is based on lambda-pi calculus, however, it seems to me that there's some subtle difference there.

Summary. A logical framework is a meta-language for the formalisation of deductive systems, where deductions become syntactic objects.

Of course what counts as a meta-language is quite vague, and it is helpful to understand the historical development of logical frameworks.
The first logical framework was de Bruijn's Automath (1), which is based on $\lambda$-calculus. Many of the ideas from the Automath language family have found their way into modern logical frameworks. Martin-Löf's work on constructive type-theories, also based on $\lambda$-calculi, has also been influential.

Edinburgh's LF (2) is a very influential logical framework.
Edinburgh LF is what you get when you enrich the simply typed $\lambda$-calculus with type-dependency. That's all. In order to make type-dependency precise, one needs to replace the function space operator $A \rightarrow B$ on types with type-abstraction, usually written $\Pi x^A. B$, and introduce the kind of types, as well as kind abstraction.
In terms of rules, the key is in the elimiation rule for $A \rightarrow B$, resp. $\Pi x^A. B$:

$$
\newcommand{\TYPES}[3]{#1 \vdash #2 : #3}
\newcommand{\SUBST}[2]{\{#1/#2\}}
\frac{
   \TYPES{\Gamma}{\color{red}{M}}{A \rightarrow B}
      \qquad
   \TYPES{\Gamma}{\color{red}{N}}{A}  }{
 \TYPES{\Gamma}{\color{red}{MN}}{B}   }
      \qquad
\frac{
   \TYPES{\Gamma}{{\color{red}M}}{\Pi x^A. B}
      \qquad
   \TYPES{\Gamma}{\color{red}{N}}{A}  }{
 \TYPES{\Gamma}{{\color{red}{MN}}}{B\SUBST{{\color{red}N}}{x}}   }
$$

On the left we have the rule for the simply typed $\lambda$-calculus, on the right the
rule that generalises the left with type dependency. We see that a value 'flows' into the
type in the conclusion on the right.

I think the interactive proof assistant Isabelle uses intuitionistic second order logic based on $\lambda$-calculus, without any numbers or recursive data types as logical framework. Various others have been proposed.

One advantage of using $\lambda$-calculi as logical framework  is that binding constructs like universal quantifiers can be implemented using the framework's $\lambda$-binder. Note that most logical frameworks are expressively weak: the frameworks  support object-level reasoning, but are insufficient to perform much meta-theoretic reasoning beyond the fact that a particular object-level statement is a theorem. In fact the metal-logic is usually so weak that even proving the deduction theorem for a Hilbert-style object logic is impossible. Of course nothing prevents you from using more powerful type-theories as a logical framework.

For these practical and historical reasons, most logical frameworks in use today are typed $\lambda$-calculi, i.e. type-theories. See (3, 4) for more in-depth discussions of logical frameworks.

N. de Bruijn: The Mathematical Language AUTOMATH, Its Usage, and Some of Its Extensions.
R. F. Harper, F. Honsell, G. Plotkin: A Framework for Defining Logics.
F. Pfenning: Logical frameworks.
F. Pfenning: Logical frameworks -- A Brief Introduction.


Translating pure literal elimination into rup I'm exploring building a CDCL SAT-solver with interesting reduction rules. I have two rules based on pure literal elimination, but if either of these rules generate a conflict, I don't know what to report for an RUP (reverse unit propagation) proof.
The first is pure-literal elimination over "base" clauses. That is, if a literal shows up with only one sign among the original clauses (but can still have the opposite sign in learnt clauses), then we set it.
The second is "would-be" pure-literal elimination binary clauses. If, among base (not learnt) clauses, literal A dominates literal B (but does not dominate -B) in the sense that every remaining unsatisfied rule containing B also contains A, then temporarily (while searching this branch) add the rule -A \/ -B since by setting A we would infer -B via pure literal elimination.
For both of these operations, it's easy to show that if a solution exists, then a solution still exists after applying the operation. But these rules can't be inferred via RUP and so it's unclear what to do in terms of providing a proof when they show up in a conflict.

Pure literal elimination over base clauses is effectively deleting those clauses from the formula, an action which cannot be encoded in a RUP proof since such proofs only encode clause additions.  But since an unsatisfiable formula will be unsatisfiable even without the clauses that contain pure literals you can treat the formula as if those clauses were not present.  Any RUP proof of the unsatisfiability of the formula with those clauses missing will also be a RUP proof of the unsatisfiability of the original formula.
As for the second example, you can't validly add $(\lnot A \lor \lnot B)$ to the proof because that clause isn't an actual requirement to satisfy the formula.  $A$ dominating $B$ after a partial assignment doesn't indicate that $\lnot B$ is mandatory, rather it means that asserting $B$ isn't helpful.  In fact, it might be a bad thing to do if $\lnot B$ is needed to satisfy some clauses later.  If you assert $\lnot B$ to satisfy all clauses containing $\lnot B$ you can be confident that $B$ will never appear in a downstream conflict clause and thus will never be part of a RUP clause generated by this partial assignment.  So asserting $\lnot B$ can't hurt but you can't be sure that it is necessary.  RUP proof clauses state only what is necessary.


What is the best lower bound for the fault-tolerance threshold in quantum computing? It is well established that there exists a noise threshold for quantum computation, such that below this threshold, the computation can be encoded in such a way that it yields the correct result with bounded probability (with at most polynomial computational overhead). This threshold depends on the encoding used and the exact nature of the noise, and it is the case that results from simulation often give thresholds much higher than what can be proved for adversarial noise models.

  So my question is simply what is the highest lower bound that has been
  proved for independent stochastic noise?

The noise model I am referring to is the one dealt with in quant-ph/0504218, where Aliferis, Gottesman and Preskill prove a lower bound $2.73 \times 10^{-5}$. Note, however, I do not care which type of encoding is used, and it need not be restricted to the code considered in that paper. The highest I'm aware of is $1.94 \times 10^{-4}$ due to Aliferis and Cross (quant-ph/0610063). Has this value been improved upon since then?

The highest threshold lower bound for for independent stochastic noise of which I am aware is $1.04 \times 10^{-3}$ by Aliferis, Gottesman and Preskill (quant-ph/0703264).  They analyze Knill's teleportation-based scheme with postselection.

If you are willing to consider independent depolarizing noise, then I know of two slightly higher lower bounds: $1.25\times 10^{-3}$ by Aliferis and Preskill (arXiv:0809.5063) and $1.32 \times 10^{-3}$ by myself and Ben Reichardt (arXiv:1106.2190).


weights in low density codes Generally, low density parity codes are decoded using sum product decoder (also known as decoding under belief propagation). Such codes are usually decoded nicely if there are no short length cycles in tanner graph, in particular length 4 cycles are to be avoided. Naturally, this puts some bound on column weight in such a parity matrix. What is the general column weight $t$ that is allowed (in terms of code dimensions $k,n$) so that there are no 4-cycles?

To state it formally

given n and k what is maximum value of $t$ for which tanner graph (bipartite t regular) has no 4 cycle?

Your question is somewhat ill-posed: given $n$ and $k$, it is easy to construct a Tanner graph with a 4-cycle and column weight at most 2.

Instead, you can ask the question of what is the maximum column weight of a Tanner graph, given that is has no 4-cycle. Assuming uniform column weights, then the maximum column weight is $O(\sqrt{k})$. This is known as the Kővári–Sós–Turán theorem (see e.g. here), which states that the number of edges in an $(n,k)$-bipartite graph without 4-cycle is at most
$$
(n-1)\sqrt{k} + k.
$$
If the Tanner graph has uniform column weights $d$, then it has $nd$ edges, which gives the bound on $d$.

This is tight up to constants for the case where $k = n$ (see e.g. here).


Is there a Time Hierarchy theorem for PH? Is it true that there are problems in the polynomial hierarchy solvable in time $O(n^k)$ (by an alternating Turing machine in some level of the polynomial hierarchy) that are not solvable in $O(n^{k-1})$ in any level of the polynomial hierarchy?
In other words - does there exist a time hierarchy theorem for the polynomial hierarchy like there does for P and NP?
If there does - a reference would be great.

The difficulty I ran into is that the simulating machine, when simulating machines from all levels of the hierarchy, is not in any distinct level of the hierarchy. Which leads to a related question - what is the smallest class such a simulating machine belongs to? Is there any sense in defining a class with $O(n)$ alternations (or $O(\log n)$ / $O(\log \log n)$)?

Yes. For example, the usual proofs of the time hierarchy theorem (by directly simulating arbitrary machines) can be used to show that for every $c \geq 1$, $\Sigma_c TIME[n^k]$ is not a subset of $\Pi_c TIME[n^{k-1}]$. The reason for switching from $\Sigma$ to $\Pi$ is that, in this diagonalization argument, we have to do the "opposite" of the machine we're simulating, so we have to run in universal mode when the simulating machine is in existential mode, and vice-versa.

You can also get a result like this without switching from $\Sigma$ to $\Pi$: for every $c \geq 1$, $\Sigma_c TIME[n^k]$ is not a subset of $\Sigma_c TIME[n^{k-1}]$. This can be done using the proof of the time hierarchy due to Zak (reference: "A Turing machine time hierarchy", Theoretical Computer Science 26(3):327--333, 1983). For an explicit reference to this version of the time hierarchy theorem, see Dieter van Melkebeek's "A Survey of Lower Bounds for Satisfiability and Related Problems" (available on his home page).


Problems with big open complexity gaps This question is about problems for which there is a big open complexity gap between known lower bound and upper bound, but not because of open problems on complexity classes themselves.

To be more precise, let's say a problem has gap classes $A,B$ (with $A\subseteq B$, not uniquely defined) if $A$ is a maximal class for which we can prove it is $A$-hard, and $B$ is a minimal known upper bound, i.e. we have an algorithm in $B$ solving the problem. This means if we end up finding out that the problem is $C$-complete with $A\subseteq C\subseteq B$, it will not impact complexity theory in general, as opposed to finding a $P$ algorithm for a $NP$-complete problem.

I am not interested in problems with $A\subseteq P$ and $B=NP$, because it is already the object of this question.

I am looking for examples of problems with gap classes that are as far as possible. To limit the scope and precise the question, I am especially interested in problems with $A\subseteq P$ and $B\supseteq EXPTIME$, meaning both membership in $P$ and $EXPTIME$-completeness are coherent with current knowledge, without making known classes collapse (say classes from this list).

The Knot Equivalence Problem.

Given two knots drawn in the plane, are they topologically the same? This problem is known to be decidable, and there do not seem to be any computational complexity obstructions to its being in P. The best upper bound currently known on its time complexity seems to be a tower of $2$s of height $c^n$, where $c = 10^{10^{6}}$, and $n$ is the number of crossings in the knot diagrams. This comes from a bound by Coward and Lackenby on the number of Reidemeister moves needed to take one knot to an equivalent one. See Lackenby's more recent paper for some more recent related results and for
the explicit form of the bound I give above (page 16).


Favorable graph decomposition for dense graphs to solve independent set problem I have to solve an independent set problem (ISP) on dense graphs with many cliques. To tackle the problem, I'm considering to use graph decompositions such as tree-, modular decomposition or clique-width k-expression trees.

Are there some decompositions (or other techniques) favorable for my type of graphs?

From what I understand, considering e.g. the tree-decomposition, the ISP can be solved in $\mathcal{O}(n2^k)$ where $n$ is number of vertices of the tree and $k$ the tree-width. Moreover, the tree-width is a measure of how similar a graph is to a tree. From this, I concluded that a graph which is not very similar to tree (maybe just like mine) has a large tree-width and, hence, the tree-decomposition is maybe not a favorable decomposition to solve the ISP.

Is e.g. the clique-width k-expression tree more suitable for my case?

The problem is that most decompositions (I know of) are themselves much harder to compute/approximate than INDEPENDENT SET.

However, if your graphs are really very dense, their complements might be sparse. Thus, it might be worth considering solving CLIQUE in the complement of the input graph. This can be done in $O(nd\cdot 1.45^d)$ time (Eppstein, Löffler, Strash), where $d$ is the degeneracy of the input graph (which is even smaller than the treewidth).