§ FOL + Fixpoint + Counting does not capture P

§ The Language

§ Game 1: k tuple pebble game

§ Game 2: cops and robbers game

Game proceeds as follows: In code:
def do_cops_win (robber_cur_pos : Vec2, 
  cops_cur_pos : List[Vec2], 
  graph : Graph,
   while True:
     # cops make strategy.
     cops_new_pos = cop_strategy (cops_cur_pos) # cops don't know where robber is?
     # insecure channel, robber learns of this and plots strategy
     robber_new_pos = robber_strategy(graph,
       cops_cur_pos, # robber knows where the cops currently are
       cops_new_pos, # robber also wknows where the cops plan to be (insecure channel)
     # robber tries to go to new position. If an avoiding path does not exist,
     # robber is trapped.
     if not avoiding_path_exists(robber_cur_pos, cops_cur_pos, robber_new_pos):
        return "cops win"
     # robber successfully makes it.
     robber_cur_pos = robber_new_pos
     # cops slowly make their way to their new position.
     cops_cur_pos = cops_new_pos

§ Warmup: n+1 cops needed for nxngrid.

Proof by picture. Consider a 3x3 grid, cells denoted by o:
Cops will occupy the first column and the first cell of the first row:
This forces the robber to live in the rest of the grid, and crucially, cuts of access to the top left position 1X. So in the next round, the cops will take the cop at 1X and move her to 2Y. The inaccessible cell is marked with -, where the cops have a guarantee that the robber cannot be:
Now note that the cell 2Yis similarly inaccessible, and thus also becomes -in the next turn.
Now we see that 3Xis unreachable, so we can take the cop at 3X and move her to 3Z to make 3Y inaccessible:
Victory for the cops:
  • In general the cops have a winning strategy if the can "sweep" the graph, and maintain some territory that they expand in each turn.
  • Note that the for nxn grid, the max-cut (NOT min-cut) is n, and any smaller graph that we get after removing cut edges will have at most nedges. So we can use n cops to repeatedly cut of access. There's probably a log(2n)number of rounds strategy by subdivision that cuts of access by halving each round, either horizontally or vertically.

§ Toroidal graphs

  • what you get if you cut a torus into squares.
  • Create an nxngrid, and connect vertices (i, j) → ((i+1) % n, j)and similarly connect (i, j) → (i, (j+1)%n). This gives a torus.
  • We claim that for the cops and robbers game, kk cops does not suffice to win.

§ Robber can win on a toroidal graph with kk cops.

  • For simplicitly, once again, let k=4k = 4.
  • Suppose the cops are on a set XX of kk vertices.
  • We want to show that GXG - X ha a connected component with at least half the vertices of GG.
  • Let's consider one possible configuration where they are in a row:
  • See that this does not cut off access, since we can move from (-, 1) to (-, 4) as the top and bottom edges are glued. So this is useless for the cops.
  • Now let's try and consider a configuration where all the cops are on distinct columns:
  • In this case too, the graph is connected, and has a large connected component.
  • The only way the cops can cut of a region is to encircle it:
  • In this case, the outside has kˆ2 - kvertices, which is larger that kˆ2/2: kˆ2 - k = k(k -1) > k * k/2.

§ Linear system of equations over F2

  • We will claim that system of linear equations over F2 (integers mod 2) cannot be solved by FPC (first order fixpoint + counting).
  • The problem can clearly be solved in polytime by gaussian elimination.

§ Encoding in unordered structure

  • consider structures over the domain x1, ..., xn and e1...em.
  • xi are variables, ei are equations.
  • unary relation E0(ei) if RHS of ei is 0.
  • unary relation E1(ei) if RHS of ei is 1.
  • M(xi, ej) if xi in ej.
  • Note that this suffices, since any linear equation over F2 can be written as x1 + ... xn = 0/1.
  • See that this problem is equivalent to XOR-SAT.
  • See that we can negate variables by writing not(xi) = 1 + xi.
  • Let Solv(F2) be the class of structures representing solvable systems.

§ Constructing the system of equations

  • Let GG be a toroidal graph.
  • Define EGE_G, the system of equations next, based on GG.
  • For each edge, we get two variables x[e,0],x[e,1]x[e, 0], x[e, 1] for each edge ee.
  • For each vertex vVv \in V, let e[v,1],e[v,2],e[v,3],e[v,4]e[v, 1], e[v, 2], e[v, 3], e[v, 4] be the edges incident on vv.
  • We make 16 equations: x[e[v,1],i]+x[e[v,2],j]+x[e[v,3],k]+x[e[v,4],l]=(i+j+k+l)x[e[v, 1], i] + x[e[v, 2], j] + x[e[v, 3], k] + x[e[v, 4], l] = (i + j + k + l) for i,j,k,l{0,1}i, j, k, l \in \{ 0, 1\}.
  • Intuitively, we pick a bitstring b\vec b, and we write the equation jx[e[v,j],b[j]]=parity(b)\sum_j x[e[v, j], \vec b[j]] = \texttt{parity}(\vec b).
  • First see that this system is satisfiable by setting x[,i]x[-, i] to ii, since the RHS is given by addint i+j+k+li + j + k + l, so will the lhs!
x[e[v,1],i]+x[e[v,2],j]+x[e[v,3],k]+x[e[v,4],l]=?(i+j+k+l)=i+j+k+l=?i+j+k+l \begin{aligned} &x[e[v, 1], i] + x[e[v, 2], j] + x[e[v, 3], k] + x[e[v, 4], l] =_? (i + j + k + l) \\ &= i + j + k + l =_? i + j + k + l \end{aligned}
  • We make another version of the equation system, E~G\tilde E_G, which is the same system, except for a fixed vertex cc (for contradition), we change the parity of the equation to be .
  • See that we perturb 1616 equations, for all possible choices of bb for a fixed cc.
  • See that this set of equations is unsatisfiable. Add up all equations that only have variables of the form x[e,0]x[e, 0].
  • The sum of all left hand sides will be double counting each variable, since we make an equation for each vertex, but we have a variable per edge. So the LHS will be zero.
  • However, see that due to our perturbation, the RHS must be 1, since we changed the parity (TODO: make this more rigorous / proof by example).
  • Now we show that for each kk, there is a large enough GG such that EGC[k]EG~E_G \equiv{C[k]} E_{\tilde G}.
  • This means that FPC cannot distinguish between the cases where the solution is true and false.
  • Thus the problem Solv(Z2)cannot be solved by FPC.

§ Putting the pieces together

  • Suppose that GG is the above toroidal graph such that the robber has a winning strategy for the 2k2k cops and robbers game played on GG.
  • We can use this to construct a winning strategy for the duplication in the kk pebble bijection game on EGE_G and EG~E_{\tilde{G}}.