Pointers for CS applications of logic I'm a grad student in math with a solid background in logic. I've taken a year-long graduate course in logic together with graduate courses on finite model theory and another on forcing and set theory. Most CS texts seem to assume only a very modest background in logic, which mostly covers basics of propositional logic and first-order logic.

I'd like to get some pointers on where to go for CS applications where heavier material from logic is being used. One interest of mine would be type theory and formal methods in general. Could anyone suggest some good readings past the introductory books on model checking and programming languages?

I briefly reviewed some areas here, trying to focus on ideas that would appeal to someone with a background in advanced mathematical logic.
Finite Model Theory
The simplest restriction of classical model theory from the viewpoint
of computer science is to study structures over a finite universe.
These structures occur in the form of relational databases, graphs,
and other combinatorial objects arising everywhere in computer
science. The first observation is that several fundamental theorems of
first-order model theory fail when restricted to finite models. These
include the compactness theorem, Godel's completeness theorem, and
ultraproduct constructions. Trakhtenbrot showed that unlike classical
first order logic, satisfiability over finite models is undecidable.
The fundamental tools in this area are Hanf locality, Gaifman
locality, and numerous variations on Ehrenfeucht-Fraisse games. The
topics studied include infinitary logics, logics with counting, fixed
point logics, etc. always with a focus on finite models. There is work
focusing on expressivity in finite-variable fragments of first-order
logic and these logics have characterisations via pebble-games. Another direction of enquiry is to identify properties of classical logics that survive the restriction to finite models. A recent result in that direction from Rossman shows that certain homomorphism preservation theorems still hold over finite models.

Finite Model Theory, Ebbinghaus and Flum
Elements of Finite Model Theory, Libkin
On winning strategies in Ehrenfeucht-Fraisse games, Arora
and Fagin, 1997.
Homomorphism preservation theorems, Rossman

The propositional $\mu$-calculus
A line of work from the late 60s showed that numerous properties of
programs could be expressed in extensions of propositional logic that
supported reasoning about fixed points. The modal-$\mu$ calculus is
one logic developed in this period that has found a wide range of
applications in automated formal methods. A lot of formal methods is
connected to temporal logic, or Hoare-style logics and much of this
can be viewed in terms of the $\mu$-calculus. In fact, I have heard it
said that the $\mu$-calculus is the assembly language of temporal
logics.
In his paper introducing the $\mu$-calculus, Kozen gave an
axiomatization and only proved it sound and complete for a restricted
fragment of the logic. The completeness proof was one of the great
open problems in logical computer science until Walukiewicz gave a
proof (based on infinite automata). The model theory of the
$\mu$-calculus has many rich results. Similar to van Benthem's theorem
for modal logic, Janin and Walukiewicz proved that the $\mu$-calculus
is expressively equivalent to the bisimulation invariant fragment of
monadic second order logic. The $\mu$-calculus has also been
characterised in terms of parity games and automata over infinite
trees. The satisfiability problem for this logic is EXPTIME complete
and Emerson and Jutla showed that the logic has the small model
property. Bradfield showed that the alternation hierarchy of the $\mu$-calculus is strict, while Berwanger showed that the variable hierarchy is also strict. Important classical tools used in this area are Rabin's theorem and
Martin's determinacy theorem.

Results on the propositional $\mu$-calculus, Kozen, 1983
Rudiments of $\mu$-calculus Arnold and Niwinski, 2001
Completeness of Kozen's Axiomatisation of the Propositional
$\mu$-Calculus, Walukiewicz 1995
Modal logics and $\mu$-calculi, Bradfield and Stirling, 2001
The modal mu-calculus alternation hierarchy is strict, Bradfield, 1996
The variable hierarchy of the mu-calculus is strict, Berwanger, E. Grädel, and G. Lenzi, 2005

Linear Temporal Logic
Linear temporal logic was adopted from philosophical logic into
computer science for reasoning about the behaviour of computer
programs. It was considered a good logic because it could express
properties such as invariance (absence of errors) and termination. The
proof theory of temporal logic was developed by Manna and Pnueli (and
others, later) in their articles and books. The model checking and the
satisfiability problem for LTL can both be solved in terms of automata
over infinite words.
Pnueli also proved fundamental resuls about LTL in his original paper
introducing the logic for reasoning about programs. Vardi and Wolper
gave a much simpler compilation of LTL formulae into Buchi automata.
The connection to temporal logic has led to intense study of
algorithms for efficiently deriving automata from LTL, and for
determinization and complementation of Buchi automata. Kamp's theorem
shows that LTL with since and until modalities is expressively
equivalent to monadic first-order logic with an order relation. There
is ongoing work extending these results to logics over dense linear
orders and time intervals. Etessami and Wilke developed a variation of Ehrenfeucht-Fraisse games for LTL and used them to show that the until hierarchy is strict. Another line of work is to extend LTL to express arbitrary $\omega$-regular properties. This leads to the linear-time $\mu$-calculus, a linear-time counterpart of the modal $\mu$-calculus. Unlike the modal counterpart, the linear-time alternation hierarchy collapses at level 2.

The temporal logic of programs, Pnueli 1977
From Church and Prior to PSL, Vardi, 2008
An automata-theoretic approach to linear temporal logic,
Vardi and Wolper, 1986
The Temporal Logic of Reactive and Concurrent Systems:
Specification, Manna and Pnueli
An Until hierarchy and other applications of an Ehrenfeucht-Fraïssé game for temporal logic, Etessami and Wilke, 2000

Computational-Tree Logics
Instead of a linear notion of time, the behaviour of a computer
program can be understood as a tree, leading to the notion of
computational tree logics. The simplest such logic, Computational Tree
Logic can be viewed as an alternation-free fragment of the
$\mu$-calculus. The difference between LTL and CTL led Emerson and
Halpern to develop CTL*, which allows reasoning about both properties
of states and traces.
The model checking problem for CTL over finite structures is in
polynomial time. The model checking problem for CTL* is EXPTIME
complete. The axiomatization of CTL* was a challenging open problem
that was finally resolved by Reynolds 2001. The analogue of van
Benthem's theorem for modal logic and Kamp's theorem for LTL is given
for CTL* by a theorem of Hafer and Thomas showing that CTL*
corresponds to a fragment of monadic second order logic over binary
trees. A later characterisation by Hirschfeld and Rabinovich is that
CTL* is expressively equivalent to the bisimulation-invariant fragment
of MSO with path quantification.

"Sometimes" and "not never" revisited: on
branching versus linear time temporal logic, Emerson and Halpern,
1986
On the Expressive Power of CTL, Moller, Rabinovich, 1999
Computation tree logic CTL* and path quantifiers in the monadic
theory of the binary tree, Hafer and Thomas, 1987
An Axiomatization of Full Computation Tree Logic, Reynolds,
2001

Languages of Infinite Words
The connection to LTL and the necessicity of modelling infinite
behaviour led to an intense study of $\omega$-languages, which are languages in which words are defined as functions from natural numbers to a finite alphabet. The community has studied properties of regular languages over infinite
words and developed several results analogous to the finite-word case. There are several surprises that show up, so we cannot just lift the finite-word results to the infinite-word case.
Some of my favourite results are the characterisiation of $\omega$-regular languages in terms of regular languages and analogues of the
Myhill-Nerode theorems. Staiger showed that you do not just get infinite word automata from an appropriately defined equivalence relation. This holds only for a specific sub-family of $\omega$-regular languages. Alpern and Schneider formalised the intuitive notions of safety and liveness of computer programs in terms of  prefix-closed and limit-closed sets of $\omega$-words. Moreover, using elementary topology, they showed that every linear-time property can be expressed as the intersection of a safety and a liveness property. This result has significant practical consequences because it means that rather than build complex property checkers, it suffices to build a safety and a liveness checker. A further reduction shows that it is enough to build an invariance checker and a termination checker. The safety-liveness characterisation was extended to trees by Manolios and Trefler and more recently to sets of traces, in the hyperproperties framework, by Clarkson and Schneider.

Infinite Words: Automata, Semigroups, Logic and Games, Perrin and Pin, 2004
$\omega$-Languages, Staiger, 1997
Beyond $\omega$-Regular Languages, Bojanczyk, 2010
On syntactic congruences for ω—languages, Maler and Staiger, 1993

Automata on Infinite Words
Where there are languages, computer scientists will have automata. Enter the theory of automata over infinite words and infinite trees. It is extremely sad that although automata over infinite words appeared within two years of automata on finite words, this fundamental topic is rarely covered in standard computer science curricula. Automata over infinite words and trees provide a very robust approach to prove decidability of satisfiability for a very rich family of logics.
A fundamental result is that the different acceptance criteria for
infinite word automata are all equivalent. The basic problems of
union, intersection, and complement for $\omega$-automata are more
involved than their finite word counterparts and the details differ
with the acceptance criterion used. Safra gave a famously complex determinization algorithm for Buchi automata and significant work has been devoted to deriving a new and simpler construction. Rabin famously proved that the monadic second order theory of the binary tree is decidable. His proof uses automata and the cornerstone result is the determinization of Rabin automata. I have heard tell that Rabin's theorem is the mother of all decidability results in program verification.

Decidability of Second-Order Theories and Automata on Infinite Trees, Rabin, 1969
Automata on infinite objects, Thomas, 1988
Automata: From Logics to Algorithms, Vardi, 2007

Infinite Games
Logical and infinite games are an active area of research. Games-theoretic notions show up in computer science all over the place in the duality between non-determinism and parallelism (alternation), a program and its environment, universal and existential quantification, box and diamond modalities, etc. Games turned out to be a great way to study properties of the various types of non-classical logics listed above.
As with acceptance criteria for automata, we have different winning conditions for games and many can be shown to be equivalent. Since you asked about classical results, the Borel Determinacy theorem and Gale-Stewart games often lie discreetly in the background of several game models we study. One pressing question of our times has been about the complexity of solving parity games. Jurdzinski gave a strategy-improvement algorithm and showed that deciding the winner was in the intersection of the complexity classes UP and coUP. The precise complexity of Jurdzinski's algorithm was open until Friedmann gave it an exponential-time lower bound in 2009.

Deciding the winner in parity games is in UP ∩ co-UP, Jurdzinski, 1998
Games for the μ-calculus, Niwinski and Walukiewicz, 1996
An Exponential Lower Bound for the Parity Game Strategy Improvement Algorithm as We Know it, Friedmann, 2009


Perfect matchings in a chessboard? Consider the problem of finding the maximum number of knights that can be placed on a chessboard without two of them attacking each other. The answer is 32: it's not too difficult to find a perfect matching (the graph induced by knight moves is bipartite, and there's a perfect matching for a 4 × 4 board), which is obviously a minimum edge cover. It's also not difficult to prove that the answer is $\left\lceil \frac{mn}{2} \right\rceil$ for an $m \times n$ chessboard whenever $m,n \geq 3$: it suffices to show matchings for $3 \leq m,n \leq 6$ and do a bit of induction footwork.

On the other hand, if the chessboard were toroidal and $m, n$ were even, the proof wouldn't even require showing a matching for small boards: the map $(x, y) \rightarrow (x+1, y+2)$ has only even-length cycles so there must be a perfect matching.

Is there any equivalent for rectangular chessboards, i.e. is there any simpler way to show that for sufficiently large $m, n$ there is always a perfect matching of the chessboard? For large boards, the rectangular board and the toroidal board are almost equivalent in the sense that the fraction of missing edges goes to zero, but I'm not aware of any theoretical results that would guarantee a perfect matching in that case.

What if, instead of jumping $(1, 2)$ in either direction, a knight jumped $(2, 3)$ squares in either direction? Or, for that matter, $(p, q)$ squares, with $p+q$ odd and $p, q$ coprime? If there is a simple way of proving that the answer is $\left\lceil \frac{mn}{2} \right\rceil$ for sufficiently large $m, n$ (say, $m, n \geq C(p, q)$), what does $C(p, q)$ look like?

The answer is NOT $\lceil \frac{mn}2\rceil$ for all large $m, n$ if e.g. $p=6$ and $q=3$. Why? Notice that because of the remainders $\mod 3$ now the graph is the (vertex) disjoint union of three bipartite graphs and from each we can select the bigger half. For example if $m=n=100$, then this way we can place (at least) 5002 knights. (This is because $x+y \mod 6$ has six classes which are in three pairs, the differences between the cardinalities of the pairs is $1,1,2$.)

I do not know what happens if we add the condition that $p$ and $q$ are relative primes. (Note that apart from the 2 divisor this is equivalent to $p+q$ and $p-q$ being relative primes, in fact this is the condition that we need and which also shows that $p+q$ being odd is necessary.)


Formal Definition/counter part in mathematics for “Objects” of Object Oriented Models This is a question I asked in mathematics SE forum, and I was referred here. So here is the question-

I'm a newbie in both formal mathematics and theoretical computer science, so please bear with me if you find my question is not properly framed. Object Oriented Modeling seems very useful in defining complex interactions when simulating real world. But it's mostly used in programming. I was wondering if we have a similar concept in mathematics. When we're doing programming, we can understand the concept of "Objects" and "Object Oriented Programming" and just implement it. But do we have formal definition of "Objects" in terms of Set Theory? Or for that matter, any other formal mathematical theory?

Can we implement/ formally define three primary object orient modeling concepts- 1. Encapsulation 2. Inheritance 3. Polymorphism

I know question is too broad, but would really appreciate if you can provide some pointers as well so that I can understand these concepts better.

The answer is complicated, for two reasons.

Different people in Computer Science interpret the term "object" differently.  One is that an object consists of some data and operations packaged together.  The other is that an object is all that but also has "state," i.e., it is some form of a changeable entity.
There are deep philosophical issues to do with what "change" means (and what "entity" means, as it is constantly changing), and whether mathematical descriptions actually capture changeable entities.

Object in the sense of data + operations: That is pretty standard in mathematics.  Take any group theory text book.  It will have somewhere a definition such as $h_g(x) = g x g^{-1}$.  (It is a conjugation operator.)  The $h_g$ is an "object" in this terminology.  It has some data ($g$) and an operation $x \mapsto g x g^{-1}$.  Or you can make it more object-y by taking the pair $\langle g, x \mapsto gxg^{-1}\rangle$ or the triple $\langle g, x \mapsto gxg^{-1}, x \mapsto g^{-1}xg\rangle$.  You can construct these kind of "objects" in any functional programming language that has lambda abstraction and some way to form tuples.  Abadi and Cardelli's "Theory of Objects" deals with objects of this kind extensively.

Objects with state (or objects that change): Does mathematics have such things?  I don't think so.  I haven't seen a mathematician talk about anything that changes, not in his/her professional life.  Newton used to write $x$ for the position of a particle, which is supposedly changing, and $\dot{x}$ for its rate of change.  Mathematicians eventually figured out that what Newton was talking about was a function $x(t)$ from real numbers into a vector space, and $\dot{x}$ was another such function which was the first derivative of $x(t)$ with respect to $t$.  From this, many deep-thinking mathematicians have concluded that change doesn't really exist and all you have are functions of time.  But what was changing in Newtonian mechanics wasn't the position, but the particle.  The position is its instantaneous state.  No mathematician or physicist would pretend that a particle is a mathematical idea.  It is a physical thing.

So it is with objects.  They are "physical" things, and the states are their mathematical attributes.  For a nice discussion of this aspect, see the Chapter 3 of Abelson and Sussman's Structure and Interpretation of Computer Programs.  This is a text-book at MIT and they teach it to all scientists and engineers, who I think understand "physical" things perfectly fine.

The fact that particles aren't mathematical doesn't mean that we can't deal with them mathematically.  If you ask a mathematician to model a two-particle system, he will immediately make up two functions and call them $x_1(t)$ and $x_2(t)$.  So, the two particles reduces to two meaningless indices (1 and 2).  This is the mathematician's way of saying we don't know what those particles are and we don't care.  All we need to know is that their positions evolve independently (or separately).  So, we will model them by two separate functions.

Similarly the standard mathematical way to model object-oriented programs is to treat each object as an index into the state space.  The only difference is that since objects come and go, and the structure of the system is dynamic, we need to extend it to a "possible world" model where each world is basically a collection of indices.  Allocation and deallocation of objects would involve moving from one world to another.

There is a problem though.  Unlike in mechanics, we want the state of our objects to be encapsulated.  But the mathematical descriptions of objects put states all over the place, completely destroying encapsulation.  There is a mathematical trick called "relational parametricity" which can be used to cut things back to size.  I won't go into it now, except to emphasize that it is a mathematical trick, not a very conceptual explanation of encapsulation.  A second way of modelling objects mathematically, with encapsulation, is to finesse the states and describe the object behaviour in terms of observable events.  For a good discussion of both of these models, I can refer you to my paper titled Objects and classes in Algol-like Languages.

[Note added:]

A nice analysis of the mathematical underpinnings of objects can be found in William Cook's article "On Understanding Data Abstraction, Revisited".


Naive definition of treewidth Treewidth has arguably pretty involved definition. Recently I was thinking about a problem and turns out it easy to solve it for graphs with small ``naive treewidth''.

Naive treewidth is defined as follows. Let $G=(V,E)$ be a graph. We say that $G$ has naive treewidth $k$ if there exists a partition $V_1 \sqcup V_2 \sqcup \ldots \sqcup V_m = V$ such that $|V_i| \le k$ and a tree $T = ([m], E_T)$ such that for every $(u,v) \in E$ either $u,v \in V_i$ for some $i \in [m]$ or $(u,v) \in V_i \times V_j$ such that $(i,j) \in E_T$.

If $T$ is a path than we say that $G$ has naive pathwidth $k$.

For naive pathwidth it is easy to see that it can be much larger than pathwidth. Consider a full binary tree with $2^k$ leaves. It has pathwidth $k-1$. On the other hand notice that if naive pathwidth of a graph is $\le t$ than the partition contains at least ${|V| \over t}$ blocks. Thus there exists a path in $G$ of length at least ${|V| \over t} - 1$. Since the longer path in the full binary tree of height $k$ is $2k$, naive pathwidth of the full binary tree is at least ${2^k \over 2k}$.

Notice that instead of the full binary tree it was possible to use a tree with one vertex connected to the remaining $|V|-1$ vertices which gives even better separation. The reason I've used the binary tree is that for my purposes all graphs have constant degree.

My questions are:

For a graph with small pathwidth (and constant degree if it is needed) can it be shown that it has small naive treewidth? If it is not true, how the counterexample looks like?
The same question for a graph with small treewidth.

Update: for arbitrary degrees there is a separation between treewidth and naive treewidth. The example is a path of length $n$ and a vertex connected to all vertices of the path. Treewidth of such graph is $2$ and naive treewidth is $\Omega(\sqrt{n})$. The proof goes like this: consider the block $B$ containing the vertex of degree $n$. Assume that this block contains at most $\sqrt{n} / 2$ vertices. Then there exists a path in $G - B$ containing at least $2 \sqrt{n}$. Notice that in $T$ all the blocks should be connected to $B$. Thus this path of length $2 \sqrt{n}$ must be contained in a single block.

Your parameter "naive treewidth" is known as tree-partition-width in the literature.
It is known that if a graph has constant treewidth and constant maximum degree, then it has constant tree-partition-width. See [Wood 2009].

Note that your example in the update actually has pathwidth 2.

[Wood 2009] David R. Wood. On tree-partition-width. European Journal of Combinatorics 30 (2009) 1245-1253. https://doi.org/10.1016/j.ejc.2008.11.010
(also on arXiv https://arxiv.org/abs/math/0602507)


Was Babbage's Analytical Engine really turing-complete? According to literature, Babbage's Analytical Engine is turing-complete because it supports conditional branching: it can perform different operations depending on the sign of the result last operation using a conditional arm (see http://web.archive.org/web/20100426034840/http://halfbakedmaker.org/2009/12/26/rod-logic-alu-2/).

However, the instruction set as devised by Babbage seems to support only going back or jumping ahead one single punched card. (see http://www.fourmilab.ch/babbage/cards.html, "Combinaritorial Cards")
Surely this is computationally less mighty than supporting a goto-statement for jumping to arbitrary statements?

If any two turing machines can emulate each other, how can the goto-behaviour be emulated using the conditional jumping of just one instruction?

Your question states:

  However, the instruction set as devised by Babbage seems to support only going back or jumping ahead one single punched card.

However, the link you supply as a reference for that says

  The number starting in column 4 indicates how many cards are to be advanced past or backed up past the reader.

This would seem to render your question moot.


What are some techniques for "balancing" a tree beside heavy-light and centroid decomposition? The only techniques i know are those in the title.

The paper "Algorithmic Meta Theorems for Circuit Classes of Constant and Logarithmic Depth" (Elberfeld, Jacobi, Tantau) gives a nice balanced tree decomposition based on tree contraction in $TC^0$:

https://eccc.weizmann.ac.il/report/2011/128/

Another nice $TC^0$-decomposition is based on so-called TSLPs in the paper "A Universal Tree Balancing Theorem" (Ganardi, Lohrey):

https://arxiv.org/pdf/1704.08705.pdf


equivalent way(s) of expressing P=?NP problem in linear programming? the paper "In defense of the Simplex Algorithm's worst-case behavior" Disser/Skutella [1] was recently cited on this tcs.se site by saeed on another interesting question. the paper introduces the idea of "NP mighty" algorithms (p3 def2). it follows a fruitful/continuing line of research analyzing P$\stackrel{?}{=}$NP wrt the simplex algorithm and linear programming of which there have been other major recent advances, eg results by Pokutta et al in [2] showing that the P-time TSP polytope must have an "unlikely/restrictive" form (commentaries in Barriers to P/NP proofs, RJLipton, also Stating P$\stackrel{?}{=}$NP without TMs). question (possibly with multiple leading answers):

  the Disser/Skutella paper has closely related ideas but does not seem to explicitly reformulate the P$\stackrel{?}{=}$NP question. what is an equivalent way to state/study it in their introduced schema/framework of "NP Mighty" algorithms? what is a/the basic open problem in simplex/linear programming complexity theory that is equivalent to P$\stackrel{?}{=}$NP?

(somewhat related question: the Disser/Skutella paper also refers to Klee-Minty cubes, long used to show worst-case behavior on the simplex algorithm. are there any results relating lower bounds on them to general algorithmic lower bounds and/or complexity class separations eg P$\stackrel{?}{=}$NP etc?)

[1] "In defense of the Simplex Algorithm's worst-case behavior" Dissker/Skutella
[2] Exponential Lower Bounds for Polytopes in Combinatorial Optimization Fiorini et al

This answer is for your "somewhat related question":

In the following recent paper, Klee-Minty cubes were used explicitly to show that  there exists a pivoting rule for the simplex method (not one of the standard ones, like Dantzig's pivoting rule analysed by Disser and Skutella) for which it is PSPACE-complete to decide whether a variable enters the basis for the simplex method with this pivoting rule. It was left open (Conjecture 3 in the paper) whether the same result holds for Dantzig's pivot rule.

I. Adler, C. Papadimitriou, and A. Rubinstein (2014).
On Simplex Pivoting Rules and Complexity Theory.
In Proc. of IPCO, pp. 13-24.

In the following paper we prove that conjecture and strengthen Disser and Skutella's result to show two PSPACE-completeness results for the simplex method with Dantzig's pivoting rule (one for whether a variable enters the basis "along the way" and another for whether a variable is in the final solution found by Dantzig's pivot rule).

J. Fearnley and R. Savani (2015).
The Complexity of the Simplex Method. In Proc. of STOC, pp. 201-208.
http://arxiv.org/abs/1404.0605

We use the known connection between linear programs and Markov decision processes (MDPs). A central part of our construction are the exponential-time examples due to Condon and Melekopoglou for single-switch policy iteration for MDPs. Those examples use a reflected binary Gray code, as used for Klee-Minty cubes. We use a modification of those examples as a clock to drive iterated circuit evaluation in our construction.


Multi-armed bandit problems where more than one arm can be selected? I want to know if there are any references in the literature on  multi-armed bandit problem where in one round, you can select $k > 1$ arms.

Yes - Satyen Kale, Rob Schapire, and I have a recent paper (NIPS '10) on this very problem, where we consider choosing "slates" of arms instead of individual arms.  We consider the cases when position matters in the slate and when it doesn't.  We also analyze both the experts MAB "contextual" model and the expertless setting.


Squared Hellinger distance between Binomial(n,p) and Binomial(n+1,p) I came across a claim in a paper Trace reconstruction revisited (in Lemma 11), which is basically that the squared Hellinger distance between Binomial$(n,p)$ and Binomial$(n+1,p)$ grows as $O(1/n)$. $p$ is a small positive number less than $\frac{1}{2}$.

I've been trying to prove it but have not been able to see this. Is there an easy way to see this?


Contradiction between Gödel's Second Incompleteness Theorem and the Church-Rosser's property of CIC? On one hand, Gödel's Second Incompleteness Theorem states that any consistent formal theory that is strong enough to express any basic arithmetical statements can't prove its own consistency. On the other hand, the Church-Rosser's property of a formal (rewriting) system tells us that it is consistent, in the sense that not all equations are derivable, for example, K$\neq$I, since they don't have the same normal form.

Then the Calculus of Inductive Constructions (CIC) clearly statisfies both conditions. It is strong enough to represent arithmetical propositions (indeed, the $\lambda\beta\eta$-calculus alone is already able to encode the Church numerals and represent all primitive recursive functions). Moreover, CIC also has the confluence or Church-Rosser property. But:

  shouldn't CIC be unable to prove its own consistency by the Second Incompleteness theorem?

Or it just states that the CIC can't prove its own consistency inside the system, and somehow the confluence property is a meta-theorem? Or maybe the confluence property of CIC does not guarantee its consistency?

I would highly appreciate  if someone could shed some light on those issues!

Thanks!

First, you are confusing consistency of CIC as an equational theory with consistency of CIC as a logical theory. The first means that not all terms of CIC (of the same type) are $\beta\eta$-equivalent. The second means that the type $\bot$ is not inhabited. CR implies the first kind of consistency, not the second.  This, as has been pointed out in the comments, is implied instead by (weak) normalization. The prototypical example of this situation is the pure $\lambda$-calculus: it is equationally consistent (CR holds) but, if you consider it as a logical system (as Alonzo Church orginally intended) it is inconsistent (indeed, it does not normalize).

Second, as Emil pointed out, even if CIC has a given property (CR or normalization) it is perfectly possible that CIC cannot itself prove that property. In this case, I do not see any inconsistency in the fact that CIC is able to prove its own CR property, and I guess that this is indeed the case (elementary combinatorial arguments usually suffice for CR, and such arguments definitely fall within the huge logical power of CIC).  However, CIC certainly does not prove its own normalization property, precisely because of the second incompleteness theorem.


Finding a graph that minimizes the number of nodes for a given number of paths There is a problem that is of great interest for communications and optics, but I do not know if there is an easy solution of it. We are looking for an oriented graph that goes from a node A (starting point) to a node B (ending point) that has a fixed number N different paths from A to B. Intermediate nodes that can only split or recombine two edges (so two input and two output nodes). What are the graphs that minimize the number of nodes met in all the N paths.

If I understand the problem properly, the answer should be $2 \log_2(n)$: make a graph with $\log_2(n) + 2$ layers, where the first layer is just $A$, the last layer is just $B$, and the intermediate layers have $2$ nodes each; we then put a directed edge from each node to the node(s) in the next layer.  We then have $2^{\log_2(n)} = n$ paths from $A$ to $B$, and the union of these paths contains $2 \log_2(n)$ intermediate nodes.

Does this fit the constraints of your problem?


Algorithmic advantages of pathwidth over treewidth Treewidth plays an important role in FPT algorithms, in part because many problems are FPT parameterized by treewidth. A related, more restricted, notion is that of pathwidth. If a graph has pathwidth $k$, it also has treewidth at most $k$, while in the converse direction, treewidth $k$ only implies pathwidth at most $k\log n$ and this is tight.

Given the above, one may expect that there may be a significant algorithmic advantage to graphs of bounded pathwidth. However, it seems that most problems which are FPT for one parameter are FPT for the other. I'm curious to know of any counter-examples to this, that is, problems which are "easy" for pathwidth but "hard" for treewidth.

Let me mention that I was motivated to ask this question by running into a recent paper by Igor Razgon ("On OBDDs for CNFs of bounded treewidth", KR'14) which gave an example of a problem with a $2^{k}n$ solution when $k$ is the pathwidth and a (roughly) $n^k$ lower bound when $k$ is the treewidth. I am wondering if there exist other specimens with this behavior.

Summary: Are there any examples of natural problems which are W-hard parameterized by treewidth but FPT parameterized by pathwidth? More broadly, are there examples of problems whose complexity is known/believed to be much better when parameterized by pathwidth instead of treewidth?

It is shown that [1] the Mixed Chinese Postman Problem (MCPP) parameterized by pathwidth is $W[1]$-hard, even if all edges and arcs of the input graph $G$ have weight $1$ and is FPT with respect to treedepth. This is the first problem are aware of that has been shown to be $W[1]$-hard with respect to treewidth but FPT with respect to treedepth. Note that the pathwidth of a graph lies between its treewidth and treedepth.

The Steiner Multicut problem, which asks, given an undirected graph $G$, a collection $T = \{T_1, . . . , T_t\}$, $T_i ⊆ V(G)$, of terminal sets of size at most $p$, and an integer $k$, whether there is a set $S$ of at most $k$ edges or nodes such that of each set $T_i$ at least one pair of terminals is in different connected components of $G \ S$.

Node Steiner Multicut, Edge Steiner Multicut, and Restr. Node Steiner Multicut are $W[1]$-hard for the parameter $k$, even if $p = 3$ and $tw(G) = 2$ [2].

[1] https://core.ac.uk/download/pdf/77298274.pdf

[2] http://drops.dagstuhl.de/opus/volltexte/2015/4911/pdf/11.pdf


Best Hamiltonian Cycle Problem solver What is the best Hamiltonian Cycle Problem (HCP) solvers available in the market?
Googling so far shows that there is one created by Flinders University that can solve at most 5000 node instances.

I know HCP is a NP-hard problem but is 5000 node the best that researchers can produce so far?  Is no researcher / commercial entity interested in producing a better one (maybe solve 50000 node instances?) because a HCP is non-monetizable unless it can solve billions node instances (crack RSA and what nots)?

I found myself having to find a Hamilton path in a graph of 200 vertices (what you called "nodes"). My first idea was to use the Hamilton path solver in Maxima ( http://maxima.sourceforge.net/docs/manual/de/maxima_50.html#IDX2257 ), but it wasn't able to solve it. Luckily, a few years ago, I used to use SAT solvers to solve difficult logic grid puzzles (because I had a friend who kept on sending them to me!), so wrote a program to write a SAT model for the graph. To my delight, when I fed the model to an open source SAT solver (MiniSat), it was able to resolve it in less than 10 minutes (I didn't time it I'm afraid - I started it, and it had finished when I came back).

Disclaimer: I am not a "theoretical computer scientist", nor even somebody who has ever done a Hamilton cycle before - I landed here after a Google search and thought I'd share what I did over the weekend. However, for a beginner, beating the mathematicians who wrote the Graphs package in Maxima isn't bad - and suggests that if you need to find a Hamilton path (or cycle) in a large graph, building a SAT model is an approach worth considering.


References to learn more about graph laplacian. I have vaguely heard of this connection between random matrix theory and graphs (the spectral gap of their laplacians) on compact Riemann surfaces.

Can someone give a pedagogic reference which helps learn this subject?
Also is there something called "free probability theory" which is somehow equivalent to random matrix theory?
Would you call the usual QFT of Hermitian matrices a random matrix theory?

Suggest these free available resources. Most textbooks on graph theory only glance at "free probability theory".

Lectures on the Combinatorics of Free Probability (London Mathematical Society Lecture Note Series):
http://www.amazon.com/Lectures-Combinatorics-Probability-Mathematical-Society/dp/0521858526

Speicher lectures: http://www.mast.queensu.ca/~speicher/papers/lectures-IHP.pdf


What's the expressive/compressive power of strongly normalizing subset of untyped lambda calculus? Let $\Lambda$ be a set of strongly normalizing lambda terms.
Let $\mathtt{NF} : \Lambda \rightarrow \Lambda$ be evaluation to the normal form.
Let $ \lvert x\rvert : \Lambda \rightarrow \mathbb{N}$ be
size of a term in number of symbols.
The following function seems to be well defined:

$$f_\Lambda:\mathbb{N} \rightarrow \mathbb{N}$$
$$ f_\Lambda(n) = \max_{t \in \Lambda, \lvert t \rvert \leq n} \lvert\mathtt{NF}(t)\rvert $$

What is the rate of growth of $f_\Lambda$?

Can we define some lower and upper bound in fast growing hierarchy?

The maximal blowup in termsize of simply typed lambda calculus is non-elementary (2 ↑↑ O(n) see e.g. [1] page 72). This is not exactly what you are asking for, but since typed lambda calculus is a strongly normalizing subset of untyped lambda calculus, it should give you some lower bounds.

I am not sure if the general question can be answered. Untyped lambda calculus is Turing-complete, the strongly normalizing fragment is then equivalent to the set of terminating programs. Since membership in this set is already undecidable, I would not expect that an upper bound on the size of normal forms can be shown.

[1] Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier Science Inc., New York, NY, USA, 2006.


Understanding performance of QFBV SMT solvers SMT solvers such as Z3 or Boolector use a complex set of heuristics to solve problems. However, this also makes predicting the performance of such a solver for a given problem very hard. My question is thus:

Question

Is there a way to understand or gain insights into the performance of a SMT solver for a specific in the theory of quantifier-free bitvectors (QFBV)?

This also includes any visualization tools that would help to understand where the solver is "stuck" / does not make progress.

Applications

Understand in advance how different encodings of the same problem affect solver performance (the state of the art here can't be "just try a few different encodings and hope one is fast enough", right?)
If a given problem is not solveable by an SMT solver due to time constraints, find a way to express the problem differently so that it can be solved.
Avoid wasting time on domain-specific problem simplifications that won't affect solver performance at all or even negatively affect solver performance.

Existing research

I tried to find research on this topic, but I have not been able to find much. I do not have much experience in the field of SAT/SMT solvers yet, so apologies if I have missed something.

SATzilla: predicts best performing solver based on features extracted from the problem using machine-learning techniques.

This applies only with SAT instead of SMT, and does not explain the reasons for solvers performance.
Z3 axiom profiler A visualization of Z3 instantiation graph and analysis of matching loops

Looks like this focuses only on the quantified theories.

The short answer is no, we don't understand it.  The long answer is yes, we have some bounds, but those bounds aren't very helpful.  It's quite clear that the worst-case running time is exponential.  That's not very helpful, because we know that in some/many practical situations, it seems to run fairly rapidly -- and we don't really know why.

We don't know why that is true for SAT solvers, let alone for QFBV.  Understanding why QFBV solvers are often fast seems at least as hard as understanding why SAT solvers are often fast, which is already beyond our current level of understanding.  If you search more on this site you can find a summary of current attempts to understand the latter topic.


Algorithm to find $n$ player nash equilibrium This is the question asked 10 years before.
Most of the algorithm and software mentioned are out of date. I am wondering is there new approchs for this problem in the last 10 years?
The game dealing with is $n$ player, finite actions, general sum.

The problem of computing Nash equilibria in general games is PPAD complete (which is believed to be hard), even for 2-player games. This was proven for 3-player games by Daskalakis et al. for 3-player games in this paper and extended to 2-player games by Chen et al. in this paper. See the Wikipedia article on the PPAD class for more details.
There are nonetheless many approaches to finding equilibria if you have further game structure, from convexity of the payoff functions to potential and zero-sum games.
Having said that, even finding local min-max equilibria in two-player zero-sum games with nonconvex-nonconcave objectives was recently proven to be PPAD complete (as hard as finding Nash equilibria in general games) by Daskalakis et al., see this video link.


Dual Barnette's Conjecture Is every Eulerian triangulated (planar) graph Hamiltonian?

On the other hand we have that:

  Barnette's Conjecture (Open): Every cubic bipartite (3-connected) planar graph is Hamiltonian.

Notice that: Eulerian triangulated planar graphs and cubic bipartite planar graphs are mutual duals.

I would be happy to know of a proof or a counterexample (I have not been able to find either). In the absence of both is this a well known conjecture?

Some additional facts (possibly relevant):

Every Eulerian triangulated planar graph is $3$-colorable (see this).
(Whitney's Theorem) Every $4$-connected triangulated planar graph is Hamiltonian.

Definitions:

Hamiltonian Graph: Undirected Graph with a simple cycle through every vertex.
Eulerian Graph: Connected graph with all degrees even.
Triangulated (planar) Graph: Planar graph with every face a triangle.
Cubic Graph: Graph with every vertex having degree exactly $3$.

Edit: (Thanks@domotorp) Triangulated planar graphs are not necessarily Hamiltonian (e.g. see this)

Maybe I am mistaken but I think it is possible to make the example from https://math.stackexchange.com/a/78835/131224 Eulerian. Just take an octahedron and place 3 new vertices on each of its faces, connected to each other and also to two of the vertices of the face in a circular order. So if the face was $abc$, then add $def$ and connect $d$ to all but $a$, $e$ to all but $b$ and $f$ to all but $c$. The same reasoning works but now every degree is even.


Which algorithms have been proposed to learn the architecture of a deep neural network? Yoshua Benhgio's Learning Deep Architectures for AI book mentions that

  we should [...] strive to develop learning algorithms that use the data to determine the depth of the ﬁnal architecture.

Would anyone know of any algorithms proposed thus far to achieve this?

So far I have come across:

The tiling algorithm for building a feed-forward network to learn a Boolean function. It adds layers as well as units, but Boolean functions aren't too relevant for applied problems.

This predates the start of the "deep learning craze" in the mid-2000s, but for me the cascade correlation algorithm (Fahlman & Lebiere, 1989; pdf) is the build-your-own-topology NN algorithm. I am not sure how popular the algorithm is in ML now-a-days, but it is still popular in cognitive science despite it's unrealistic grounding in biology. If you want intersections with genetic algorithms (like the one @vzn points out with more recent examples) then that has been done with CC as well (Potter, 1992; pdf).

You might also find the following questions on other SEs to be of interest:

Why do neural networks seem to perform better with restrictions placed on their topology?
Dynamically adjusting NN architecture: inventing the unnecessary? (also on MetaOptimize)


Theories which characterize classes of computational complexity When reading the paper "An applicative theory for FPH" you can encounter the following passage:

Considering theories which characterize classes of computational complexity, there are three different approaches:

in one, the functions which can be defined within the theory are “automatically” within a certain complexity class. In such an account, the syntax has to be restricted to guarantee that one stays in the appropriate class. This results, in general, in the problem that certain definitions of functions do not work any longer, even if the function is in the complexity class under consideration.
In a second account, the underlying logic is restricted.
In the third account, one does not restrict the syntax, allowing, in general, to write down “function terms” for arbitrary (partial recursive) functions, nor the logic, but only for those function terms which belong to the complexity class under consideration, one can prove that they have a certain characteristic property, usually, the property that they are “provably total”. While the function terms, according to the underlying syntactical framework, may
have a straightforward computational character, i.e., as $\lambda$ terms, the logic which is used to prove the characteristic property may well be classical.

My question concerns references which can be as an introduction to the three above-mentioned approaches. In this passage we see just characterizations for approaches, but do these have any generally accepted names?

I think the first approach, the bounded arithmetic approach, is the most popular and well-studied approach. The name bounded arithmetic indicates the use of weak subsystems of Peano arithmetics, where  induction is restricted to formulas with bounded quantifiers.  I already summarized the main idea behind this approach in this post. An excellent recent reference on bounded arithmetic is the book by Cook and Nguyen, whose draft is freely available.

The second approach uses linear logic and its subsystem as mentioned by Kaveh, which I don't know much about.

I haven't heard of the third approach although I'm working on bounded arithmetic. But it sounds a bit strange to me since without some form of syntactic or logical restriction, how does then a theory characterize a complexity class?


Proof software for Primitive Recursive Arithmetic Primitive Recursive Arithmetic is a critical foundational system in mathematics at large, and all the more so in areas studying constructive reasoning and/or computability such as Theoretical Computer Science.

Is there any proof software that deals with Primitive Recursive Arithmetic... or equivalent systems?

The ACL2 theorem prover seems quite close to what you want, though it is hard to know exactly what the strength of the system is.

From the logical description here it looks like the base is a quantifier-free equational logic with induction principles, which include principles allowing the definition of PR functions.

This gives exactly PRA, but in addition, the standard library defines induction up to $\varepsilon_0$, which brings the strength up to full Peano Arithmetic.

You might therefore want to work in ACL2 with a restricted version of the standard induction principle (I don't know how hard that is).


Independent set size in triangle-free graphs Consider a triangle-free graph $G$. The notations used are:

$\alpha(G) = $ the size of a largest independent set of $G$.
$n(G) = $ the number of vertices in $G$.

Theorem (Ajtai et al.): For a triangle-free graph $G$ with maximum degree $\Delta$,

$$\alpha(G) \geq \frac{n(G)}{8\Delta}\log_2\Delta.$$

The book "Probabilistic Methods" by Alon-Spencer gives a very cute proof in the section "The Probabilistic Lens", (pg 272).

But the theorem is true even when $\Delta$ is subsituted by the average degree $d_{avg}$ in the above expression and Bollobas proves this in his book "Random Graphs, 2nd edition", pg 332, using completely different techniques.

My Question : Can we obtain Bollobas' result by tweaking the technique used by Alon-Spencer?

PS: For a graph theory enthusiasts, both proofs are worth reading!

Thanks in advance!

If you don't care about the constants, then the answer is 'yes' by an easy reduction:

Take a triangle-free graph $G$ with average degree $d_{avg}$. Create a new graph $G'$ which is obtained from $G$ by deleting all vertices with degree $\ge 2d_{avg}$. Obviously, any independent set in $G'$ is an independent set in $G$, and $G'$ is triangle-free. Also, the number of vertices in $G'$ is at least $n(G)/2$. Now we can apply the Alon--Spencer proof.


What do these lower bounds really mean? I was reading an abstract for a paper that gives a minimum number M of good agents that guarantees f-Byzantine gathering, if there are f Byzantine agents. It gives a lower bound of f+1 for strongly byzantine agents. It also says that:

"...we give deterministic gathering algorithms for at least 2f+1 good agents when the size of the network is known...".

There are two lower bounds to the number of good agents. What do those two lower bounds mean? If it was only one lower bound, it would have been clear.

The abstract is: Gathering Despite Mischief

Note that the paper considers strongly Byzantine agents and weakly Byzantine agents.
From the abstract:

  For weakly Byzantine agents, we show that any number of good agents permits solving the problem for networks of known size. If the size is unknown, then this minimum number is f+2. More precisely, we show a deterministic polynomial algorithm that gathers all good agents in an arbitrary network, provided that there are at least f+2 of them. We also provide a matching lower bound: we prove that if the number of good agents is at most f+1, then they are not able to gather deterministically with termination in some networks.

So for $f$ weakly Byzantine agents any number of good agents will do if the network size is known. Alternatively if it is not known, $\ge f+2$ good agents is a lower bound and they also show the matching upper bound.

  For strongly Byzantine agents, we give a lower bound of f+1, even when the graph is known: we show that f good agents cannot gather deterministically in the presence of f Byzantine agents even in a ring of known size. On the positive side, we give deterministic gathering algorithms for at least 2f+1 good agents when the size of the network is known and for at least 4f+2 good agents when it is unknown.

In the strongly Byzantine case, they show that $f+1$ is a lower bound on the number of good agents required when the network size is known, which implies that this is true when the network size is unknown. These lower bounds aren't tight it seems as their best algorithms require $\ge 2f+1$ good agents in the case where the network size is known, or $\ge 4f+2$ good agents if the network size is unknown.


Parallel algorithms to color interval graphs Several NP-hard graph problems get easy if we consider interval graphs. There is a greedy algorithm to color optimally an interval graph. Just sort the intervals according their left endpoints and color each interval with the last freed color.

Every coloring algorithm especially every efficient parallel algorithm I see, use the endpoints of intervals to get an optimal coloring. With "efficient parallel" I mean that the problem is in the complexity class NC.

There is a possibility to use only the structure of the graph to color the interval graph but this uses a maximum matching in a bipartite graph which isn't known to be in NC.

Is there any efficient parallel algorithm that doesn't use the endpoints of the intervals and just uses the structure of the graph to color an interval graph?

I'm not really familiar with the topic, but with some searching there are some results.

For example, Efficient parallel algorithms on interval graphs by Das and Chen, and A simple optimal parallel algorithm for the minimum coloring problem on interval graphs by Yu and Yang both gave an algorithm with $O(\log n)$ time and $O(n)$ processors on the EREW PRAM model. Even for the chordal graphs (which is a superclass of the interval graphs) there is an algorithm with $O(\log^2 n)$ time and $O(n)$ processors on the CRCW PRAM model, in the paper Efficient parallel algorithms for chordal graphs by Klein. Maybe you can take a look at the papers and references, to make sure if there are any additional assumptions, like whether the interval representations are given or not.


What is the name of a function $f$ such that $f(x,y) \in L \iff x\in L \wedge y \in L$? Let $L$ be a language and $f\colon {\Sigma^\star}\times\Sigma^\star\to\Sigma^\star$ a function on two parameters with the property that for all $x$ and $y$, $f$ returns an element of $L$ if and only if both $x$ and $y$ are elements of $L$:

$$f(x,y)\in L \iff x\in L\wedge y\in L .$$

Question Do such functions have a name in the literature?

Following are some amusing observations. These functions, which I will call "conjunctive reductions", can be constructed for the complete problems of a variety of complexity classes. For example, for $L=SAT$, take the function $f(\psi, \phi)=\psi\wedge\phi$. Analogously, we may consider "disjunctive reductions", so that $g(\psi,\phi)=\psi\vee\phi$ is a disjunctive reduction over $SAT$. These two reductions work fine over quantified boolean formulas too, so they also work for all levels of the polynomial hierarchy and for PSPACE.

It is easy to construct both conjunctive and disjunctive reductions for the L and NL-Complete languages DSTCON and USTCON: Given two graphs, $G, H$ and two pairs of vertices, $(u,v), (x,y)$, construct a new graph by taking the disjoint union $G\cup H$, add two nodes $s,t$ and add edges $(s,u),(v,x),(y,t)$. A disjunctive reduction puts these two graphs in parallel, rather than in series.

A conjunctive reduction exists for Graph Isomorphism, but no disjunctive reduction obviously exists. Conversely, a disjunctive reduction exists for the Nontrivial Graph Automorphism problem, but I could not find a conjunctive reduction. This surprised me, because I thought these problems were on some level the same, and then I had learned something new about graph isomorphism!

As an obvious last step, one may consider "conjugate reductions", functions such that $f(x)\in L \iff x \not\in L$. Finding such a reduction for Graph Isomorphism would show that it is in coNP. I could find neither a conjunctive, nor a disjunctive, nor a conjugate reduction for the decision version of Factoring.

They are typically called AND-functions. (I'm not joking.) Indeed, this concept has been considered before, and that's what people call them. See, for example, the book by Kobler, Schoning, and Toran on Graph Iso, where they talk about AND- and OR-functions for GI. And, by the way, there is an OR-function for GI (ibid.).

The question of an AND-function for graph automorphism is, I believe, still open :) (as stated in the book above).

Based on your last paragraph, the type of reduction you are talking about can also be generalized to what are called "truth-table" or "tt" reductions. These are non-adaptive Turing reductions (the queries are fixed by the input, but cannot depend on the answer to previous queries). For example, the negation kind of reduction in your last paragraph is a 1-tt reduction (1=number of queries).


What are the classic papers from the recursion theoretic area of complexity theory? Two papers I would include are:

D. Kozen, "Indexing of subrecursive classes", STOC, 1978.
R. Ladner, "On the Structure of Polynomial Time Reducibility", JACM, 1975.

Hajek, P. Arithmetical hierarchy and complexity of computation. Theoret. Comp. Sci. 8 (2): 227-237, 1979.  Started the study of the complexities of index sets (where their "complexities" often lie somewhere in the arithmetical hierarchy; see this answer to another question.)

On the study of polynomial-time degrees (buzzword="polynomial-time degree theory", for the sake of future searches) I'd say these papers are of interest (several of them are based on Ladner's technique):

Homer, S. Minimal degrees for polynomial reducibilities.  J. ACM 34(2):480-491, 1987.
Schöning, U. Minimal pairs for P. Theoret. Comp. Sci. 31: 41-48, 1984.
Downey, R. Nondiamond theorems for polynomial time reducibility. Journal of Computer and System Sciences 45(3):385-195, 1992.
Downey, R. and Fortnow, L. Uniformly hard languages. Theoret. Comp. Sci. 298(2): 303-315, 2003.
Fenner, S., Homer, S., Prium, R. and Schaefer, M. Hyper-polynomial hierarchies and the polynomial jump. Theoret. Comp. Sci. 262: 241-256, 2001.

Probably a forward and backwards reference search will find several more papers in the same area (though it's not that big an area!).


Approximate-#SAT solver I am looking for a solver that computes an approximation to #SAT.  In other words, given a formula $\phi(x)$ in CNF, approximately count the number of satisfying assignments to $\phi$.  I'm interested in an approximate count, not the exact number.  Are there any existing working implementations that I can download and try?

To be clear, I'm not looking for algorithms or for papers describing algorithms; I'm looking for an implementation I can use, in the style of a SAT solver.  This question is related to #SAT Solver download, except that one asks for solvers that exactly count the number of satisfying assignments, whereas I am interested in solvers that approximate the number of satisfying assignments (I do not need an exact count).

Ashish Sabharwal lists some software (e.g., SampleCount, ApproxCount, and more) for this on his web page.  I haven't tried any of these.


Reference on cryptography methods I'm looking for a good reference, possibly a survey, on the different types of cryptography methods. As far as I understand, the security of a cryptographic method depends on some hardness assumptions, and I've heard of methods based on the hardness of factorization, discrete logarithm, NP-complete problems (such as the Knapsack problem) and problems on lattices.

Is there any good text addressing the different existing paradigms?

In particular, I would be interested on open problems and questions on less studied methods.

Answers for this question may include both references to a text giving an overview of the area but also to specific methods.

A good start would be Katz and Lindell's Introduction to Modern Cryptography.

Alternatively, you might want to take one of the crypto courses on Coursera: I recommend the ones taught by Jonathan Katz and by Dan Boneh (search for "cryptography" on Coursera). They are both free.


Best method of Error Correction in Quantum Key Distribution As far as I can tell, almost all implementations of QKD use Brassard and Salvail's CASCADE algorithm for error correction. Is this really the best known method of correcting errors in a shared sequence of random qubits, or is there a better proposition that implementations of QKD should be using instead?

Actually, there is a lot going on in the research of better and faster error correction codes for QKD. The biggest bottleneck of the CASCADE protocol is that it requires a lot of classical communication between Alice and Bob.

A lot of work has been done on LDPC codes. You can have a look to the following papers:

-Efficient reconciliation protocol for discrete-variable quantum key distribution (arXiv:0901.2140v1)

-Rate Compatible Protocol for Information Reconciliation: An application to QKD (arXiv:1006.2660v1).

Moreover, I suggest to look at the slides at https://sqt.ait.ac.at/software/projects/hipanq/wiki/Schedule where there are many talks about error correction in QKD.

Finally, regarding the applications, I would like to point out that the demostration that has been done in Tokyo was also implemented using LDPC codes (see arXiv:1103.3566v1 on page 13 for a reference).


Sparsification Lemma for k-SAT and Exponential Time Hypothesis According to R. Impagliazzo, R. Paturi and F. Zane, 2001 an instance of $k$-SAT is called sparse if $m = O(n)$ where $m$ denotes the number of clauses and $n$ the number of variables. The Sparsifiction Lemma, as mentioned in R. Impagliazzo, R. Paturi, 2001 says:

  [...] that an arbitrary $k$-CNF can be expressed (in subexponential time) as the disjunction of a subexponential number of linear size $k$-CNFs. More precisely [...]

  For all $\varepsilon > 0$, $k$-CNF $F$ can be written as the disjunction of at most $2^{\varepsilon n}$ $k$-CNF $F_i$ such that $F_i$ contains each variable in at most $c(k,\varepsilon)$ clauses for some function $c$. Moreover, this reduction takes at most $poly(n) 2^{\varepsilon n}$ time.

In the above reduction, each $k$-CNF $F_i$ has at most $c(k,\varepsilon)n$ many clauses, hence is sparse in the above sense. According to this talk, the Exponential Time Hypothesis (ETH) says:

  $3$-SAT instances (with $n$ variables and $m$ clauses) cannot be solved in time $O(poly(n) 2^{o(n)})$.

(the $O^{\ast}$-star notation just suppresses polynomials). And it says that the Sparsification Lemma is equivalent to:

  If ETH holds, then $3$-SAT instances cannot be solved in time $O(poly(n) 2^{o(n+m)})$.

I do not understand the second claim, so I am asking if anyone could please explain why this is a statement of the Sparsification Lemma, what has it to do with the Lemma as stated before?

I think your confusion might come from misquoting the statement of ETH.

  $3$-SAT instances (with $n$ variables and $m$ clauses) cannot be solved in time $poly(n)\cdot 2^{o(n)}$.

This statement is not ETH, but rather its weak (but often very useful) corollary. The ETH claims the following:

  There exists a $\delta>0$ such that no algorithm with running time $poly(m)\cdot 2^{\delta n}$ can solve $3$-SAT.

Now we can actually use the Sparsification Lemma to prove the following:

  If ETH holds, then $3$-SAT instances cannot be solved in time $poly(m)\cdot  2^{o(n+m)}$.

Assume that there is an algorithm $A$ which solves $3$-SAT in time $poly(m)\cdot  2^{o(n+m)}$. For any $\delta>0$, we'll construct an algorithm $B_\delta$ which solves $3$-SAT in time $poly(m)\cdot 2^{\delta n+o(n)}$. (This contradicts ETH and finishes the proof.)

First, the algorithm $B_\delta$ takes an input formula $\phi$, applies the Sparsification Lemma with $\varepsilon=\delta$, and in time $poly(m)\cdot 2^{\delta n}$ produces $2^{\delta n}$ formulas $\phi_i$, such that $\phi$ is satisfiable if and only if $\exists i\colon \phi_i$ is satisfiable. Now the algorithm $B_\delta$ solves each of $\phi_i$ using the algorithm $A$. Note that by Sparsification Lemma the number of clauses in $\phi_i$ is $O(n)$, thus, each $\phi_i$ is solved by $A$ in time $2^{o(n)}$. Now the total running time of $B_\delta$ is $$poly(m)\cdot 2^{\delta n} + poly(m)\cdot 2^{\delta n}2^{o(n)}=poly(m)\cdot 2^{\delta n+o(n)}\; .$$


Implications of unprovability of $P\neq NP$ I was reading "Is P Versus NP Formally Independent?" but I got puzzled.
It is widely believed in complexity theory that $\mathsf{P} \neq \mathsf{NP}$. My question is about what if this is not provable (say in $ZFC$). (Let's assume that we only find out that $\mathsf{P} \neq \mathsf{NP}$ is independent from $ZFC$ but no further information about how this is proven.)
What will be the implications of this statement? More specifically,
hardness
Assuming that $\mathsf{P}$ capture the efficient algorithms (Cobham–Edmonds thesis) and $\mathsf{P} \neq \mathsf{NP}$, we prove $\mathsf{NP\text{-}hardness }$ results to imply that they are beyond the present reach of our efficient algorithms. If we prove the separation, $\mathsf{NP\text{-}hardness}$ means that there is no polynomial time algorithm. But what does an $\mathsf{NP\text{-}hardness }$ result mean if the separation is not provable? What will happen to these results?
efficient algorithms
Does unprovability of the separation mean that we need to change our definition of efficient algorithms?

Your question might better be phrased, "How would complexity theory be affected by the discovery of a proof that P = NP is formally independent of some strong axiomatic system?"

It's a little hard to answer this question in the abstract, i.e., in the absence of seeing the details of the proof.  As Aaronson mentions in his paper, proving the independence of P = NP would require radically new ideas, not just about complexity theory, but about how to prove independence statements.  How can we predict the consequences of a radical breakthrough whose shape we currently can't even guess at?

Still, there are a couple of observations we can make.  In the wake of the proof of the independence of the continuum hypothesis from ZFC (and later from ZFC + large cardinals), a sizable number of people have come around to the point of view that the continuum hypothesis is neither true nor false.  We could ask whether people will similarly come to the conclusion that P = NP is "neither true nor false" in the wake of an independence proof (for the sake of argument, let's suppose that P = NP is proved independent of ZFC + any large cardinal axiom).  My guess is not.  Aaronson basically says that he wouldn't.  Goedel's 2nd incompleteness theorem hasn't led anyone that I know of to argue that "ZFC is consistent" is neither true nor false.  P = NP is essentially an arithmetical statement, and most people have strong intuitions that arithmetical statements—or at least arithmetical statements as simple as "P = NP" is—must be either true or false.  An independence proof would just be interpreted as saying that we have no way of determining which of P = NP and P $\ne$ NP is the case.

One can also ask whether people would interpret this state of affairs as telling us that there is something "wrong" with our definitions of P and NP.  Perhaps we should then redo the foundations of complexity theory with new definitions that are more tractable to work with?  At this point I think we are in the realm of wild and unfruitful speculation, where we're trying to cross bridges that we haven't gotten to and trying to fix things that ain't broke yet.  Furthermore, it's not even clear that anything would be "broken" in this scenario.  Set theorists are perfectly happy assuming any large cardinal axioms that they find convenient.  Similarly, complexity theorists might also, in this hypothetical future world, be perfectly happy assuming any separation axioms that they believe are true, even though they're provably unprovable.

In short, nothing much follows logically from an independence proof of P = NP.  The face of complexity theory might change radically in the light of such a fantastic breakthrough, but we'll just have to wait and see what the breakthrough looks like.


Good reference about approximate methods for solving logic problems It is known that many logic problems (e.g. satisfiability problems of several modal logics) are not decidable. There are also many undecidable problems in algorithm theory, e.g. in combinatorial optimization. But in practice heuristcs and approximate algorithms works well for practical algorithms.

So one can expect that approximate algorithms for logic problems can be suitable as well. However the only reseach trend along these lines I have managed to find is the max-SAT problem and its development was active in nineties.

Are there some other active research trends, workshops, keywords, good references for the use and development of approximate methods for modal logics, logic programming and so on?

If automated reasoning is expected to gain prominence in the future applications of computer science then one will have to be able to go beyond undecidability constraints of logics and approximate methods or heuristics can be natural path to follow, isn't it so?

The motivation you state for dealing with undecidability applies to decidable but hard problems as well. If you have a problem that is NP-hard or PSPACE-hard, we will typically have to use some form of approximation (in the broad sense of the term) to find a solution.

It is useful to distinguish between different notions of approximation.

Numeric approximation: applies when you have a metric on the solution space and you can measure distance from the solution. This is the case for problems like #SAT, where you count solutions and can design an approximation algorithm that returns a value within $\varepsilon$ of the solution.
Probabilistic approximation: when you use a randomized algorithm you can give up certainty in the solution you will obtain every time you run the algorithm. You can move between randomness in the algorithm and randomness in the solution space by considering a probability distribution over solutions. Then the approximation here is that with some probability greater than $\delta$, you will obtain a correct solution.

There are $(\varepsilon,\delta)$-algorithms for problems like ALLSAT which combine the two perspectives above. In the specific case of undecidable problems, or problems where there is no obvious metric and we do not want to use a randomized algorithm, there is a question of what notion of approximation to use. This problem arises specifically in the analysis of programs in optimizing compilers and in program verification. Determining complex properties of programs is either undecidable or computationally expensive, so some form of approximation is required.

Here is an example of a different notion of approximation.  Suppose you perform a computation like multiplying two large numbers and want to check if it the multiplication was correct. There are lots of heuristic techniques that are used in practice to check correctness without repeating the calculation again. You can check that the signs were multiplied to obtain the right sign. You can check whether the numbers have the right parity (even/odd number properties). You can use a more sophisticated check like Casting out nines. All these techniques have a common property that they can tell you if you made a mistake, but they cannot guarantee if you got the right answer. This property can be viewed as a logical approximation because you may be able to prove that the original calculation is wrong but you may not be able to prove that it is correct.

All the checks I have mentioned above are examples of a technique called abstract interpretation. Abstract interpretation makes completely rigorous a notion of logical approximation distinct from numeric and probabilistic approximations. The problem I described with analysis of a single calculation extends to the more complex case of analysis of a program. The literature on abstract interpretation has developed techniques and frameworks for approximate, logical reasoning about programs, and more recently about logics. The following references might be useful.

Abstract Interpretation in a Nutshell by Patrick Cousot, which is a simple overview.
Overview of Abstraction by Patrick Cousot, as part of his course. There is a very nice example of abstraction for determining properties of a boquet of flowers. The bouquet analogy includes fixed points and can be made completely mathematically precise.
Course on Abstract Interpretation by Patrick Cousot, if you want all the depth and details.
Abstract interpretation and application to logic programs, Patrick Cousot and Radhia Cousot, 1992. Applies to logic programs, as per your request. The initial section also formalises the casting out nines procedure as an abstract interpretation.

All of this has typically been applied to reason about computer programs. There has been fairly recent work on applying ideas from abstract interpretation to study decision procedures for logics. The focus has not been modal logic but satisfiability in propositional logic and quantifier-free first-order theories. (Since I have worked in this space, one paper below is mine)

A generalization of Staalmarck's method by Aditya Thakur and Thomas Reps, 2012. Gives a generalisation of Staalmarck's method to problems in program analysis.
The reduced product of abstract domains and the combination of decision procedures, Patrick Cousot, Radhia Cousot, and Laurent Mauborgne, 2011. This paper studies the Nelson-Oppen technique for combining decision procedures and shows that it can also be used for incomplete combinations, which is particularly interesting if you have undecidable problems.
Satisfiability Solvers are Static Analysers, my paper with Leopold Haller and Daniel Kroening, 2012. Applies the lattice-based approximation view to characterise existing solvers. You could also look at my slides on the topic, instead.

Now none of the papers above answers your specific question about attacking satisfiability problems which are undecidable. What these papers do is take an approximation-oriented view of logical problems that is not numeric or probabilistic. This view has been applied extensively to reason about programs and I believe it addresses exactly what you are asking.

To apply it to modal logic, I would suggest a starting point is to use algebraic semantics of Jonsson and Tarski or the later semantics of Lemmon and Scott. This is because abstract interpretation is formulated in terms of lattices and monotone functions, so Boolean algebras with operators are a convenient semantics to work with. If you want to start with Kripke frames, you can apply Jonsson and Tarski's duality theorem (which some may call Stone duality) and derive the algebraic representation. Thereafter, you can apply the theorems of abstract interpretation for logical approximation.


Name of the problem to find the maximum number of characters covered by a set of strings I am interested in the following problem. One has two collections $Q$ and $T$ of strings, and a set $A$ of alignments of strings in $Q$ to strings in $T$. I want to find a subset $A'$ of $A$ that (i) involves each element of $Q$ only once and (ii) maximizes the total number of characters in elements $T$ that are covered by an alignment in $A'$.

(To be precise: Let $a$ be an alignment in $A$. We can think of $a$ as a tuple $(q,t,f)$ where $q\in Q$, $t\in T$, and $f : \mathcal I_a \to \mathcal J_a$ is a bijection such that $f(i)=j$ if $a$ aligns the $i$th character of $q$ to the $j$th character of $t$. Here $\mathcal I_a \subset \{1,2,\dots,|q|\}$ and $\mathcal J_a \subset \{1,2,\dots,|t|\}$, where $|\cdot|$ means length. We can think of characters in elements of $T$ as pairs $(t,j)$ where $t\in T$ and $j\in\{1,2,\dots,|t|\}$. We say that $(t,j)$ is covered by an alignment in $A'$ if there exists $a=(q,t',f)\in A'$ such that $t=t'$ and $j\in\mathcal J_a$. (Note that there might exist several such $a\in A'$.) Let $\chi(t,j,A') = 1$ if such an $a\in A'$ exists, and 0 otherwise. We want to maximize the cardinality of $\{(t,j) : \chi(t,j,A')=1\}$ over $A'\subset A$ such that for all $q\in Q$, there exists at most one $a=(q',t,f)\in A'$ with $q=q'$.)

My question: What is a name for this problem, if any? Thanks in advance! I guess that it is related to maximum matchings and maximum coverage, but it's not quite the same as either.

This sounds like the maximum cover problem which is NP-hard.


Matrix permanent is 0 Valiant's theorem says that computing the permanent of an $n\times n$ matrix is #P-hard. Is the problem of determining if a permanent is 0 any easier? This arises in the context of sequence A006063 in the OEIS, where membership is determined by the sign (0 or nonzero) of a certain permanent. (A solution to the restricted problem would be enough for me.)

Expanding my comment:

Computing the permanent of a matrix is #P-hard (Valiant 1979) even if the matrix entries are all either 0 or 1.

We can interpret a matrix $M \in \{0,1\}^{n \times n}$ as a bipartite graph $G$ with left vertices $[n]$ and right vertices $[n]$, where the edge $(i,j)$ is present if and only if $M_{i,j}=1$. A perfect matching is a subset of the edges of $G$ such that every left and right vertex is incident to exactly one vertex in this subset. Now the permanent of the matrix $M$ is simply the number of perfect matchings in $G$.

To see why this is the case, note that each perfect matching in $G$ can be uniquely specified by a permutation $\sigma : [n] \to [n]$. So that the matching is the set of edges $\{(i,\sigma(i)) : i \in [n]\}$. That is each left vertex $i$ is matched to right vertex $\sigma(i)$. A permutation $\sigma$ is a valid matching if and only if all the edges $(i,\sigma(i))$ are present in $G$. By the definition of $G$, a permutation $\sigma$ gives a valid matching if and only if $\prod_{i=1}^n M_{i,\sigma(i)}=1$. Thus the number of valid matchings in $G$ is exactly $$\sum_{\sigma \in S_n} \mathbb{I}[\sigma \text{ specifies a valid matching}] = \sum_{\sigma \in S_n} \prod_{i=1}^n M_{i,\sigma(i)} = \mathrm{Permanent}(M).$$

As a consequence $\mathrm{Permanent}(M) \ne 0$ if and only if $G$ has a perfect matching. There are simple polynomial-time algorithms to find a perfect matching in a bipartite graph. Thus there is a polynomial-time algorithm to determine whether the permanent of a matrix is nonzero.

This works for all matrices with non-negative entries: Simply replace each nonzero entry with 1. This will distort the permanent but will not change whether or not it is nonzero.

The simplest algorithm for finding a perfect matching is augmenting paths and runs in $O(n^4)$ time.

We can actually do better and approximate the permanent for matrices with non-negative entries.


A clarification in Signature schemes for Strong Unforgeability. Signature scheme is strongly unforgeable.
"making the message m being signed depend on the randomness r — we break
the proof of security for the underlying signature."

From Paper: Strongly Unforgeable Signatures Based on Computational Diffie-Hellman - Dan Boneh, Emily Shen, and Brent Waters.

Can some one point out how a scheme can be broken when the message being signed depends on the randomness?

Thanks. Please let me know if I am not clear. The paper has it all.

Their comment was not meant to apply to all signature schemes, just the specific construction they are talking about in that paragraph. (Also, it was not meant as a formal statement; it was just mentioned as part of the intuition for their construction.)


"Security Against Covert Adversaries" question I was reading the paper Security Against Covert Adversaries: Efficient Protocols for Realistic Adversaries by Aumann and Lindell, and had some questions with the protocol for covert OT given errorless homomorphic encryption.  This is section 5.1, and in this .pdf it's page 25.
I've put just pages 25 and 26 (the ones relevant to my question) here.

The protocol itself is a little long (a little over a page for the full description).  I'll mention the part I have questions about.

As part of the protocol, the ciphertext $\tilde{c}_0 = x_0\cdot_E c_0$ is computed.
Later it's claimed that (if $c_0$ is an encryption of $0$) that:
$$\tilde{c}_0 = x_0\cdot_E c_0 = E_{pk}(0\cdot x_0) = E_{pk}(0)$$

I have two real questions about this:

It seems like it should be true that $x_0\cdot_E c_0 = Enc_{pk}(Dec_{sk}(x_0)\cdot Dec_{sk}(c_0))$.
It's instead stated (implicitly) that $x_0\cdot_E c_0 = Enc_{pk}(x_0\cdot Dec_{sk}(c_0))$.
Is this a typo, or a misunderstanding on my part of what homomorphic encryption is?
In the part I mentioned about $\tilde{c}_0$, it seems like $0\cdot x_0$ is an operation in the message-space group.
For the proof of security, it seems vital that $0\cdot x_0 = 0$.
But this seems to imply that $0$ isn't invertible (as it typically isn't), so is this really occuring in a group?
If not, is this ok for some other reason?

I haven't really worked with homomorphic encryption before (or much computer science to be honest), so I apologize if these questions are rather basic.

1) $x_0$ is (indeed) a plaintext. (Perhaps to guess at where confusion arose from:) the 'more modern' version of homomorphic encryption is fully homomorphic encryption (FHE) fully supporting both additive and multiplicative homomorphisms, whereas the paper you're reading was published about 2.5 years before Gentry's original FHE scheme came out. (Check out the wikipedia article on homomorphic encryption for more examples..)

This paper uses additive-homomorphic encryption, which allows the computation $Enc(pk, x_0) + Enc(pk, x_1) = Enc(pk, x_0 + x_1)$. Note that additive-homomorphic encryption schemes tend to support (must.. support?) an additional "scalar-multiplication homomorphism." That is, the computation
$$x_0 \cdot Enc(pk, x_1) = Enc(pk, x_0\cdot x_1),$$
where plaintext $x_0$ is public information.

(Note that the above is different than FHE, which supports both the prior additive homomorphism, and simultaneously the "full" multiplicative homomorphism of $Enc(pk, x_0) \cdot Enc(pk, x_1) = Enc(pk, x_0\cdot x_1).$)

2) Read it as a field =)


Statistical Distance Growth Given K Independent Copies Let $X$ and $Y$ be distributions with statistical distance (total variation distance) at most $d$. What is the best upper bound you can give on the statistical distance between $k$ independent copies of $X$ and $k$ independent copies of $Y$?
I can show using a "hybrid argument" that it is at most $k\cdot d$, and I am looking for something better (maybe not always, but at least in some cases).

For example if $d=1/2$ and $k=2$ this bound is $1$ which is meaningless and it cannot be reached by actual distributions because $X_1,X_2$ and $Y_1,Y_2$ have statistical distance $1$ iff their supports are disjoint which would imply that the supports of $X$ and $Y$ are also disjoint in contradiction to $X$ and $Y$ having statistical distance at most $1/2$. The best example I could find was $X\equiv1$ and $Y$ being a uniformly distributed bit so the distance between $X$ and $Y$ is $1/2$ and the distance between $X_1,X_2$ and $Y_1,Y_2$ is $3/4$.

For general $k,d$ I'd like to show that the distance between $k$ samples of $X$ and $k$ samples of $Y$ is at most $1-\left(1-d\right)^k$. (For sanity check: $\left(1-d\right)^k\geq 1-d\cdot k$ for $k\geq 1,d\in\left[0,1\right]$ can be easily shown using basic calculus).
Can you do better (give a counter example), or can you prove that it is the best?

See the "inclusion-exclusion" Lemma 2.2 here
https://www.cs.bgu.ac.il/~karyeh/mark-conc2.pdf .
For distributions $p,q,p',q'$, we have
$$
||p\otimes q-p'\otimes q'||
\le
||p-p'||
+
||q-q'||
-
||p-p'||
\cdot
||q-q'||.
$$

From here, it immediately follows that if $p=p_1=p_2=\cdots=p_k$
and $q=q_1=p_2=\cdots=q_k$ and furthermore $||p-q||=d$,
then the TV between the corresponding products is upper-bounded by $1-(1-d)^k$. This is proved explicitly in Lemma 4.2 in the linked paper.


Applications of Christol theorem I'm looking forward to know about applications of Christol theorem mentioned in Jefrrey Shallit's Number theory and formal languages. One of them is purely algebraic: if $f, g \in \mathbb{F}_q[[z]]$ are algberaic then their Hadamard product $f \odot g$ is also algebraic.

Can you name other applications?

There are lots of applications to transcendence in finite characteristic.  Christol's theorem makes it possible to give proofs of theorems about transcendence of formal power series using the tools of formal language theory.  This was pioneered by Allouche, Valerie Berthe in her thesis, etc.


Comparing two graphs I have a quite big graph which has millions of nodes and edges. I modify the graph using an algorithm which only changes small portion of edges. At then end, I'd like to investigate how the algorithm affects the graph. There are a couple of options I have considered, but neither are appropriate.

1) compare the graph metrics (e.g. avg nodes degree, avg. coefficient clustering) for two graphs. The problem is as the algorithm only affects small portion of edges, and as there are great number of nodes and edges, the reported values are almost the same.

2) sample portion of each graph and find graph metrics on the sampled graphs. Again, the reported numbers are quire similar.

Is there any metric or technique to compare only subgraphs of two graphs? That is, I would like to consider only the modified nodes in the comparison.

here is one table about the different similarity measures which can be found in this paper https://www.cs.cmu.edu/~jingx/docs/DBreport.pdf


Find the maximum flux path between two nodes Given a graph $G$ and two vertices $s$ and $t$, I want the maximum flux path from $s$ to $t$.That is, imagine $G$ to be a flow network with capacities on the edges. I want to find a single path that can carry the maximum flow between $s$ and $t$.

Note that this is not the same as the maximum flow problem where you can compute flows from multiple paths.

Can someone point me to fast algorithms for computing the max flux path?

The problem is known as "Maximum capacity path problem" or  "Widest path problem"

See the original paper: T. C. Hu, "The Maximum Capacity Route Problem", Operations Research Vol. 9, No. 6 (Nov. - Dec., 1961), pp. 898-900

or the linear time algorithm described in: A. P. Punnen, "A linear time algorithm for the maximum capacity path problem" (but I didn't download/read it)


What are "$\mu$-recursive functions" and $\mu$-calculus? I saw in this question a reference to $\mu$-recursive functions or $\mu$-calculus as some computation model equivalent to Turing machines and $\lambda$-calculus. I know about these two but never heard of $\mu$-calculus. Can you briefly describe it and compare it with the other models? Bonus points for link references and books for beginners. Thanks in advance.

Edit: Ok, just for clarification i'm interested in both $\mu$-recursive functions and $\mu$-calculus.

If it is the μ-recursive functions you are interested in (and not the μ-calculus, which is a totally different thing as slimton pointed out) it makes the most sense if you start looking at the primitive recursive functions (PRFs). The set of PRFs is interesting in it self and it turns out that the μ-recursive functions can be introduced by an extension of it.

Here are some slides that seems to be a relatively gentle introduction:
Link


Is there a gap amplification type of result for the Graph Isomorphism Problem? Suppose $G_1$ and $G_2$ are two undirected graphs on vertex set $\{1, \dotsc, n\}$. The graphs are isomorphic if and only if there is a permutation $\Pi$ such that $G_1 = \Pi(G_2)$, or more formally, if there is a permutation $\Pi$ such that $(i,j)$ is an edge in $G_1$ if and only if $(\Pi(i),\Pi(j))$ is an edge in $G_2$. The Graph Isomorphism Problem is the problem of deciding whether two given graphs are isomorphic.

Is there an operation on graphs that produces "gap amplification" in the style of Dinur's proof of the PCP Theorem? In other words, is there a polynomial time computable transformation from $(G_1,G_2)$ to $(G'_1,G'_2)$ such that

if $G_1$ and $G_2$ are isomorphic, then $G'_1$ and $G'_2$ are also isomorphic, and
if $G_1$ and $G_2$ are not isomorphic, then for each permutation $\Pi$, the graph $G'_1$ is "$\epsilon$-far" from $\Pi(G'_2)$ for some small constant $\epsilon$, where $\epsilon$-far means that if we choose $(i,j)$ uniformly at random, then with probability $\epsilon$ either

$(i,j)$ is an edge of $G'_1$ and $(\Pi(i),\Pi(j))$ is not an edge of $G'_2$, or
$(i,j)$ is not an edge of $G'_1$ and $(\Pi(i),\Pi(j))$ is an edge of $G'_2$.

I do not know if such a thing could exist or not. But it is interesting (and perhaps timely) to note that such a "gap amplification" would likely imply a quasipolynomial time algorithm for graph isomorphism (different than the recently announced one)

In this paper, an approximation algorithm is given for the "MAX-PGI" problem of maximizing matched pairs of edges/non-edges; if we reduce from GI to "Gap-MAX-PGI", then we can approximate to distinguish which side of the gap we are on.

So, I think Dinur's proof of the PCP theorem is unlikely to be directly generalizable to such a "gap amplifier", given the hurdles that would have to be overcome.


Modular Decomposition and Clique-width I am trying to understand some concepts about Modular decomposition and Clique-width graphs.

In this paper ("On P4-tidy graphs"), there is a proof of how to solve optimization problems like clique-number or chromatic-number using Modular decomposition.
Solving these problems by composing (using disjoint sum or disjoint union) two graphs G1,G2 is easy when you know the answer for G1 and G2. Since the prime-graphs on the decomposition of P4-tidy graphs are bounded graphs (i.e. C5,P5,etc.), it is easy to solve it for these "base case" and then solve it for compositions.
Hence by using the decomposition tree it is possible to solve these problems in linear time.

But it seems that this technique would work with any graph class such that graph-primes are bounded.
Then I found this paper "Linear Time Solvable Optimization Problems on Graphs of Bounded Clique Width" which seems to make the generalization I was looking for but I couldn't understand it very well.

My question are:

1- Is equivalent to say that prime-graphs of the decomposition tree are bounded (like in the P4-tidy graphs case) and say that a graph has the property "Clique-Width" bounded?

2- In case the answer for 1 is NO, then: Does exists any result about classes of graphs with graph-primes bounded (like in P4-tidy graphs) and thus optimization problems like clique-number solvable on linear time on all these classes?

you will find an introductory text on clique-width (cwd for short) here: Upper bounds to the clique-width of graphs (B. Courcelle and S. Olariu, DAM 101). You can find more recent results in this survey: Recent developments on graphs of bounded clique-width (M. Kaminski, V. Lozin, M. Milanic, DAM 157(12): 2747-2761 (2009))

Cwd is a complexity measure based on graph operations that generalise word concatenation. Infinite countable graphs can have bounded cwd. You will say that a set (possibly infinite) of graphs (finite or countable) has bounded cwd if there exists a constant k such that any graph in this set has cwd at most k. For instance, complete graphs have cwd 2, distance hereditary graphs cwd at most 3, ...

1) The link between cwd and modular-dec is the following: cwd(G) = max {cwd(H) | H prime in the modular dec of G}. Hence, you can say that cwd generalises the fact that "prime graphs has bounded size". You can have graphs with prime-graphs of unbounded size but with bounded cwd.

2) if the size of prime-graphs is bounded, the cwd is bounded. The results in the paper you cite says that any problem expressible in MSOL can be solved efficiently in graph classes of bounded cwd. This set of problems include many NP-complete problems: clique-number, stable number, 3-colorability, ...

Some algorithmic aspects of  modular dec are studied here "A survey of the algorithmic aspects of modular decomposition" (M. Habib and C. Paul, Computer Science Review 4(1): 41-59 (2010))


Inclusion probability of irregularly shaped polygon I have two shapes, one is a circle, let's call it Circle A, and another irregularly shaped Polygon B. A will always have a greater area than B. Both of these polygons exist inside an area S.

My task is to compute the inclusion probability of Polygon B in a random sample, where inclusion is defined as Polygon B being entirely inside of Circle A (the circle).

My assumption is that the inclusion probability of Polygon B is the area of another Polygon C, which equates to the area in which Circle A can be placed so that it can enclose Polygon B divided by the total area of S.

If this assumption is correct, then computing Polygon C seems computationally intensive.

Is there an efficient method for finding Polygon C?

The first thing to notice is that an $n$-vertex polygon polygon $B$ is inside circle $A$ if and only if all of the vertices of $B$ are inside $A$. (1)

So the solution to your problem is exactly the area of $n$ arbitrary intersecting circles, each of radius $r$ and centered at a vertex of $B$. (You then divide by $S$ to get the final probability).  There's an interesting blog about this problem here which includes some heuristic solutions which may be sufficient for your use case.

From a theoretical point of view, the furthest-point Voronoi diagram gives us a good starting point.  Let's look at a point $p$ inside a cell of the furthest-point Voronoi diagram.  We want to know if the circle $A$ centered at $p$ contains $B$.  By the above, this happens if and only if all vertices of $B$ are within distance $r$ of $p$.  Now, since we're inside a cell of the furthest-point Voronoi diagram, we can just test whether or not $p$ is within distance $r$ of that furthest point.

In particular, the area we want within a given Voronoi cell is the intersection of that Voronoi cell with a single circle of radius $r$.  This can be easily calculated in time linear in the number of edges of the cell.  Since the furthest-point Voronoi diagram has $O(n)$ cells with $O(n)$ total edges, this takes $O(n)$ time in total.

Then the total running time is dominated by the time to calculate the furthest-point Voronoi diagram, which is $O(n \log n)$. A similar strategy gives you an explicit region $C$ in the same amount of time.

(1): The "only if" direction is obvious.  To see the "if" direction, we can first note that by convexity if all vertices of $B$ are inside $A$, then all edges of $B$ must be as well.  The same argument then extends to all interior points of $B$ since they must lie on a line between two vertices or edges.


What is known about NP hard problems that access preprocessed information? Please accept my apologies ahead of time since I fear that this isn't an adequate question for cstheory.  I plan on releasing my ideas to get feedback, but I don't know if my target audience will include state-of-the-art reaseachers.  I'd like to know more about the research that is already out there concerning this question.

Essentially, what I think I've discovered is an oracle.  The oracle must be precomputed, which will probably take an exponential amount of time.  However, once computed, it can essentially answer any question about 3-SAT fast.  In other words, it can then solve any 3-SAT problem in polynomial time/space.  I'm wondering what has been researched in this scenario.

MY ORIGINAL QUESTION

As an armchair cstheory enthusiast, I'm now working on a way to preprocess 3-SAT.  I'm wondering how this relates to research on oracles and related ideas.  Please let me briefly describe my method, or conjectured approach.

We take a given problem size.  Essentially we have exactly $2^n$ clauses and $v$ variables.  (Note that problems smaller than this can automatically be solved, too.)  After we know the maximum amount of clauses, we can preprocess information for every possible 3-SAT clause, given the information just stated.  This may take an exponential amount of information, even for each individual clause.

However, once the information is preprocessed, we can solve 3-SAT fast.  In other words, using this pre-computed database, which is polynomial in size, we can determine satisfiability for a particular instance as well as generate a certificate in polynomial time and space.

So if I'm correct, we use an oracle and we can ensure that 3-SAT can be solved in polynomial time and space.  However, the oracle itself takes a possibly exponential amount of time and space to compute.

My question is where in the literature can I find information concerning pre-computing information (like I have described) to solve NP-hard and NP-complete problems in polynomial time and space?  What is known about this approach?  I don't mean to be vague, but I'm simply trying to find out what has been considered about an approach like this in the past.  I plan on eventually releasing my ideas if they are interesting, but I would like to know if they have already been researched.

Precomputation is often related to the class P/poly which captures problems solvable in polynomial time by Turing machines with access to some poly-sized advice string, that only depends on the size of the instance, but not the instance itself. The Karp-Lipton theorem states, that NP is not contained in P/poly, unless the PH collapses to the second level, which is considered unlikely by many complexity theorists.


What's the difference between reduction strategies and evaluation strategies? From the evaluation strategy article on Wikipedia:

  The notion of reduction strategy in lambda calculus is similar but distinct.

From the reduction strategy article on Wikipedia:

  It is similar to but subtly different from the notion of evaluation strategy in computer science.

What is the subtle distinction between evaluation strategies and reduction strategies that these two articles hint at? Are they just two similar concepts from different domains?

A reduction strategy is a function on Lambda that picks one redex (reducible expression) from all possible redexes -- depending on what you define as a redex.

Informally, an evaluation strategy is the order in which a language evaluates its arguments. A parameter-passing strategy is what the language hands to the function.

To understand the connection among these, study Plotkin's paper on Call-by-name, call-by-value, and the lambda calculus. He clearly spells out that you want to choose distinct AXIOMS depending on which order of evaluation you want. For Cb-name you want the old beta axiom and for cb-value you want a beta-value axiom. If you do that, all meta-theorems work out the same for both flavors. I showed later on (with many collaborators) that this idea generalizes to everything the world of PL has studied.

It's all technical, not some poem that can be interpreted. Just read up on it.

-- Matthias Felleisen

p.s. I will say that I think people will have an easier time understanding Plotkin's paper from Part I in our Redex book. But yes, it's 3x as long.