SATisfaction guaranteed
Or some such lame pun... Folks, this post is yet another puzzle. It should be pretty easy for anyone who knows a certain famous combinatorial Lemma (which I'll name in the comments section). To everyone else, this is a chance to rediscover that lemma, and do a little more besides; I think that, approached with pluck, it should be solvable--but not easy.
The puzzle is to give an efficient algorithm to decide satisfiability (and to produce satisfying assignments when possible) of a restricted class of boolean formulae. They are going to be k-CNFs, that is, a big AND of many ORs, each OR of k variables from {x[i]} or their negations {~x[i]}.
As stands this is NP-complete, even for k = 3. Here is the extra restriction on instances: for every subset S of k variables, there is an OR clause C[S] which contains each variable from S exactly once, possibly negated, and no other variables. (So, these SAT instances are fairly 'saturated' with constraints.)
For example, the property that a bit-vector contains at most k-1 ones can be written this way: for each variable-set S = {x[i_1], ... x[i_k]} of size k, we include the constraint
C[S] := (~x[i_1] OR ~x[i_2] OR ... OR ~x[i_k]).
That's the problem statement--get to it!
The puzzle is to give an efficient algorithm to decide satisfiability (and to produce satisfying assignments when possible) of a restricted class of boolean formulae. They are going to be k-CNFs, that is, a big AND of many ORs, each OR of k variables from {x[i]} or their negations {~x[i]}.
As stands this is NP-complete, even for k = 3. Here is the extra restriction on instances: for every subset S of k variables, there is an OR clause C[S] which contains each variable from S exactly once, possibly negated, and no other variables. (So, these SAT instances are fairly 'saturated' with constraints.)
For example, the property that a bit-vector contains at most k-1 ones can be written this way: for each variable-set S = {x[i_1], ... x[i_k]} of size k, we include the constraint
C[S] := (~x[i_1] OR ~x[i_2] OR ... OR ~x[i_k]).
That's the problem statement--get to it!
Labels: complexity, puzzles
posted by Andy D at
9:30 PM
2 Comments:
Sauer's Lemma, a cornerstone of VC dimension theory, and independently rediscovered in various settings--see Lance's post
http://weblog.fortnow.com/2006/02/sauers-lemma.html
By
Andy D, at 10:06 PM
An amusing observation:
Suppose you're not actually shown the clauses of the formula, but they are held by an adversary. You can propose an assignment to the variables, and if it doesn't satisfy the formula the adversary has to show you a violated clause (of his choice).
In this case, deciding satisfiability is NP-hard even for the Sauer-type formulae described in this post (for simple reasons).
By
Andy D, at 6:40 PM
Post a Comment
<< Home