schep wrote:
I only mentioned expression length because I wasn't sure what's normally meant by calling satisfiability non-polynomial (in what variable?)
If you're talking about whether a problem is polynomial solvable, that typically means that the computation needed to find the solution is proportional to (actually, bounded by) a polynomial in terms of the length of the problem's formulation (often called the "
input"
). The length of the input depends on how it's encoded, but when you're talking abut polynomial versus non-polynomial there are usually a wide variety of encodings that more or less give you the same answer. So for satisfiability, you could roughly state that it's
verifiable in polynomial time in terms of
the number of terms in the expression, but not
solvable in polynomial time. (The "
solvable"
part is not strictly proven, but is widely believed to be true.)
As a point of trivia, in computer theory the satisfiability problem is typically limited to three variables per term. This isn't a serious limitation, though, since a problem with more variables in a term can be converted to one of the proper form that's roughly a comparable size. This proper form is called 3-SAT, and that is used instead of 2-SAT because the same conversion is not necessarily possible for 2-SAT. (In fact, 2-SAT is known to be polynomially solvable.)
Edit: Incidentally, the expression (A or not B) and (B or not C) and (not A or C) and (not A or not B or not C) is in fact satisfiable (by setting all variables to false) and your example hold shows the solution at level start. But the hold is a good representation of the expression, and gives a good idea of how it works.
____________________________
I was charged with conspiracy to commit jay-walking, and accessory to changing lanes without signaling after the fact
.
++Adam H. Peterson
[Last edited by AlefBet at 08-08-2005 05:25 PM]
