Constraint satisfaction problem (CSP) vs. satisfiability modulo theory (SMT); with a coda on constraint programming

SAT, CP, SMT, (much of) ASP all deal with the same set of combinatorial optimisation problems.
However, they come at these problems from different angles and with different toolboxes.
These differences are largely in how each approach structures information about the exploration of the search space.
My working analogy is that SAT is machine code, while the others are higher level languages.

Based on my thesis work on the structural theory of CSPs, I have come to believe that the notion of "clause structure" is essential in unifying all these paradigms and in understanding how they differ.
Each clause of a SAT instance represents a forbidden partial assignment; a clause like $x_1 \lor \overline{x_2} \lor x_3$ forbids the partial assignment $\{(x_1,0),(x_2,1),(x_3,0)\}$ that simultaneously sets $x_1$ and $x_3$ to false and $x_2$ to true.
The clause structure of a combinatorial optimisation problem is its representation as a SAT instance, using some suitable encoding.
However, the clause structure includes all the forbidden partial assignments, not just the ones given at the start.
The clause structure is therefore usually too large to manipulate directly: typically it has at least exponential size in the number of variables, and may be infinite.
Hence, the clause structure has to be approximated with a limited amount of space.
SAT/CP/SMT/ASP maintain and update a more-or-less implicit representation of an underlying clause structure.
This is possible because if one partial assignment is known to be in the clause structure, then this implies that many other clauses are also present.
For instance, the SAT clause above also forbids any partial assignment that contains it as a subset, so clauses like $x_1 \lor \overline{x_2} \lor x_3 \lor x_4$ and $x_1 \lor \overline{x_2} \lor x_3 \lor \overline{x_4} \lor x_5$ are all in the clause structure of that instance.

An approximation of the clause structure is kept to narrow down the set of solutions, and to help determine whether this set is empty.
During search some partial assignments may turn out not to be contained in any solution (even if they individually satisfy each of the constraints in the instance).
These are known as nogoods, a term introduced by  ("Mr GNU") Stallman and Sussman.
A nogood clause is therefore in the clause structure and can be included in an approximation of the clause structure, as a compact representation of many clauses that can be pruned from the search for solutions.
Adding nogoods to the approximate clause structure retains all the solutions, but better approximates those solutions.
So the approximate clause structure usually changes as search progresses.
Further, the way the problem is modelled in one of the combinatorial optimisation approaches affects the clause structure, often quite significantly.
For instance, propositional variables can represent intervals such as $x \le 5$ or points such as $x = 5$.
Hence there isn't a single general clause structure but one associated with each choice of representation, depending on what the singletons (literals) of the clause structure represent.

Constraint programming (CP) was traditionally an AI discipline, with a focus on scheduling, timetabling, and combinatorial problems, and therefore has a central role for variables that can take more than just two values (but usually only finitely many).
CP has emphasised efficient search and, motivated by the traditional applications, has given a central role to the all-different (injectivity) constraint, but has also developed efficient propagators for many other kinds of constraints.
The formal definitions of CP have been around since at least Montanari's 1974 paper Networks of constraints, with precursors going back even earlier.
This weight of history may have contributed to CP lagging behind other approaches in raw performance over the last decade.
CP classically maintains an approximation of the complement of the clause structure, via a set of active domains for the variables.
The aim is to eliminate values from the active domains, exploring the clause structure by trying to assign candidate values to variables and backtracking when necessary.

Satisfiability modulo theories (SMT) came out of the verification community.
Each theory in an SMT solver forms an implicit representation of potentially infinitely many SAT clauses.
The theories used with SMT and the constraints used in CP reflect their different historical applications.
Most of the theories SMT considers have to do with integer-indexed arrays, real closed fields, linear orders, and suchlike; these arise from static analysis of programs (in computer aided verification) or when formalising mathematical proofs (in automated reasoning).
In contrast, in timetabling and scheduling the injectivity constraint is central, and although the standard SMTLIB language has had an injectivity constraint since its inception in 2003 (via the distinct symbol), until 2010 SMT solvers only implemented distinct via a naive algorithm.
At that stage the matching technique from the standard CP propagator for all-different was ported across, to great effect when applied to large lists of variables; see An Alldifferent constraint solver in SMT by Banković and Marić, SMT 2010.
Moreover, most CP propagators are designed for problems with finite domains, whereas standard SMT theories deal with infinite domains (integers, and more recently reals) out of the box.
SMT uses a SAT instance as the approximation of the clause structure, extracting nogood clauses from the theories as appropriate.
A nice overview is Satisfiability Modulo Theories: Introduction and Applications
by De Moura and Bjørner,
doi:10.1145/1995376.1995394.

Answer set programming (ASP) came out of logic programming.
Due to its focus on solving the more general problem of finding a stable model, and also because it allows universal as well as existential quantification, ASP was for many years not competitive with CP or SMT.

Formally, SAT is CSP on Boolean domains, but the focus in SAT on clause learning, good heuristics for conflict detection, and fast ways to backtrack are quite different to the traditional CSP focus on propagators, establishing consistency, and heuristics for variable ordering.
SAT is usually extremely efficient, but for many problems huge effort is required to first express the problem as a SAT instance.
Using a higher level paradigm like CP can allow a more natural expression of the problem, and then either the CP instance can be translated into SAT by hand, or a tool can take care of the translation.
A nice overview of the nuts and bolts of SAT is On Modern Clause-Learning Satisfiability Solvers by Pipatsrisawat and Darwiche, doi:10.1007/s10817-009-9156-3.

Now let's move on from generalities to present day specifics.

Over the last decade some people in CP have started to focus on lazy clause generation (LCG).
This is essentially a way to bolt CP propagators together using more flexible SMT-like techniques rather than the rather rigid active domains abstraction.
This is useful because there is a long history of published CP propagators to efficiently represent and solve many kinds of problems.
(Of course, a similar effect would be achieved by concerted effort to implement new theories for SMT solvers.)
LCG has performance that is often competitive with SMT, and for some problems it may be superior.
A quick overview is Stuckey's CPAIOR 2010 paper Lazy Clause Generation: Combining the power of SAT and CP (and MIP?) solving, doi:10.1007/978-3-642-13520-0_3.
It is also worth reading the position paper of Garcia de la Banda, Stuckey, Van Hentenryck and Wallace, which paints a CP-centric vision of The Future of Optimization Technology, doi:10.1007/s10601-013-9149-z.

As far as I can tell, much of the focus of recent SMT research seems to have shifted to applications in formal methods and formalised mathematics.  An example is reconstructing proofs found by SMT solvers inside proof systems such as Isabelle/HOL, by building Isabelle/HOL tactics to reflect inference rules in SMT proof traces; see Fast LCF-Style Proof Reconstruction for Z3 by Böhmer and Weber at ITP 2010.

The top ASP solvers have over the last few years been developed to become competitive with CP, SMT and SAT-only solvers.
I'm only vaguely familiar with the implementation details that have allowed solvers such as clasp to be competitive so cannot really compare these with SMT and CP, but clasp explicitly advertises its focus on learning nogoods.

Cutting across the traditional boundaries between these formalisms is translation from more abstract problem representations into lower level efficiently implementable formalisms.
Several of the top ASP and CP solvers now explicitly translate their input into a SAT instance, which is then solved using an off-the-shelf SAT solver.
In CP, the Savile Row constraint modelling assistant uses compiler design techniques to translate problems expressed in the medium level language Essence' into a lower level formalism, suitable for input to CP solvers such as Minion or MiniZinc.
Savile Row originally worked with a CP representation as the low-level formalism but introduced SAT as a target in version 1.6.2.
Moreover, the even higher-level language Essence can now be automatically translated into Essence' by the Conjure tool.
At the same time, low level SAT-only solvers like Lingeling continue to be refined each year, most recently by alternating clause learning and in-processing phases; see the brief overview What's Hot in the SAT and ASP Competitions by Heule and Schaub in AAAI 2015.

The analogy with the history of programming languages therefore seems appropriate.
SAT is becoming a kind of "machine code", targeting a low-level model of exploration of the clauses in the clause structure.
The abstract paradigms are becoming more like higher level computer languages, with their own distinct methodologies and applications they are good at addressing.
Finally, the increasingly dense collection of links between these different layers is starting to resemble the compiler optimisation ecosystem.


Any references for techniques in FPT reductions?

Both the original parametrized complexity book by Downey and Fellows, and the newer book by Flum and Grohe, are good references for reduction techniques.


A 3-CNF formula that requires resolution width $5$

The following example comes from the paper which gives a combinatorial characterization of resolution width by Atserias and Dalmau (Journal, ECCC, author's copy).

Theorem 2 of the paper states that, given a CNF formula $F$, resolution refutations of width at most $k$ for $F$ are equivalent to winning strategies for Spoiler in the existential $(k+1)$-pebble game.
Recall that the existential pebble game is played between two competing players, called Spoiler and Duplicator, and the positions of the game are partial assignments of domain size at most $k+1$ to variables of $F$.
In the $(k+1)$-pebble game, starting from the empty assignment, Spoiler wants to falsify a clause from $F$ while remembering at most $k+1$ boolean values at a time, and Duplicator wants to prevent Spoiler from doing so.

The example is based on (the negation of) the pigeonhole principle.

  For every $i \in \{1, \dotsc, n+1 \}$ and $j \in \{1, \dotsc, n \}$, let $p_{i,j}$ be a propositional variable meaning that pigeon $i$ sits in hole $j$.
  For every $i \in \{1, \dotsc, n+1 \}$ and $j \in \{0, \dotsc, n \}$, let $y_{i,j}$ be a new propositional variable.
  The following $3$-CNF formula ${EP}_i$ expresses that pigeon $i$ sits in some hole:
  $$ {EP}_i \equiv \neg y_{i,0} \wedge \bigwedge_{j=1}^n (y_{i,j-1} \vee p_{i,j} \vee \neg y_{i,j} ) \wedge y_{i,n}. $$
  Finally, the $3$-CNF formula ${EPHP}_n^{n+1}$ expressing the negation of the pigeonhole principle is the conjunction of all ${EP}_i$ and all clauses $H_k^{i,j} \equiv \neg p_{i,k} \vee \neg p_{j,k}$ for $i,j \in \{1, \dotsc, n+1 \}, i \ne j$ and $k \in \{1, \dotsc, n \}$.

Lemma 6 of the paper gives a fairly short and intuitive proof that Spoiler cannot win the $n$-pebble game on ${EPHP}_n^{n+1}$, hence ${EPHP}_n^{n+1}$ has no resolution refutation of width at most $n-1$.

The paper has another example in Lemma 9, based on the dense linear order principle.

Given that computing the minimum width for resolution refutations is EXPTIME-complete, and moreover it takes $\Omega(n^{(k-3)/12})$ time to certify that the minimum width is at least $k+1$ (see Berkholz's paper in FOCS or arXiv), perhaps it is hard to come up with examples which provably need wide resolution refutations?


What is the best approximation and exact algorithm for vertex cover on cubic graphs?

The best-known algorithm for vertex cover in (general) graphs runs in time $O(1.2114^n)$ by Bourgeois, Escoffier, Paschos and van Rooij. You may read their paper and see whether their algorithm can be improved for cubic graphs.

Bourgeois, N., Escoffier, B., Paschos, V. T., & van Rooij, J. M. (2012). Fast algorithms for max independent set. Algorithmica, 62(1-2), 382-415.

Moreover, the following paper proves a hardness result for an ($1+\epsilon$) approximation algorithm for vertex cover in cubic graphs.

Alimonti, P., & Kann, V. (1997, March). Hardness of approximating problems on cubic graphs. In Italian Conference on Algorithms and Complexity (pp. 288-298). Springer, Berlin, Heidelberg.

However, a greedy 2-approximation algorithm for vertex cover in general graphs is easy. Just pick an uncovered edge each time and choose both of its ends.


Does every regular language contains a strictly locally testable language?

The answer is no. The argument was suggested by phs, but you have to start with a different language. Take $L = (aa)^*$. Then any regular language $K$ contained in $L$ is of the form
$$
 K = \{(aa)^n \mid n \in U \}
$$
 for some ultimately periodic subset $U$ of $\mathbb{N}$. If $K$ is infinite, then the period $p$ of $U$ is not $0$ and thus $K$ is not star-free (hence not locally testable and not strictly locally testable).


Problems in $\text{PSPACE} \cap \text{Co-NP-Hard}$

Formula Isomorphism is in $\mathsf{\Sigma_2 P} \subseteq \mathsf{PSPACE}$, is easily seen to be $\mathsf{coNP}$-hard, but is not known to be $\mathsf{NP}$-hard. Note that FI is not $\mathsf{\Sigma_2 P}$-complete unless $\mathsf{PH}$ collapses to the third level. All of this can be found in Agrawal & Theirauf.


I believe Artem Kaznatcheev's answer is correct, but it does not give polynomial space. So here's a different approach that should work a little better in that respect.

Using max flow it is possible to solve a slightly more general problem: find a pair of edge disjoint paths from some two vertices {s1,s2} to some other pair of vertices {t1,t2}, but without controlling which source vertex is connected to which destination vertex.

Suppose we have a graph G and vertices s1,s2,t1,t2 for which we want to list all pairs of paths. Find a single pair of paths P1,P2, and let e = (s1,v) be the first edge on one of those paths. Then we can split the problem space into two subproblems: the pairs of paths that use e are the same as the paths from {v,s2} to {t1,t2} in G-s1, and the pairs of paths that do not use e are the same as the paths from {s1,s2} to {t1,t2} in G-e. Recurse in both of these two subproblems, and (to avoid duplication) only report a path when you're at the bottom of the recursion.


We can reduce it to the following problem:

  Given a directed graph on vertex set $\{1,2,\dots,n\}$, we want to know if there exists a permutation $T$ such that for each edge $(i,j)$ in the graph, $T[i]<T[j]$.

The reduction: add an edge to the graph for each pair $i,j$ where both $P_b[i]$ and $P_b[j]$ exist for some $b \in \{0,1\}$; the orientation of the edge is determined by whether $P_b[i]<P_b[j]$ or not.  This yields a directed graph that contains the union of edges from $P_0$ plus edges from $P_1$.

Conveniently, the new problem is easy.  Of course, if there are any cycles in the graph, then there is no such permutation $T$ (i.e., the two permutations $P_0,P_1$ are not compatible).  Conversely, if there are no cycles in the graph, then there is such a permutation $T$ (i.e., the permutations $P_0,P_1$ are compatible).  Do you see why?  We can simply apply a topological sort to the graph and use it to construct an example of such a permutation $T$, where we assign $T[i]=j$ if vertex $i$ is the $j$th vertex to be visited in the topologically sorted order.

I'm not sure what BDDs have to do with it.  This does not seem like a research-level question.


Classes of graphs with easy Hamiltonian cycle but NP-hard TSP

Cographs are not always Hamiltonian, have polynomial time tests for Hamiltonicity, and are NP-hard to solve the traveling salesman problem for.

More generally the Hamiltonian cycle problem can be solved in polynomial time (but is not fixed-parameter tractible) on graphs of bounded clique-width; see, e.g., Fomin et al., "Clique-width: on the price of generality", SODA'09. But again because these graph families include the complete graphs, the TSP is hard on these graphs.


Completeness of the extension of first order logic with least fixed point order operator

FO-LFP is neither complete (its valid sentences cannot be described by a recursively presented proof system) nor compact (there is an unsatisfiable set of sentences all of whose finite subsets are satisfiable). The basic argument is given in Denis’s answer so I won’t repeat it here, but let me instead point out that as a general principle due to Per Lindström, when extending first-order logic, some important property has to give way.

The setup is that we consider logics given by a satisfaction predicate $M\models\phi$ between ordinary first-order models, and an abstract set of sentences, that satisfy a handful of natural technical conditions.

The first Lindström’s theorem states that no proper extension of FO can simultaneously satisfy

(Löwenheim–Skolem) If a sentence has a model, it has an at most countable model.
(Compacteness) If $T$ is a set of sentences such that every finite subset of $T$ has a model, then $T$ has a model.

The second Lindström’s theorem states that no proper extension of FO with effectively presented syntax can satisfy

The Löwenheim–Skolem property as above.
(Completeness) The set of valid sentences can be described by an effectively axiomatized proof system (i.e., it is recursively enumerable).

For example, FO+TC has the Löwenheim–Skolem property (as it is a fragment of $L_{\omega_1,\omega}$), hence it can be neither complete nor compact, and a fortiori the same applies to all extensions of FO+TC such as fixed-point logics. (This is of course easy to show directly.)


I don't know any reference, so just an extended comment:

If you allow a succinct representation for the input integers, i.e. you can represent the input integers as factors, then the "multiplicative" versions of Knapsack are NP-complete; indeed:

$\sum_{i=1}^n w_i x_i \leq W$ can be reduced to the equivalent $\prod_{i=1}^n 2^{w_i} x_i \leq 2^W$;

and $\sum_{i=1}^n v_i x_i$ maximization can be reduced to  $\prod_{i=1}^n 2^{v_i} x_i$ maximization.

I didn't think about it too much but the above reduction should work even if we require that in a mixed instance ( maximize sum of values under multiplicative weight constraint OR maximize product of values under addictive weight constraint ) all input values must be given with their prime factorization (building a direct reduction from exact cover).

Without a succinct representation the above reduction doesn't work because Knapsack is not strongly NPC.


What is the worst case of the randomized incremental delaunay triangulation algorithm?

The first approach can be formalized as follows.

Let $P$ be an arbitrary set of $n$ points on the positive branch of the parabola $y=x^2$; that is,
$$
P = \{ (t_1, t_1^2), (t_2, t_2^2), \dots, (t_n, t_n^2) \}
$$
for some positive real numbers $t_1, t_2, \dots, t_n$.  Without loss of generality, assume these points are indexed in increasing order: $0 < t_1 < t_2 < \cdots < t_n$.

Claim: In the Delaunay triangulation of $P$, the leftmost point $(t_1, t_1^2)$ is a neighbor of every other point in $P$.

This claim implies that adding a new point $(t_0, t_0^2)$ to $P$ with $0 < t_0 < t_1$ adds $n$ new edges to the Delaunay triangulation.  Thus, inductively, if we incrementally contract the Delaunay triangulation of $P$ by inserting the points in right-to-left order, the total number of Delaunay edges created is $\Omega(n^2)$.

We can prove the claim as follows.  For any real values $0<a<b<c$, let $C(a,b,c)$ denote the unique circle through the points $(a,a^2), (b,b^2), (c,c^2)$.

Lemma: $C(a,b,c)$ does not contain any point $(t,t^2)$ where $a<t<b$ or $c<t$.

Proof: Recall that four points $(a,b), (c,d), (e,f), (g,h)$ are cocircular if and only if
$$
\begin{vmatrix}
1 & a & b & a^2 + b^2 \\
1 & c & d & c^2 + d^2 \\
1 & e & f & e^2 + f^2 \\
1 & g & h & g^2 + h^2 \\
\end{vmatrix}
=
0
$$
Thus, a point $(t,t^2)$ lies on the circle $C(a,b,c)$ if and only if
$$
\begin{vmatrix}
1 & a & a^2 & a^2 + a^4 \\
1 & b & b^2 & b^2 + b^4 \\
1 & c & c^2 & c^2 + c^4 \\
1 & t & t^2 & t^2 + t^4 \\
\end{vmatrix}
=
0
$$
It's not hard (for example, ask Wolfram Alpha) to expand and factor the $4\times4$ determinant into the following form:
$$
(a-b)(a-c)(b-c)(a-t)(b-t)(c-t)(a+b+c+t) = 0
\tag{$*$}
$$
Thus, $(t,t^2)$ lies on $C(a,b,c)$ if and only if $t=a$, $t=b$, $t=c$, or $t=-a-b-c < 0$.  Moreover, because $0<a<b<c$, these four roots are distinct, which implies that the parabola actually crosses $C(a,b,c)$ at those four points.  It follows that $(t,t^2)$ lies inside $C(a,b,c)$ if and only if $-a-b-c<t<a$ or $b<t<c$.$\qquad\Box$


Appilicability of Theoritical Computer Science in Malware research

Fred Cohen is an authority & early researcher on the theory of computer viruses.  see that wikipedia page for references. his 1987 paper is given credit as maybe the 1st analogy of the virus checking problem to the halting problem.

the basic idea is to create a program X that calls a virus checking subroutine with a program code as parameter. then, if the subroutine returns "is a virus", exit. if it returns "is not a virus", infect the system. such a program cannot exist by diagonalization/contradiction, passing its own code as the parameter. therefore there is no perfect virus checker.

but it would seem an easy counterargument to this statement could be, program X contains a harmful section of code, and that its irrelevant whether it is called or not-- the program is potentially harmful if it contains any "harmful section of code".

as I recall this result was published separately in a mathematical journal but cant find the reference right now.

a more recent/advanced topic is detecting polymorphic viruses that change their code in equivalent but random ways.

another promising approach that seems to avoid the halting problem issue (in a way that demonstrates abstract theoretical "no-go theorems" can be misleading or even inapplicable in practice) is to create a secure "sandbox" in which a program can run but cannot do anything harmful.

the modern web browser can be seen as an attempt to build such a system. the complexity of securing it arises mainly with Javascript.

Google is building the NaCL[3] framework that partly originated in academia and is the current leading contender for a high functional sandbox system integrated into the modern browser that still allows machine code. a provably secure software checker validates candidate programs. there are recent dramatic improvements announced[4].

a novel recent idea is to use graph based analysis of execution traces[5].

a more recent topic of virtualization has various security implications/applications as you note eg virus vendors building virtualization systems to find/detect viruses etc.[6]

the sophistication of the recent stuxnet virus, apparently the worlds 1st state/govt-sponsored, military-agency-developed virus for cyber/espionage/sabotage purposes, has led to serious/heavy academic study, see the extensive references on wikipedia. there is a recent/new variant discovered targeting the financial industry called flame.

[1] An Undetectable Computer Virus David M. Chess and Steve R. White

[2] Trends in computer virus research Cohen, 1991

[3] Native Client: A Sandbox for Portable, Untrusted x86 Native Code by Yee et al 2009

[4] NaCl to give way to RockSalt: Computer scientists develop a tool to improve software fault isolation 2012

[5] Graph-based malware detection using dynamic analysis by Anderson et al

[6] Detection of Metamorphic and Virtualization-based
Malware using Algebraic Specification by Webster, Malcolm


Good seating arrangements for sequence of meals and tables of size k for a group of people

Here's a variant of the original answer (below) that gives the desired setting: tables of size 5, 45 people, and 10 meals, except that one meal has a few tables of size 4.

Let $F$ be the field of size 9.  Pick 4 vertical, degenerate lines  $\{(b,x) | x \in F\}$ for every $b = 0,1,2,3$ and declare their people "empty."  We are left with 81 - 9x4 = 45 people.

9 meals are given by slopes $a = 0,1,\ldots,8$.  The intersections with the 4 empty degenerate lines reduce the table size to 9-4=5.

An additional meal is given by the remaining degenerate lines $\{(b,x) | x \in F\}$ for every $b = 4,5,6,7,8$.  Here the table size is 9.  However (in any solution) we can break a table of size 9 into a table of size 5 and one of size 4.

If there are a few more people one can use the field of size 11.

First let us handle $k^2$ people and $k$ meals.

Pick a finite field $F$ of size $k$ and identify people with $F \times F$.  To each meal there corresponds a slope, to a table a line parallel to that slope.

Specifically, meal $a$ has $k$ tables $\{(x,ax+b) | x \in F\}$ for every $b \in F$.

The intersection property you want is the fact that lines with distinct slopes intersect in exactly one point.

To handle $2k^2$ people, divide them up in two groups of $k^2$ each, and apply the construction above to each group.  To handle $2k^2 - k = 45$, label (in the first group) a fixed line such as $\{(x,x)|x\in F\}$ as "empty."  You may have a few tables with $k-1$ people.

For more meals one could e.g. pick a different partition in two groups at the beginning of the 6th meal. (Say you interleave the original partition, to ensure that the two groups "mix.") Though of course this may result in some intersections.


Is predicting (in the limit) computable sequences as hard as a dominating function?

The uniform version is theorem 7 of the paper "Inductive inference and unsolvability" by Adleman and M. Blum. The result is for Gold's model of learnability in the limit (the oracle, instead of predicting the next bit, gives you an index of a program that computes the sequence you are trying to discover). Both models are equivalent.

The idea behind the proof is that, for every total computable function $h$ there is a total computable function $g$ whose running time dominates $h$. So, you use the oracle to, on input x, find the greatest of the running time of all functions inferable from a prefix of length $x$. In order not to run forever, you stop counting the steps of the function predicted by the oracle if you find that it will change its prediction when a finite number of 0s are appended to the prefix (this eventually happens because the oracle has to predict every finite variation of the constantly 0 function). The trick is that for every $h$ and every sufficiently large $z$, the output is at least as big as the number of steps to compute $g(z)$, for the respective $g$.


You are incorrect about the definition of large elimination: it refers to the ability to build values of type $\mathrm{Type}$ by eliminating an inductive value. The canonical example:

bool_to_type : bool -> Type := fun b =>
     match b with
         | true => Unit
         | false => Empty

Where Unit and Empty are inductive types with 1 and 0 constructors, respectively. Notably, this allows you to prove the proposition $0 \not= 1$, which cannot be proven without this ability.

As noted in another answer (https://cstheory.stackexchange.com/a/21878/3984) a good resource that explains this is the following github repo: https://github.com/FStarLang/FStar/issues/360


NP-hardness of a Set Cover specialization

Overview

This problem is NP-hard; more precisely, the associated decision problem (in which we ask whether a target number of tridents $k$ can cover all of the given $x_i$s) is NP-hard. We will refer to this decision problem as the Numerical Trident Cover Problem.

To prove that the Numerical Trident Cover Problem is NP-hard, we introduce the following intermediate problem, which we will call the Grid Triangle Cover Problem:

Input: A finite set $S \subset \mathbb{Z}^+ \times \mathbb{Z}^+$ of integer coordinate pairs and an integer value $k$.

Output: Yes or no, with an output of yes if and only if there exists a set $T \subset \mathbb{Z} \times \mathbb{Z}$ with $|T| \le k$ such that $S \subseteq \bigcup_{(x,y) \in T} \{(x, y), (x, y+1), (x+1, y)\}$

Thinking about this problem graphically, we are given a subset of the integer lattice and asked to cover every point in this subset with $k$ side-length-$(1, 1, \sqrt{2})$ right triangles in a particular orientation (in particular these triangles must have vertices of the form $(x, y)$, $(x, y+1)$, and $(x+1, y)$). We are asked to say yes if and only if this is possible.

To show that Numerical Trident Cover is NP-hard, we provide two reductions: a reduction from Planar 3SAT to Grid Triangle Cover and a reduction from Grid Triangle Cover to Numerical Trident Cover. Together, these compose into a reduction from the NP-hard problem Planar 3SAT to the Numerical Trident Cover problem, implying that Numerical Trident Cover is NP-hard.

Note that since we are using real numbers in the Numerical Trident Cover Problem, the issue of encoding and input size should come up. We avoid this problem by always using numbers of the form $p + q\sqrt{2}$ in our Numerical Trident Cover instances, allowing for an efficient encoding simply by encoding $p + q\sqrt{2}$ as $(p, q)$. In fact, the problem is still hard even if the numbers are further restricted to be integers, though that reduction requires a bit more work, and is therefore omitted here.

Reduction 1: From Grid Triangle Cover to Numerical Trident Cover.

Suppose we are given an instance of the Grid Triangle Cover problem consisting of a set $S \subseteq \mathbb{Z}^+ \times \mathbb{Z}^+$ and a number $k$.

Then we construct an instance of Numerical Trident Cover (consisting of a list of real numbers $x_1, ..., x_N$, a pair $a, b$, and a target number of tridents $k'$) as follows.

Let the elements of $S$ be $s_1 = (p_1, q_1), s_2 = (p_2, q_2), ..., s_{|S|} = (p_{|S|}, q_{|S|})$. For each $i$ from $1$ to $N = |S|$ let $x_i = -p_i + q_i \sqrt{2}$. Let $a = 1$ and $b = \sqrt{2}$. Finally, let $k' = k$. This is the output instance of Numerical Trident Cover.

This reduction is clearly a polynomial time operation, so the only thing left to show is that the reduction is answer preserving.

To do this, consider the "reasonable" places to put the tridents. The only places where we can put a trident so that it hits at least one $x_i$ are locations of the form $x_i$, $x_i + a$, or $x_i - b$. For each of the $x_i$s, these three values are all of the form $-v_a + v_b \sqrt{2}$ for some integers $v_a$ and $v_b$. Thus we can restrict our attention to numbers of the form $-v_a + v_b \sqrt{2}$. Define the bijection $f$ between the set of all $p + q \sqrt{2}$ and the set of all pairs of integers according to the rule $f(-v_a + v_b\sqrt{2}) = (v_a, v_b)$. Note that $f$ maps $x_i$ to $s_i$.

Also note that if a trident is located at $-p + q\sqrt{2}$ then its three prongs are located at $-(p+1) + q\sqrt{2}$, $-p + q\sqrt{2}$, and $-p + (q+1)\sqrt{2}$. In other words, the image of the three prongs under $f$ consists of points $(p,q)$, $(p+1, q)$, and $(p, q+1)$. The image of a trident under $f$ is exactly a triangle of the form we are using to cover the values in $S$. Similarly, every properly oriented triangle maps to a trident under $f^{-1}$. In fact, the triangles and tridents are in exact bijection under $f$.

Since $f$ is bijective, it is clearly the case that some set of tridents covers $\{x_1, ..., x_{|S|}\}$ if and only if the images of those tridents under $f$ cover $S = \{s_1, ..., s_{|S|}\} = \{f(x_1), ..., f(x_{|S|})\}$. Then since the image of a trident under $f$ is a side-length-$(1,1\sqrt{2})$ triangle in the proper orientation, we can conclude that we can cover the $x_i$s with $k$ tridents if and only if we can cover the set $S$ with $k$ side-length-$(1,1\sqrt{2})$ triangles in the proper orientation. We conclude that the reduction is answer preserving.

Reduction 2: From Planar 3SAT to Grid Triangle Cover.

For this reduction, we are given a 3SAT instance in the form of a planar bipartite graph. The vertices in one part correspond to variables, and the vertices of the other part, each of degree 3, correspond to clauses. Each edge is labeled as positive or negative, indicating which way the variable is included into the clause (positively or negatively).

Then we can construct a Grid Triangle Cover instance $(S, k)$. We can construct $S$ out of variable gadgets, clause gadgets, and wire gadgets. After describing these gadgets and their desired behaviors, we will be able to describe how $k$ is computed.

First we describe a wire. A wire consists of a sequence of an odd number of points (in the integer lattice) where the first and last are called terminals such that every consecutive pair can be covered by a triangle without the triangle hitting any other point in the wire. As an example consider the following wire:

xoo       x
   o       o
   o ooo   o
   o o  oooo
    oo

The point of a wire is that it can be satisfied using a minimum number of covering triangles in two ways. In particular, if $p$ is the number of non-terminal points in the wire ("o"s in the above example) then $\frac{p+1}{2}$ triangles are necessary and those triangles will, in addition to covering the non-terminal points, cover exactly one of the two terminals.

Here we show the two ways to cover the example from above (where two points are labeled the same number if they are covered by the same triangle):

x11       9
   2       9
   2 556   8
   3 4  6778
    34

or

112       x
   2       9
   3 566   9
   3 5  7788
    44

One concern is that we might wish to connect two terminals with a wire but be unable to do so because any "wire" between those two terminals would have even length. However, that is not the case: we can always choose a route for a wire to make that wire have odd length (and therefore be a valid wire). Replacing any horizontal segment of wire of length 6 with the following length 7 wire segment can fix the parity of the wire length:

oo  oo
  ooo

Next we introduce a clause gadget. A clause simply connects one of the terminals of three wires in such a way that if one of the wires is satisfied so that the shared terminal is covered, then the triangle covering that shared terminal does not cover any points from the other wires:

      o
      o
      o
   ooox
       ooo

In order for the shared terminal to be covered, at least one of the three wires must be satisfies in such a way that the triangles satisfying the wire do not cover the wires' non-shared terminal.

Finally, we introduce the variable gadget. The variable gadget is a large wire-like loop (of even length) with terminals optionally occurring to the side every three rows as follows:

oo
o o
o ox
o o
o o
o ox
o o
o o
o ox
o o
o o
o ox
o o
 oo

The variable can grow vertically to accommodate the necessary number of terminals The terminals on rows of even parity correspond to positive occurrences of the variable and those on rows of odd parity correspond to negative occurrences. As with wire, the non-terminal points of the variable gadget can be satisfied using the minimum number of triangles (half the number of points in the loop) in exactly two ways. Those two settings cover either all the positive occurrence terminals or all the negative occurrence terminals of the variable gadget.

Putting it all together is pretty obvious: we build the bipartite graph using variable gadgets, clause gadgets (shared terminals) and wires connecting the terminals. The total number of triangles necessary to cover the non-terminal points of the wires and variables is then the target number of triangles.

Clearly we cannot cover the entire grid with fewer than that triangles. Furthermore, we can be assured that the non-terminal points are each covered since the variables and wires will each be satisfied in one of the two ways described. Thus the only task is to satisfy the terminals.

At each variable, either all the positive or all the negative occurrence terminals will be satisfied by the variable gadget. The other terminals at the gadget have to be satisfied by their attached wires. Then the clause terminals can be satisfied if and only if every clause is attached to at least one wire whose other terminal did not already use up the wire (a wire whose other terminal was satisfied by its attached variable gadget). In other words, the terminals are all satisfied if and only if the assignment of variables according to the settings of the variable gadgets satisfies every clause.

As you can see, the produced Grid Triangle Cover instance is a yes instance if and only if the input Planar 3SAT instance is a yes instance. Since this reduction is also polynomial time (all of the gadgets require space polynomial in the size of the input instance), we conclude that we have a valid reduction.


Encoding sets of permutations with a generating set and a set of excluded elements

If you are storing random permutations with probability ${1\over2}$ then you are going to need $log_{2}(n!)$ bits per permutation, Kolmogorov complexity dictates it.

If the distribution is non-random it depends.

To understand the state space it might help to look at http://oeis.org/A186202 , the size of any min dominating set over $S_{n}$ using a monogenic inclusion relation between permutations (ignoring the identity which is in all subgroups).

You can encode the relevant prime order permutations in $log_{2}( OEIS\_A186202(n) )$ bits each. That will give you some savings over the usual $log_{2}(n!)$ needed for a random permuation.


How many negations do we need to compute monotone functions?

Markov proved that any function of $n$ inputs can be computed with only $\lceil \log (n+1)\rceil$ negations. An efficient constructive version was described by Fisher. See also an exposition of the result from the GLL blog.
More precisely:

Theorem: Suppose $f : \{0,1\}^n \to \{0,1\}^m$ is computed by a circuit $C$ with $g$ gates, then it is also computed by a circuit $C^*$ with $2g + O(n^2 \log^2 n)$ gates and $\lceil \log (n+1) \rceil$ negations.

The main idea is to add for each wire $w$ in $C$ a parellel wire $w'$ in $C^*$ that always carries the complement of $w$. The base case is for the input wires: Fisher describes how to construct an inversion circuit $I(x) = \overline x$ with $O(n^2 \log^2 n)$ gates and only  $\lceil \log (n+1) \rceil$ negations. For the AND gates of circuit $C$, we can augment $a = b \land c$ with $a' = b' \lor c'$, and likewise for OR gates. NOT gates in $C$ cost nothing, we just swap the roles of $w$ and $w'$ downstream of the NOT gate. In this way, the entire circuit besides the inverter subcircuit is monotone.

A. A. Markov. On the inversion complexity of a system of functions. J. ACM, 5(4):331–334, 1958.
M. J. Fischer. The complexity of negation-limited networks - A brief survey. In
Automata Theory and Formal Languages, 71–82, 1975


What is an equivalent definition of mP/poly in terms of a Turing machine?

There is a notion of a monotone non-deterministic and, more generally, alternating Turing machine in the paper Monotone Complexity by Grigni and Sipser. Since polynomial time is the same as alternating logarithmic space, a machine characterization of uniform $\mathsf{mP}$ is the monotone alternating logspace Turing machine. Providing such a machine with polynomial advice will then give a machine definition of $\mathsf{mP/poly}$.


As commented by Serge Gaspers, for $k=0$ the problem is Sorting by Transpositions, and was introduced by Bafna and Pevzner in 1995. Its NP-hardness has been proved only in 2010; see Laurent Bulteau, Guillaume Fertin, and Irena Rusu, "Sorting by Transpositions is Difficult".


$\mathbb{N}$ in intensional MLTT with judgmentally commutative $+$ and $\times$

This is impossible.

Suppose that we have such a type $T$, with an implementation of addition $\mathit{add} : T \to T \to T$, which is judgementally commutative.
Because MLTT is strongly normalising, we know that we can put $\mathit{add}$ in $\beta$-normal, $\eta$-long form.
Now suppose that we have two variables $x, y$ of type $T$.
Now consider the terms $\mathit{add}\,x\,y$ and $\mathit{add}\,y\,x$.
Substituting $x$ and $y$ for the formal parameters of $\mathit{add}$ will not create any new $\beta$-reducible expressions, because $x$ and $y$ are neutral terms.
Now, $\eta$-expand the occurences of $x$ and $y$ as demanded by the definition of $T$.
Now, the resulting terms will be identical except that we've permuted the occurences of $x$ and $y$.
Recall that judgemental equality for $\beta$-normal, $\eta$-long terms is just $\alpha$-equivalence.
Since we assumed $\mathit{add}\,x\,y$ and $\mathit{add}\,y\,x$ were assumed to be judgementally equal, this means that the normal forms for these two terms are $\alpha$-equivalent.
Since anywhere that $x$ occurs in the normal form for $\mathit{add}\,x\,y$, a $y$ occurs in the corresponding position of the normal form for $\mathit{add}\,y\,x$, the only way that these two terms can be $\alpha$-equivalent is if neither $x$ nor $y$ occurs in the term.
This means that $\mathit{add}\,x\,y$ and $\mathit{add}\,y\,x$ do not use their arguments!
As a result, we can conclude that $\mathit{add}\,1\,1$ and $\mathit{add}\,0\,0$ are also judgementally equal.
Therefore $T$ cannot be the natural numbers, since $2$ and $0$ must not be judgementally equal.


If $F_3$ and $F_2$ are both monotone, satisfiability can be checked in polynomial time (or even in coNLOGTIME), as $F_3\land F_2$, which is also monotone, is satisfiable iff it is satisfied by the $\vec1$ assignment, that is, iff it does not contain the empty clause.
If one of the formulas is allowed to be monotone and the other one negated monotone (i.e., having only negative literals), then satisfiability of $F_3\land F_2$ is NP-complete: given a 3-CNF $F$ in variables $x_1,\dots,x_n$, let $F_3$ be the monotone 3-CNF obtained from $F$ by replacing all negative literals $\neg x_i$ with new variables $y_i$, and let $F_2=\bigwedge_i(\neg x_i\lor\neg y_i)$. Then $F$ is equisatisfiable with $F_3\land F_2$.
In particular, if $(\vec x,\vec y)$ is a satisfying assignment for $F_3\land F_2$, then for each $i$, at most one of $x_i$ or $y_i$ gets value $1$, that is, $y_i\le\neg x_i$. Thus, if we modify the assignment so that $y_i:=\neg x_i$, it will still satisfy $F_3$ as it is monotone. It follows that $\vec x$ satisfies the original formula $F$.


What constitutes denotational semantics?

The distinction I personally make between denotational and operational semantics is something like this:

denotational semantics is mathematical and equational. The details of the reduction matter less than the end result, which is a timeless value in some mathematical space.
operational semantics is algorithmic. It unfolds in individual steps in time.  The process is part of the the meaning, and the end result is just a distinguished step in that process.

The difference can sometimes be quite subtle, and it can be hard to tell if it is just a difference in style, or in substance.

However, we can see how Andrej's compositional definition follows more naturally from the denotational definition, and we can also easily imagine a non-confluent, non-compositional semantics that still meets the operational definition.


Smallest representatives of a quotient by an equivalence relation

It seems to me that your question is too general to answer.  Let me focus on the case of ∼L.  Then here is an example which shows a lower bound; namely, the length of a representative can be at least $e^{(1-o(1))\sqrt{n \ln n}}$, where n is the number of states of the minimum DFA.

We will actually show a lower bound on the length of a representative with respect to the right-equivalence relation RL on strings defined as: x RL y if and only if for all strings u, ux∈L ⇔ uy∈L.  Because equivalence relation RL is coarser than ∼L, any complete set of representatives with respect to ∼L must contain a complete set of representatives with respect to RL, and therefore a lower bound shown for RL applies also to ∼L.

Number-theoretic preparations.  Let pK be the Kth prime number.  We write the sum of the first K primes as Σ(K).  We also write the product of the primes that are less than or equal to N as N# (the primorial of N).  Then the following facts are known:

pK ∼ K ln K (from the prime number theorem).
Σ(K) ∼ K2 ln K (see the MathWorld article on prime sums).
ln(N#) ∼ N (see the MathWorld article on Chebyshev functions).

By combining these facts, we obtain that $\lim_{K\to\infty}\frac{\ln(p_K \#)}{\sqrt{\Sigma(K) \ln \Sigma(K)}} = 1$, and therefore $p_K \# = e^{(1-o(1))\sqrt{\Sigma(K) \ln \Sigma(K)}}$.

(I think that this final statement is a standard fact in the number theory, but I do not know a good reference for it.  See a related discussion in comments to this post.)

Construction and analysis.  For k∈ℕ, construct a DFA Mk on the alphabet {0, 1} as follows.  Let K=2k.  First, there is a complete binary tree of depth k rooted at the initial state.  Label the K leaves of this binary tree as q1, …, qK.  At each qi, we add a cycle of length pi, labeling each edge of the cycle with both 0 and 1 (that is, once you reach state qi, only the length of the rest of the string matters).  Mark the K states q1, …, qK as accepting states.

If x RL y, then we have that |x|≡|y| (mod pi) for every i≤K by prepending the binary notation of i−1 and some string of an appropriate length to both x and y.  This means that any complete set of representatives with respect to the relation RL contains at least one string with length at least pK#−1.

The number of the states in DFA Mk is K−1+∑i=1K pi = Σ(K)+K−1.  If we denote this number as n, then n ∼ Σ(K), and the length of at least one representative must be at least $p_K \# - 1 = e^{(1-o(1))\sqrt{n \ln n}}$.


Accomplished autodidact theoretical computer scientists

In addition to some of the great people listed in the comments, Gregory Chaitin independently developed much of Kolmogorov complexity while he was a highschool student in New York city.


Do there exist groups with word problems in arbitrary P-degrees?

I think this is not known. (I apologize - I think I was also one of the people that said I had remembered reading this somewhere.) For example, I believe that Sapir-Birget-Rips, Annals of Math 2002 were the first to show the existence of a group with $\mathsf{NP}$-complete word problem (which would be a trivial consequence of the result asked for in this question). Their Corollary 1.1 states:

  There exists a finitely presented group with NP-complete word problem. Moreover, for every language $L \subseteq A^*$ for some finite alphabet $A$ there exists a finitely presented group $G$ such that the nondeterministic time complexity of $G$ is polynomially equivalent to the nondeterministic time complexity of $L$.

While the second half of this corollary is kind of in a similar spirit to this question, it is a far cry from proving that every $\leq_T^p$-degree contains a word problem.


Is graph isomorphism in UP ${\cap}$ coUP?

Graph isomorphism is not known to be in $\mathsf{UP}$ nor known to be in $\mathsf{coUP}$.

For $\mathsf{UP}$: the natural nondeterministic algorithm - guess a map between the two graphs and check if it's an isomorphism - has either 0 witnesses (iff the graphs are not isomorphic) or $|\text{Aut}(G)|$ witnesses. Although most graphs have $|\text{Aut}(G)|=1$ (that is, if you pick a random graph on $n$ vertices, the probability that it has any nontrivial automorphsims goes to $0$ quite quickly with $n$), this is not enough to say that there is always at most one witness. This of course does not rule out some other algorithm that could show that graph isomorphism in $\mathsf{UP}$. (After all, it's possible that graph isomorphism is in $\mathsf{P} \subseteq \mathsf{UP}$.)

As for $\mathsf{coUP}$, as pointed out by Peter Shor, we don't even known if graph isomorphism is in $\mathsf{coNP}$, so we certainly don't know if it's in $\mathsf{coUP}$. (Under a plausible derandomization assumption it is in $\mathsf{coNP}$, but I don't know any natural assumption that puts it in either $\mathsf{UP}$ or $\mathsf{coUP}$.)


Are the Actor Model and Process Algebra "equivalent"?

This question is too vague to admit a clearcut answer, but it points towards a fascinating research field. The key problem is that neither is the actor model formally well-defined, nor is the notion of equivalency between (formalised) models of computation clear. Defining what expressivity of programming languages means precisely is a wide open problem, particularly for models of concurrent computation. It's unlikely that there is one clearcut notion of expressivity. Instead, language expressivity would appear to be parametric in properties of interest. Joachim Parrow's paper Expressiveness of Process Algebras gives an overview of the problem area, and explains some approaches that have been used to tackle it. There's even an annual conference -- Express -- dedicated to this question.

Process calculi such as CCS, CSP or π-calculi were developed in parts to offer a formalisation of actors, but are themselves of varying expressivity w.r.t. various elaborations of the latter concept. Even seemingly small variations in the operations a process calculus offers leads to huge expressivity gaps w.r.t.  various notions of expressivity.


Delaunay triangulation when some triangles have been pre-specified?

Just insert sufficient number of points along the edges of the triangle you want - if you insert enough points, the edges of the triangle you want would be the union of edges of the triangulation. It is not pretty but it would work. This the basic idea behind many of the constrained triangulation meshing algorithms. Here is a nice paper on the topic, which contains more information:

https://people.eecs.berkeley.edu/~jrs/papers/2dj.pdf


Modifying Hopcroft-Karp algorithm to get approximate bipartite matching

This is a combination of comments from me and Chandra Chekuri above, elaborated a bit.

As background, if you have a partial matching then its symmetric difference with the optimal matching can be decomposed into disjoint alternating paths (and possibly also some alternating cycles but those can be ignored). Hopcroft–Karp maintains a partial matching as it proceeds in a sequence of stages. Each stage exhausts all the shortest alternating paths left over from the previous stage, and increases the shortest alternating path length by at least two (because the length must be odd). Each stage takes linear time. The exact algorithm can be proven to take $O(\sqrt n)$ stages, leading to a nonlinear total runtime.

First, the additive approximation. If the shortest alternating path length is $k$, then the symmetric difference between your matching and optimal can have at most $n/k$ disjoint alternating paths, so the difference in cardinality between your matching and optimal is at most $n/k$. So if you set $k=1/\epsilon$ for your favorite constant $\epsilon$, and stop after $k/2$ stages, you should get an additive approximation of $\epsilon n$ to the optimal matching, in time $O((m+n)/\epsilon=O(m+n)$.

Now, for a multiplicative approximation, again suppose that the shortest alternating path length is $k$, and observe that each alternating path includes at least $(k-1)/2$ edges that are already part of your matching. So the ratio between the number of edges you already have in the alternating paths and the number you can get by adding one more edge per alternating path is at most $$\frac{k-1}{2}\left/\left(\frac{k-1}{2}+1\right)\right.\approx 1-\frac{2}{k}.$$ Therefore, if you set $k\approx 2/\epsilon$, and again do only $k/2$ stages before stopping, you will get a $(1-\epsilon)$-approximation, again in time $O(m+n)$.


Does k-PATH admit a constant approximation?

Karger, Motwani and Ramkumar (1997) discuss this question.
They show that if any polynomial-time algorithm can approximate the longest path to a ratio of $2^{O(\log^{1−\epsilon} n)}$, for any $\epsilon>0$, then NP has a quasi-polynomial deterministic time simulation; this results even holds for graphs of bounded degree.

  David R. Karger, Rajeev Motwani, G. D. S. Ramkumar:
  On Approximating the Longest Path in a Graph.
  Algorithmica 18(1): 82-98 (1997)


Can we replace deterministic part of alternative turing machine with some other equivalent machines?

I think you need to work on what $(0.2)^2$ is before you go any further.


Union-find is a beautiful problem whose best algorithm/datastructure (Disjoint Set Forest) is based on a spaghetti stack. While very simple and intuitive enough to explain to an intelligent child, it took several years to get a tight bound on its runtime. Ultimately, its behavior was discovered to be related to the inverse Ackermann Function, a function whose discovery marked a shift in perspective about computation (and was in fact included in Hilbert's On the Infinite).

Wikipedia provides a good introduction to Disjoint Set Forests.


Ways to think formally about Satisfiability Modulo Theories

It's actually surprisingly hard to relate SMT to type-theoretic/categorical approaches to logic -- the results in this area are very recent! This is because categorical logic is primarily conceived of as a semantics of proofs, and SMT arises from the model-theoretic view of logic, which is a semantics of provability.

A formula in SMT is a boolean combination of primitive assertions over some theory. For example, for linear arithmetic you might have the following terms and primitive formulas.

$$
\newcommand{\bnfalt}{\;\;|\;\;}
\array{
\mbox{Terms} & t & ::= & x \bnfalt n \bnfalt t + t \bnfalt -t \\
\mbox{Primitive Formulas} & p & ::= & t \leq t \bnfalt t = t \bnfalt t < t \\
\mbox{SMT Formulas} & \phi & ::= & p \bnfalt \top \bnfalt \phi \land \phi' \bnfalt \lnot \phi \\
}$$

Given a formula $\phi$, an SMT solver will either give you a satisfying assignment for the variables -- i.e., it will give you a number for each variable, such that substituting that number for each variable gives you a true boolean formula -- or it will tell you that the formula $\phi$ is unsatisfiable.

The fact that this is all happening in classical logic is quite important; the architecture of SMT solvers relies upon this fact. Basically, SMT solvers are built as a combination of an DPLL-based SAT solver, which communicates with a theory solver, which deduces equalities from pure conjunctions of theory formulas. There are also various conditions under which you can combine solvers for different theories, which is important because it gives researchers a good "API" for figuring out if particular theories will fit together nicely.

A good reference to the standard view of SMT is Clark Barrett and Cesare Tinelli's handbook chapter on Satisfiability Modulo Theories.

Work on how to interpret SMT in terms of proof theory is much newer. The basic idea is to relate DPLL(T) with "focused" or "polarized" calculi for proof search. Focused calculi are variants of the sequent calculus originally designed to optimize proof search, but which turned out to work because they expose fundamental ideas in proof theory.

Two good references to this are
Mahfuza Farooque's PhD thesis, Automated reasoning techniques
as proof-search in sequent calculus, in which she relates the actions of a DPLL(T) algorithm to search in a particular focused calculus, and Stéphane Graham-Lengrand's habilitation thesis Polarities & Focussing: a journey from Realisability to Automated Reasoning, in which he gives a broader perspective on this work (eg, by connecting it to work on biorthogonality).


Random sampling data structure with removal

Copying my comment on that from here:

There exist published algorithms that support sampling from discrete probability distributions in O(1) time, AND modifying the distribution in O(1) time per update:

Hagerup, T., K. Mehlhorn, and J. I. Munro. "Optimal algorithms for
generating discrete random variables with changing distributions."
Lecture Notes in Computer Science 700 (1993):
253-264.
Matias, Yossi, Jeffrey Scott Vitter, and Wen-Chun Ni. "Dynamic
generation of discrete random variates." Theory of Computing Systems
36.4 (2003): 329-358.

These papers are a little unsatisfactory in that they are theoretical algorithms in a model that doesn't fully deal with issues of numerical precision and bit complexity. This can be an issue in practice if the probability distribution has some entries that are much larger than others. Consequently, in the application I had, I used some of the ideas from these papers, but implemented something else that was more practical.

EDIT: What I implemented was a bucketing system. Assume without loss of generality that each weight (non-normalized probability) is a power of 2.(Normalize so each weight is a 64-bit integer. Round each weight up to its nearest power of 2, then sample from the rounded weights instead.  When you sample a value $i$ that has been rounded up to $2^k$, only actually take it with probability $i/2^k$, and otherwise resample. You get at most 1 repeat in expectation.)  Keep all rounded weights with the same value $2^k$ in a single bucket indexed by $k$.  As you do updates, keep track of the currently largest rounded weight $2^K$, the sum of the weights in each bucket, and the total weight $W$.

To sample, draw a random integer $x$ in $[1,W]$, start from the non-empty bucket that holds the largest weight $2^K$.  If $x$ is at most the sum of the weights in the bucket, take the $j$th item in this bucket, where $j$ is something like $\lceil x/2^K\rceil$. Oherwise subtract the sum of the weights in the bucket from $x$ then recurse with the bucket that holds $2^{K-1}$.

If you have a weight distribution with very high ratio of largest weight to smallest weight, classify a weight as small if its ratio to the maximum weight is less than, say, $1/n^3$.  Let $2^k$ be the smallest power of 2 larger than all small weights, and round each small weight up to $2^k$ (instead of its next largest power of 2).  (This may be necessary in order to use 64-bit integer arithmetic to keep track of the exact total weight $W$.) If you happen to sample a small weight $i$ that has been rounded up to $2^k$, as before you only keep it with probability $i/2^k$, and otherwise resample.  The probability of keeping it can be small, but the probability that you draw any such item is, say, $O(1/n^3)$, so you still do $O(1)$ resamples in expectation.

Now you have at most $3\log_2 n$ buckets, and worst-case (expected) time per sample is $O(\log n)$.  As you delete weights, when the total weight of the small items reaches, say, a $1/n^2$ fraction of the total weight, reclassify the small items, taking some out of the "small-item" bucket.  This happens $O(\log X / \log n)$ times, where $X$ is the ratio of largest weight to smallest weight.

You can get time $\Theta(\log n)$ for some distributions (e.g., for each $k\le \log n$ you have $2^k$ items of weight $n/2^k$).  But in practice I was getting small constant sample time and update time.


What is the complexity of the set of closed boolean tautologies assuming well formed formulae?

The answer to all three questions is negative. Consider e.g. the prefix version (3), and assume for contradiction that it is decidable by a (wlog deterministic) automaton $A$ with $m$ states. Consider the strings

$$\begin{align}
u_k&={+}^{m-k}{*}{+}^k,\\
v_l&=1^{l+1}0^{m-l+1}.
\end{align}$$

Notice that $u_kv_l$ is a well-formed Boolean sentence for every $0\le k\le m$, $0\le l\le m+1$, and it is easy to see that $u_kv_l$ evaluates to $1$ iff $k<l$. By the pigeonhole principle, there are $0\le k<l\le m$ such that $u_k$ and $u_l$ land in the same state of $A$, thus $u_kv_l$ and $u_lv_l$ are both accepted or both rejected. However, the former evaluates to $1$, and the latter to $0$.

For infix formulas (questions 1,2), one can use in a similar way formulas of the form

$$(0+((0+\cdots((0+((1+((0+\cdots((0+0)*1))*1))\dots*1))*0))*1))\dots*1)).$$

The argument in fact shows that any deterministic automaton evaluating well-formed Boolean sentences of length $n$ must have size $\Omega(n)$, or in other words, any online algorithm for evaluation of such sentences needs space at least $\Omega(\log n)$. This bound is tight: as shown by Buss, it is possible to evaluate Boolean sentences in infix notation in online space $O(\log d)$, where $d$ is the depth of the formula (i.e., maximum nesting of brackets). (The paper advertises it as an online $O(\log\log n)$-space algorithm for evaluation of balanced formulas, using the fact that these have depth $d=\log n$.)

On the other hand, as also shown by Buss, Boolean sentence evaluation (in either prefix or infix notation) can be done in ALOGTIME, aka uniform $\mathrm{NC}^1$, and it is in fact complete for this class under DLOGTIME many-one reductions. Since regular languages with unsolvable syntactic monoid (for example, $\bigl((a|b)^3(ab^*a|b)\bigr)^*$) are also $\mathrm{NC}^1$-complete, it follows that one can reduce Boolean sentence evaluation in DLOGTIME to a regular language.


To the best of my knowledge, no heap data structure matches your requirements. In terms of complexity, the best one is the Brodal queue, a heap data structure with worst case $O(1)$ time for insertion, find-minimum, meld (merge two queues) and decrease-key, and $O(\log~n)$ for delete-minimum and general deletion. However, this data structure is only of theoretical interest.

If you depart from the comparison-based model and adopt the RAM model where keys are regarded as binary strings, each one contained in one or more machine words, the best you can achieve for both insert and delete operations $\mathcal{O}(\sqrt{\log \log n}) $. See my answer to this question.


Does the following 2-rounds distributed algorithm approximates a maximal matching well?

No. For the following graph the expected size of the generated matching is $O(\sqrt n)$, but any maximal matching has size $\Theta(n)$.

The graph consists of a $k$-vertex core $C$ and a matching $M_0$ of $k^2$ edges and vertices (disjoint from $C$), plus all edges $(u,w)$ where $u\in C$ and $w\in M_0$.

lemma 1. Any maximal matching $M$ has $\Omega(k^2)$ edges

Proof. Every edge in $M_0$ is either in $M$ or is touched by an edge in $M$ into $C$, but all at most $k$ edges of $M$ can touch $C$. QED

lemma 2. In your random process, the expected number of edges chosen in the random matching is $O(k)$.

Proof.  Clearly at most $k$ edges are chosen that are not in $M_0$ (as there are only $k$ vertices in $C$).  For a given edge $(u,w)$ in $M_0$, the chance that it is chosen is $O(1/k)$, because, given that, say, $u$ is active and $w$ is passive, the chance that $u$ picks $w$ is $O(1/k)$, as $w$ has $k$ other edges (to $C$). QED

(One thing you can prove about your process is that, for any graph, in expectation, a constant fraction of the edges will touch the edges in the generated matching.  See e.g. here.  Roughly, if you direct each edge $(u,w)$ from the lower-degree vertex to the higher-degree vertex, and call a vertex good if more than one-third of its incident edges are directed into it, then at least half the edges must be directed into good vertices (Lemma 6).  And each good vertex has constant probability of being matched in your process.  So, at least half the edges touch vertices that have a constant probability of being matched.

EDIT: So after $O(\log n)$ rounds of your process, it will have a maximal matching with high probability.)


Is there such a thing as a state-based programming language?

The short answer is no.

The long answer is that such languages are invented on a regular basis, but if they see any significant degree of use, for good semantic reasons they never remain in this mode for very long.

The basic problem is that it is very difficult to build programs compositionally using state machines. The modular construction of programs rests on two pillars: the variable, and the procedure abstraction. Variables let you define data in one place, and use it in another, and procedures let you parameterize a computation by some data. Without these features, it is extremely hard to build larger programs out of smaller programs.

State machines lack both of these features, and one of the first nontrivial theorems of computability (the $snm$ theorem) is the proof that Turing machines can implement them. However, the $snm$ theorem is too impractical to use as a practical calling convention, since it essentially says that the calling convention for programs is to  pass arguments by passing strings which are interpreted as programs. This doesn't matter for the purposes of computability theory, but it ends up imposing order-of-magnitude slowdowns in practice (i.e., "interpretive overhead"). So people invariably add a primitive variable and procedure call mechanism to every language that sees serious use.

In fact, the lambda calculus demonstrates that you can build a Turing complete language out of nothing but variables and procedural abstractions. Unlike TMs, however, it's surprisingly practical to program in pure lambda calculus. The technical reason for this is that both lambda calculus and TMs form "closed categories" -- that is, they have the algebraic structure necessary to represent variables and procedures. However, the lambda calculus turns out to be basically a syntactic presentation (in the sense of generators and relations) of this algebraic structure, and so it makes it a lot more convenient to work with this structure.


Maximal Clique partition of vertices with smallest number of cut edges

This problem is the Cluster Edge Deletion problem.

  Given a graph $G = (V,E)$ and an integer, can we delete at most $k$ edges $F \subseteq E$ such that $G-F$ is a cluster graph?

A cluster graph here is a graph whose connected components are cliques.

The approximability of Cluster (Edge) Deletion, was studied by Shamir, Sharan, and Tsur (Cluster graph modification problems. Discrete Applied Mathematics, 144(1):173–182, 2004).  They show that the problem is NP-hard to approximate within a constant factor:

  Theorem 12. There is some constant $\epsilon > 0$ such that it is NP-hard to approximate Cluster Deletion to within a factor of $1 + \epsilon$.


The answer is no, me think.

To see why consider two lines that are a perturb copy of each other that intersect at a point p. By giving one line weight 1, and one line weight -1, we created a tiny wedge where the path can not go through. Think about this wedge now as a ray. Now, using a collection of such rays, we can create the following configuration:

------------------------

             -----------------------------------

-------------------------

             --------------------------------

--------------------------

That is - interleaving horizontal rays. Now, the path must wiggle between these rays in the natural way. It is now trivial to add an almost vertical ray that its tail (i.e., non ray part) intersect all the horizontal rays. The path must intersect the two lines defining this ray as many times as we want.

Here is a figure:

(source: uiuc.edu)

(Ipe source.)

The solution is slightly more complicated because these rays open up. By adding the two rays on the sides, one guarentees that only the region of interest is really relevant.


Where is relational parametricity in hyperdoctrine or topos models explored?

For technical reasons, there hasn't been much work on parametric topos models. The internal logic of a topos is a form of set theory, and F-style impredicative indexing and the powerset axiom are incompatible. See Andy Pitts's Non-trivial Power Types Can't Be Subtypes of Polymorphic Types:

  This paper establishes a new, limitative relation between the polymorphic lambda calculus and the kind of higher-order type theory which is embodied in the logic of toposes. It is shown that any embedding in a topos of the cartesian closed category of (closed) types of a model of the polymorphic lambda calculus must place the polymorphic types well away from the powertypes, P(X), of the topos, in the sense that P(X) is a subtype of a polymorphic type only in the case that X is empty (and hence P(X) is terminal). As corollaries, we obtain strengthenings of Reynolds' result on the non-existence of set-theoretic models of polymorphism.

As a result, even though you can give a universe interpreting F's types in topos logic, you can't let it interact in interesting ways with the full universe of sets. However, all is not lost!

The fact that a (non-parametric) universe of sets interpreting System F means that you can give a parametric model of System F in the internal logic of the topos, much more easily than you can in ordinary set theory. Essentially, you don't have to muck around with PERs, since you can just assume that you have a suitable collection of sets. Bob Atkey used this idea in his paper Relational Parametricity for Higher Kinds, where he worked out parametricity for $F_\omega$ by working in the impredicative calculus of constructions.
Another reaction to Pitts's result is to not work with a set theory, but a dependent type theory. Since there's no power type former in dependent type theory, you don't have to worry about the interaction of power types and polymorphism. See Atkey, Ghani and Johann's A Relationally Parametric Model of Dependent Type Theory.

However there are no such obstacles to building hyperdoctrine-ish models, where terms of System F are objects of the logic. Research along these lines was probably initiated by Abadi and Plotkin in their seminal paper A Logic for Parametric Polymorphism. Lars Birkedal and his collaborators have worked heavily on formulating categorical models for this and similar logics --- see in particular Birkedal, Møgelberg, and Petersen's Category-Theoretic Models of Linear Abadi and Plotkin Logic, which gives a logic for reasoning about linear System F, plus a proof that it is sound and complete with respect to a certain class of categorical models.


Define the language $BACKPOINTER$ to have words of length $n+t\log n$, divided to $1+t$ parts, one of length $n$ and the rest of length $\log n$, by commas such that $BACKPOINTER=\{(x,p_1,\ldots,p_t)\mid x_{p_i}=1 \forall i\}$.
It should follow from some standard one-way communication complexity bound that $BACKPOINTER$ needs at least $t$ bits of memory stored after $x$ is read. So for any $t\gg \log n$, $BACKPOINTER\in L\setminus 1NL$.

ps. Note that $BACKPOINTER\in 1co\text{-}NL$.


Fixed point theorems for constructive metric spaces?

The axiom of choice is used when there is a collection of "things" and you choose one element for each "thing". If there is just one thing in the collection, that's not the axiom of choice. In our case we only have one metric space and we are "choosing" a point in it. So that's not the axiom of choice but elimination of existential quantifiers, i.e., we have a hypothesis $\exists x \in A . \phi(x)$ and we say "let $x \in A$ be such that $\phi(x)$". Unfortunately, people often say "choose $x \in A$ such that $\phi(x)$", which then looks like application of the axiom of choice.

For reference, here is a constructive proof of Banach's fixed point theorem.

Theorem: A contraction on an inhabited complete metric space has a unique fixed point.

Proof. Suppose $(M,d)$ is an inhabited complete metric space and $f : M \to M$ is a contraction. Because $f$ is a contraction there exists $\alpha$ such that $0 < \alpha < 1$ and $d(f(x), f(y)) \leq \alpha \cdot d(x,y)$ for all $x, y \in M$.

Suppose $u$ and $v$ are fixed point of $f$. Then we have $$d(u,v) = d(f(u), f(v)) \leq \alpha d(u,v)$$ from which it follows that $0 \leq d(u,v) \leq (\alpha - 1) d(u,v) \leq 0$, hence $d(u,v) = 0$ and $u = v$. This proves that $f$ has at most one fixed point.

It remains to prove the existence of a fixed point. Because $M$ is inhabited there exists $x_0 \in M$. Define the sequence $(x_i)$ recursively by $$x_{i+1} = f(x_i).$$ We can prove by induction that $d(x_i, x_{i+1}) \leq \alpha^i \cdot d(x_0, x_1)$. From this it follows that $(x_i)$ is a Cauchy sequence. Because $M$ is complete, the sequence has a limit $y = \lim_i x_i$. Since $f$ is a contraction, it is uniformly continuous and so it commutes with limits of sequences: $$f(y) = f(\lim_i x_i) = \lim_i f(x_i) = \lim_i x_{i+1} = \lim_i x_i = y.$$
Thus $y$ is a fixed point of $f$. QED

Remarks:

I was careful not to say "choose $\alpha$" and "choose $x_0$". It is common to say such things, and they just add to the confusion that prevents ordinary mathematicians from being able to tell what is and isn't the axiom of choice.
In the uniqeness part of the proof people often assume unnecessarily that there are two different fixed points and derive a contradiction. This way they have only managed to prove that if $u$ and $v$ are fixed points of $f$ then $\lnot\lnot (u = v)$. So now they need excluded middle to get to $u = v$. Even for classical mathematics this is suboptimal and just shows that the author of the proof does not exercise good logical hygiene.
In the existence part of the proof, the sequence $(x_i)$ depends on the existential witness $x_0$ we get from eliminating the assumption $\exists x \in M . \top$. There is nothing wrong with that. We do that sort of thing all the time. We did not choose anything. Think of it this way: someone else gave us a witness $x_0$ for inhabitedness of $M$, and we are free to do something with it.
Classically, "$M$ is inhabited" ($\exists x \in M . \top$) and "$M$ is non-empty" ($\lnot\forall x \in M . \bot$) are equivalent. Constructively, the former makes more sense and is useful.
Because we showed uniqueness of fixed points we actually get a fixed-point operator $\mathrm{fix}_M$ from contractions on $M$ to points of $M$, rather than just a $\forall\exists$ statement.
Finally, the following fixed-point theorems have constructive versions:

Knaster-Tarski fixed-point theorem for monotone maps on complete lattices
Banach's fixed-point theorem for contractions on a complete metric space
Knaster-Tarski fixed-point theorem for monotone maps on dcpos (proved by Pataraia)
Various fixed-point theorems in domain theory usually have constructive proofs
Recursion theorem is a form of fixed-point theorem and it has a constructive proof
I proved that Knaster-Tarski fixed-point theorem for monotone maps on chain-complete posets does not have a constructive proof. Similarly, the Bourbaki-Witt fixed-point theorem for progressive maps on chain-complete posets fails constructively. The counter-example for the later one comes from the effective topos: in the effective topos ordinals (suitably defined) form a set and the successor maps is progressive and has no fixed points. By the way, the successor map on the ordinals is not monotone in the effective topos.

Now that's rather more information than you asked for.


Real computers have only a finite number of states, so what is the relevance of Turing machines to real computers?

To complete the other answers: I think that Turing Machine are a better abstraction of what computers do than finite automata.
Indeed, the main difference between the two models is that with finite automata, we expect to treat data that is bigger than the state space, and Turing Machine are a model for the other way around (state space >> data) by making the state space infinite. This infinity can be perceived as an abstraction of "very big in front of the size of the data". When writing a computer program, you try to save space for efficiency, but you generally assume that you won't be limited by the total amount of space on the computer. That is part of the reason why Turing Machines are a better abstraction of computers than finite automata.


Algorithm: Find the first k longest substrings between two similar strings

Depending on your application (and assuming I have correctly understood your general aim), a standard practical method will be to find all maximal repeated substrings between the two strings, number those substrings and then compute the longest increasing subsequence.  This is exactly what the bioinformatics tool Reputer does. See http://bibiserv.techfak.uni-bielefeld.de/reputer/ and
http://bioinformatics.oxfordjournals.org/content/15/5/426 for an original reference.

This is is slightly super-linear time overall as you have to compute the longest increasing subsquence (see e.g. http://en.wikipedia.org/wiki/Longest_increasing_subsequence ).


Minimum spanning tree over all vertex matchings

(Moved from comments) Here's an idea for getting a constant factor approximation, assuming P and Q satisfy the triangle inequality. I thought it might give a 2-approximation, but all I can prove right now is an approximation ratio of 4.

(1) In the problem as stated, the weight of edge $pq$ in the combined graph (after the correspondence $p$–$p'$ and $q$–$q'$ is determined) is $\max\{P(pq),Q(p'q')\}$. Instead, let's use $P(pq)+Q(p'q')$. This loses at most a factor of two but makes the problem easier to describe: we are now trying to find a spanning tree in $P$, and an isomorphic spanning tree in $Q$, with minimum total weight. The correspondence between $P$ and $Q$ is then given by the isomorphism between these two trees.

(2) In $P$, find a minimum spanning tree, and use the path-doubling Euler tour technique to find a path with at most twice the weight. Do the same thing independently in $Q$. The result is two isomorphic trees (both paths) that are separately at most twice the weight of their graph's MSTs, and therefore at most twice the cost of the solution to the minimum isomorphic spanning tree problem, and four times the weight of the original problem.

(3) The original problem is NP-complete, by a reduction from Hamiltonian path. Let $P$ be defined from a graph in which you wish to test the existence of a Hamiltonian path; define $P(pq)=1$ when $pq$ is an edge in $P$ and $2$ when $pq$ is not an edge. Let $Q$ be defined in exactly the same way from a path graph. Then there is a solution of total cost $n-1$ if and only if the graph from which $P$ was defined has a Hamiltonian path. Probably this can also be used to prove inapproximability below some fixed constant.


Berman-Hartmanis Isomorphism for NP$_{\mathbb{R}}$?

Depending on which version of $\mathsf{NP}_{\mathbb{R}}$ you use, yes or it's open. When one considers BSS machines that only use addition and subtaction, and only branch on equality, the answer is yes. If one includes branching on $<$, I believe it is still open, and the same if one allows multiplications. For details, see Cucker, Koiran, and Matamala "Complexity and dimension," Inform. Proc. Lett. 1997


So the answer is yes, as pointed out by in one comment with reference to the original paper.


What is the logarithm or root operation in type-space?

A type $C$ has a logarithm to base $X$ of $P$ exactly when $C \cong P\to X$. That is, $C$ can be seen as a container of $X$ elements in positions given by $P$. Indeed, it's a matter of asking to what power $P$ we must raise $X$ to obtain $C$.

It makes sense to work with $\mathop{log}F$ where $F$ is a functor, whenever the logarithm exists, meaning $\mathop{log}\!_X(F\:X)$. Note that if $F\:X\cong \mathop{log}F\to X$, then we certainly have $F\:1\cong 1$, so the container tells us nothing interesting other than its elements: containers with a choice of shapes do not have logarithms.

Familiar laws of logarithms make sense when you think in terms of position sets

$$\begin{array}{rcl@{\qquad}l}
 \mathop{log} (\mathop{K}1) &=& 0   & \mbox{no positions in empty container}\\
 \mathop{log} I &=& 1 & \mbox{container for one, one position}\\
\mathop{log} (F\times G) &=& \mathop{log}F+\mathop{log}G &
  \mbox{pair of containers, choice of positions} \\
\mathop{log} (F\cdot G) &=& \mathop{log}F\times\mathop{log}G &
  \mbox{container of containers, pair of positions}
\end{array}$$

We also gain $\mathop{log}\!_X(\nu Y. T) = \mu Z. \mathop{log}\!_X T$ where $Z=\mathop{log}\!_XY$ under the binder. That is, the path to each element in some codata is defined inductively by iterating the logarithm. E.g.,

$$\mathop{log}\mathop{Stream} = \mathop{log}\!_X(\nu Y. X\times Y) = \mu Z. 1 + Z = \mathop{Nat}$$

Given that the derivative tells us the type in one-hole contexts and the logarithm tells us positions, we should expect a connection, and indeed

$$F\:1\cong 1 \;\Rightarrow\; \mathop{log}F\cong \partial F\:1$$

Where there is no choice of shape, a position is just the same as a one-hole context with the elements rubbed out. More generally, $\partial F\:1$ always represents the choice of an $F$ shape together with an element position within that shape.

I'm afraid I have less to say about roots, but one could start from a similar definition and follow one's nose. For more uses of logarithms of types, check Ralf Hinze's "Memo functions, polytypically!". Gotta run...


Proof for Upper Bound of Sum of Square Roots Problem

Here is a rather sloppy proof sketch. Let $S = \sum_{i=1}^n \delta_i \sqrt{a_i}$ where $\delta_i \in \{\pm 1\}$. This is an algebraic number of degree at most $2^n$ and height at most $H = (max(a_i))^{n}$. Now it is easy to check if $S = 0$ (can be done even in $TC^0$ -- see this).If $S \neq 0$ then it is bounded away from $0$ by a quantity (because it is an algebraic number and hence is a non-zero root of a univariate polynomial) that is a function of the degree and height of the minimal polynomial of $S$. Unfortunately, the dependence on the degree is exponential in the number of square roots (and if the $a_i$'s are distinct primes, this degree bound is even tight, though that case of sign evaluation is easy to handle). The precision needed is hence exponential in the number of square roots, which is $2^n$-bits for $S$. It now suffices to truncate each of the $\sqrt{a_i}$ to say $2^{10n}$ bits to ensure the sign is guaranteed to be correct. This is easily done via polynomially many steps of Newton iteration). Now it is down to checking if the sum is positive, which is just addition and hence linear in the number of bits in the summands. Notice that this computation is in Polynomial time on a BSS machine. Also notice that we are not doing any computation directly with the minimal polynomial of $S$ itself, which could have huge coefficients and look ugly, we just use it to reason about the precision to which we need to truncate the square roots. For more details, check Tiwari's paper.


NP-hard problem on planar unit disk graph

Did you try doing a search for "planar unit disk graphs"? According to this paper the problem of finding the largest possible induced matching is NP-complete for planar unit disk graphs, according to this paper so is the minimum connected dominating set, and according to this paper so is the maximum number of disjoint dominating sets.


Coupon collector - the effect of randomization

$E[m]$ equals $n(H_n-1)$.

Here's a more complete proof sketch, following the argument suggested in my comment.

We start by showing that each permutation of the first $k-1$ elements is equally likely.

More precisely, let $X^*=(X_1,X_2,\ldots,X_K, \ldots)$ be an infinite random sequence where each $X_i$ is drawn independently and uniformly from $S$.  Let r.v. $K$ be the first index at which all elements of $S$ have been seen. Let r.v. $X'=(X_1,X_2,\ldots,X_{K-1})$.

Let $i$ denote any positive integer. Let $s$ denote any element of $S$.
Let $x=(x_1,x_2,\ldots,x_{i-1})$ denote any value of $X'$ that can occur,
given that $K=i$ and $X_K = s$.  (That is, $x$ is any length-$(i-1)$ sequence in which
each element of $S-\{s\}$ occurs, and $s$ does not occur.)

Let $\pi$ be any permutation of $[i-1]$.
Let $\pi(x)$ denote sequence $x$, permuted by $\pi$.

Lemma: Fix any such $i$, $s$, $x$, and $\pi$. Conditioned on $K=i$ and $X_k=s$, the probability that $X' = x$ is the same as the probability that $X' = \pi(x)$.

Proof.  To save typing, let $(i,s)$ denote the event that $K=i\wedge X_K=s$.

We want to show $\Pr[X'=x ~|~ (i,s)] = \Pr[X'=\pi(x) ~|~ (i,s)]$.

Let $x\prec X^*$ denote that $x$ is a prefix of $X^*$.
Let $x,s\prec X^*$ denote that $(x_1,\ldots,x_{i-1},s)$ is a prefix of $X^*$.
Note that
$$\Pr[X' = x ~|~ (i,s)]\,\Pr[(i,s)] ~=~ \Pr[X' = x \wedge (i,s)] ~=~ \Pr[x,s\prec X^*] ~=~ \frac{1}{n^i}.$$
Thus,
$$\Pr[X' = x ~|~ (i,s)] ~=~ \frac{1}{n^i \Pr[(i,s)]}.$$
Since the right-hand side is independent of $x$,
and $\pi(x)$ is also a possible value of $X'$,
$\Pr[X' = \pi(x) ~|~ (i,s)]$ also equals the right-hand side above.  QED

Corollary: Randomly permuting the first $k-1$ elements of $X$
(as described in the question) does not change the distribution of $X$.

This implies that the distribution of the r.v. $m$ as defined in the question
(with permutation of the first $k-1$ elements)
is the same as the distribution of $m$ if the elements are not permuted.
That is, $m$ is distributed as the first index at which $n-1$ distinct
elements in $S$ have been seen.  By a standard calculation,
$E[m]$ equals $n(H_{n}-1)$.


I'm not sure this is quite what you're looking for, since I've seen the "uncommon" proof in textbooks, but: the O(n log n) time bound for quicksort.

"Textbook" proof: set up a randomized recurrence relation, prove by induction that it has the desired solution.
"Uncommon" proof: find a simple formula for the probability that any two elements are compared (it's just 2/(d+1) where d is the difference between their ranks in the sorted order), and use linearity of expectation and harmonic series to compute the expected number of pairs that get compared.

The textbook proof requires less creative insight, but the uncommon proof introduces a technique that's very useful in other algorithm analysis e.g. for randomized incremental algorithms in computational geometry.


Is the convex combination of two potential games a potential game?

NO.

The following two-player game, with e very close to 0, is a potential game:

(e,0)   (e,1)

(0,0)   (0,e)

Taking the 8 equivalent games (switching the roles of the players / rows / columns), then a convex combination of them gets you as close as you want to any game with positive utilities, like to matching pennies with a positive constant added to each utility.  But that is not a potential game.


It is a special case of the transportation problem (or the minimum-cost flow problem), and so can be solved in polynomial time.  The coefficient matrix is totally unimodular since it is the incidence matrix of a bipartite graph.

The following Wikipedia articles could be useful.

http://en.wikipedia.org/wiki/Minimum_cost_flow_problem
http://en.wikipedia.org/wiki/Unimodular_matrix


Is testing two SO-Horn queries for equivalence decidable?

First, note that the equality of two TMs is harder than the halting problem (it is $\Pi^0_2$-complete), i.e. you can not compute it even with an oracle for the halting problem. So it is not even c.e. (i.e. $\Sigma^0_1$, a.k.a. r.e.). Rice's theorem implies that the set is not c.e., it does not imply the stronger result.

There is a complexity theoretic version of Rice's theorem (by D. Kozen), but that gives a weaker result, which is expected, we can check non-trivial properties if we know that the machine halts, e.g. we can check if the machine accepts when run on an empty tape. Intuitively the result says (kind of) that the only way to check non-trivial properties of language of TMs is to simulate the machines (if I remember correctly).

Descriptive complexity does not change things, so I think you can ignore it and just replace it with the TMs with polynomial clocks (they can be converted to descriptive complexity characterization and descriptive complexity characterization can be converted to characterization using TMs).

I think the question of deciding the equality of even simpler functions is co-c.e.-complete (i.e. $\Pi_1$-complete). We can not check if two multinomials are equivalent over natural numbers (since the complement is c.e.-complete by the MRDP theorem), and this implies that we cannot check the equality of two SO-Horn queries.


Local Smoothness vs optimisation in combinatorial problems

It sounds like you need to make your question much more precise or pick up a good book on smooth optimization and marvel at what smoothness makes possible. See for instance "Numerical Optimization" by Nocedal and Wright (Springer).


Let us first step back and say more precisely (mathematically) what "the Random Oracle Model (ROM)" is, because it is fundamentally different from an "assumption" as they are thought of in cryptography.

One way to formalize the ROM is to see it as alternative model of computation.  In particular, algorithms in this model of computation have a extra distinguished state (or subroutine, or circuit gate, whatever), that computes some function $H:\{0,1\}^\ast\to\{0,1\}^n$, where n is the security parameter.  An algorithm A is executed in this model by picking $H$ at random from all possible functions, and then running $A$ with its $H$ subroutine set to compute that function.

When we "analyze a protocol in the ROM", we mean first define the protocol via algorithms that have access to $H$, and then we prove a theorem about the protocol when it is attacked by adversaries that also have access to $H$.  The theorem will say that something happens with high probability, where the probability is over the choice of $H$, amongst other things.

This model of computation is not realistic, however, because we do not all have access to a truly random function.  So instead we take our algorithms (which were defined in the ROM) and set $H$ to something efficiently computable, like SHA-256.  Of course, the theorem does not actually cover such usage, but this approach is remarkably effective for avoiding wide classes of attacks against protocols.  We just hope ("assume") that things will work out for the protocols under consideration, but in general this assumption is false[1].

A cryptographic assumption, on the other hand, say something about the limitations of the "standard model of computation", i.e. Turing machines, circuit families, etc.  A distinguishing feature here is that assumptions might true, but the ROM will never "true".  This holds even for interactive assumptions that involve weird oracles - even a random oracle.

Things brings us to the point of confusion:  When you're sitting down to design a protocol (algorithm) and prove it secure in the standard model under an assumption, you can't assume that your algorithm has access to any oracles, because it needs to be an algorithm in the usual sense.  Even if your assumption has a random oracles represented somewhere in it, you still need to give a well-defined algorithm or protocol.

[1] See "The random oracle methodology, revisited" by Ran Canetti, Oded Goldreich and Shai Halevi.


Maximize the expected number of "losers" - Is it NP-hard?

Look at the graph that is formed by the comparisons. Each element corresponds to a vertex. If an element is a vertex of degree $d$, then the probability that it will be the lowest in at least one of these comparisons is the probability that it is not larger than all of its neighbors. This probability is $d/(d+1)$.

Now, expectation is linear. This means that the expected number of losers is $$ \sum_{v \in G} \frac{d_v}{d_v+1}.$$ To illustrate, with your example there is one vertex of degree 2 and two of degree 1, so the expected number of losers is $\frac{2}{3} + \frac{1}{2} + \frac{1}{2} = \frac{5}{3}.\ $

It is easy to prove that this quantity is maximized when the degrees of the vertices are all as close to equal as possible, so the vertex degrees all are either $d$ or $d+1$ for some $d$.


To complement the other answer: Costello, Shapira and Tetali showed that the expected approximation ration achieved by Johnson's algorithm on a random permutation of the variables is strictly better than $\frac{2}{3}$. Poloczek and Schnitger showed that another randomized version of the algorithm has expected approximation ratio $\frac{3}{4}$, and that the random permutation version does worse than $\frac{3}{4}$.

By the way do not feel bad about getting stuck on this. Proving an approximation ratio better than $\frac{1}{2}$ for this algorithm was an open problem for a while.


Binary matrix column subset selection complexity

Rephrasing as a set system, each row represents a subset $E_i$ of some set $X$, for $i=1,2,\dots,m$.  You want a set $Y \subseteq X$ with at most $k$ elements, such that $E_i \cap Y \ne \emptyset$ for each $i$.  In other words, you want a hitting set of size at most $k$; this problem is NP-complete.


Compiler Optimization: How do you automatically fuse conditionals into the loop index?

A general approach is to automatically infer loop invariants.  There are techniques for inferring loop invariants that can be expressed in Presburger arithmetic, i.e., linear expressions over the integers plus quantifiers.  These typically rely upon the fact that there exist decision procedures for Presburger arithmetic, e.g., the Omega method (see also the web site).

These methods should be enough to build a special optimization that can solve your first two challenges.  For instance, you can use those methods to find loop strides.  In particular, you can use those methods to characterize the values of i that will reach the then-block of the if-statement: you can first check whether the sequence of values of i lies in an arithmetic progression, then characterize the progression (deduce find the minimum value of i, deduce the maximum value of i, and deduce the stride).

These methods have been studied in depth in the compiler literature on loop vectorization, where we want to know whether we can execute each iteration of the loop in parallel on a separate core.  Similar techniques should be useful for your kind of problem as well.

I don't know whether there's any reasonable algorithm for your third example, or whether anyone has studied that sort of thing in the compiler literature.


Methods for proving deterministic communication complexity lower bounds

One approach that's quite different from the ones you mention is proving communication complexity lower bounds by reductions to query complexity problems. This approach can give lower bounds which are nearly quadratically stronger than the partition-based bounds, i.e. is able to actually exploit the structure of a deterministic communication protocol.

The basic idea is to compose a boolean function $f:\{0,1\}^k \to \{0,1\}$ with $k$ copies of a two party "gadget" function $g:\{0,1\}^{b} \times \{0,1\}^b \to \{0,1\}$, where $b = n/k$. It turns out that, by a simulation theorem of Raz and McKenzie, for a well-chosen $g$ and every $f$, the deterministic communication complexity of the composed function $F =f \circ g^k$ is equivalent up to lower-order factors to the deterministic decision tree complexity of $f$. The upshot is that to prove communication lower bounds it suffices to prove query lower bounds, which can be much easier.

See this paper by Göös, Pitassi, and Watson for references, and an application of this approach to giving nearly optimal separation between the partition number and deterministic communication complexity.


Type theories in which every type is inhabited are far from being useless. True enough, through the eyes of logic they are inconsistent, but there are other things in life apart from logic.

A general purpose programming language has general recursion. This allows it to populate every type, but we would not conclude from this fact that programming is a useless exercise, would we?

In the theory of programming languages types are used as a safety feature ("A well typed program does not go wrong" sad a famous man), as an organizational device, and a tool for program analysis. None of these purposes requires that there be an empty type.

Type inference is only one aspect in which type theory relates to programming languages. Some other uses of types in programming languages are:

Specification: before the programmer starts writing code he writes down the type of the program he is after. He specifies (although usually not fully) what he wants. This is also useful for communication between programmers.
Modularization: when several pieces of software need to be assembled together we have to make sure they fit. One way of doing this is to speficy the interfaces through which the pieces connect. This can be done with types.

Dependent types appear in programming languages, but in limited form (because general dependent types cannot be handled automatically by the compiler). For instance, an ML-style module is a dependent sum, while a polymorphic type can be seen as a dependent product.

You ask what is gained by studying type theory? Clarity of mind where there was only Visual Basic before. Ability to write 30000 lines of code without making it look like the Flyng Spaghetti Monster. Inner peace and feeling of superiority over the unfortunate users of Lisp.


This answer has a problem; see comments below.

Following up on my comments, here is the rest of the full answer:

First, take a look at the 2008 paper Euclidean Skeletons of Digital Image and Volume Data in Linear Time by the Integer Medial Axis Transform
 by Hesselink and Roerdink.

From my reading of your question, Section 2 of the paper is answering your question fairly explicitly. In particular, the process they use is essentially a scan across grid points.

Additionally, I wouldn't worry about the runtime being excessive. The algorithms involved are all linear time, and in fact experimental results from the paper show that the $IMA$ transform can be computed in a matter of seconds on a modern computer, even on data sets in the tens of millions. An especially nice piece of this: It appears $MB$ is computed along the way (again, Section 2), so if you simply stop the algorithm at that point, you should have an even faster runtime than "a matter of seconds" in practice.