[Prev][Next][Index][Thread]
Constant-only fragment of MLL is NP-complete
Date: Mon, 6 Apr 92 21:50:47 -0700
To: linear@cs.stanford.edu
Constant Multiplicative Linear Logic is NP-complete
Patrick Lincoln and Tim Winkler
In work announced last year on LINEAR and to be reported at this
year's LICS, Max Kanovich showed that multiplicative linear logic and
its Horn fragment are NP-Complete. Together with Natarajan Shankar,
Tim Winker and I developed an encoding of an NP-hard problem using
only two propositions. This has now led to an encoding of an NP-hard
problem in MLL using only the constants one and bottom and the
connectives par and tensor. Bottom-only Horn MLL, and fragments
containing only linear implication and bottom are also NP-Complete.
Some time ago, J-Y. Girard developed a necessary condition for
the provability of constant multiplicative linear expressions:
M(one) = 1
M(bottom) = 0
M(A par B) = M(A) + M(B)
M(A tensor B) = M(A) + M(B) - 1
If a formula A is provable in multiplicative linear logic and contains
no propositions, then M(A) = 1. (In other words, the number of
tensors is one less than the number of ones in any provable constant
MLL formula.) There was a question as to whether some form of simple
"truth table" or numerical evaluation function like the above could
yield a necessary and sufficient condition for provability of constant
multiplicative expressions. The result claimed here shows that no
simple (polynomial time) evaluation function exists for constant
MLL expressions unless P=NP.
One may encode a 3-Partition problem (Where the size of each partion
is B, there are 3*M elements of sizes S1, S2, ... S3M, and
for all Si: B/4 < Si < B/2) in MLL with propositions k and c as follows
(where we use the notation "f^X" for the tensorization of X copies of
the formula f, "-o" for linear implication and "ox" for tensor.)
[(k -o c^S1) ox (k -o c^S2) ox ... ox (k -o c^S3M)] -o (k^3 -o c^B)^M
This formula is provable in MLL if and only if the corresponding
3-Partition problem is solvable. Informally, the [...] formula
encodes the size of each element "locked" by a k. The 3-Partition
problem is solvable iff one can break the "^M" tensors correctly
partitioning the [...] formulas so that three "keys" unlock a total
size of exactly B.
The result announced here is that replacing k and c with bottom in the
above formula yields a correct encoding of a 3-Partition problem in
constant-only MLL. (writing "|" for bottom)
-
[(| -o |^S1) ox (| -o |^S2) ox ... ox (| -o |^S3M)] -o (|^3 -o |^B)^M
- - - - - - - -
Using the contrapositive (A -o B === (B perp) -o (A perp)), we can
develop a "1 only" encoding: ("f~X" is the parization of X copies of f)
[(1~S1 -o 1) ox (1~S2 -o 1) ox ... ox (1~S3M -o 1)] -o (1~B -o 1~3)^M
Eliminating the "-o" in favor of par these formulas become:
[(| ox 1~S1) par (| ox 1~S2) par...par (| ox 1~S3M)] par (1~3 par |^B)^M
- - - _
Which one may see satisfies Girard's measure condition if
there are 3*M elements, and the sum of the Si's = M*B,
side conditions on the statement of 3-Partition (Garey+Johnson).
Analyzing sequents using this condition, one may show that
the "^M" tensors are analyzed "first" (lower in a sequent proof tree),
and that this is a correct encoding of 3-Partition. Note
that 3-Partition is NP-Complete in the strong sense, and thus remains
NP-Hard even when presented in unary as it is here.