Re: X3SAT Question




"RickO" <ricko137@xxxxxxxxx> wrote in message
news:1131813177.935259.71830@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
Russell Easterly schrieb:

I have been studying the exclusive 3SAT problem (X3SAT),
also known as the 1 in 3 SAT problem.
Given a collection of clauses, where each clause contains
exactly three literals, is there a set of literals such that
each clause contains exactly one member from the set?

I am particularly interested in "reduced" X3SAT instances.
There are reduction rules that guarantee that, in a reduced instance,
no two clauses share more than one variable in common.

For simplicity, I am looking at instances that don't contain
any negated variables. It is well known that X3SAT is NP-Complete
even when there are no negated variables.

I want to find an unsatisfiable reduced X3SAT instance.
I can't prove that all unnegated reduced X3SAT instances are solvable,
but I haven't yet been able to prove that they aren't always solvable,
either.

It should be simple to prove they aren't always solvable.
Just produce a reduced X3SAT instance that is unsatisfiable.
But, I haven't been able to come up with such an instance.
I would appreciate any help finding such an instance.

The instance should have the following properties:

1) No variable is negated.
2) No two clauses share more than one variable in common.
3) The instance is unsatisfiable.

This is an example of an instance that meets the first two criteria:

(a,b,c)(a,d,e)(b,d,f)(c,e,f)

The set (a,f) is one of the many solutions to this instance.

Coming up with an unsatisfiable reduced X2SAT instance is easy:
(a,b)(b,c)(a,c) in unsatisfiable.

Again, any help will be appreciated.


Russell
- 2 many 2 count

Hi Russel
Try (a,b,c)(a,d,e)(a,f,g)(b,d,f)(c,e,g)(b,g,h)(c,d,h)

Unless I messed up (what? me make a mistake :) this shouldn't be
satisfiable.

Argument:
To satisfy (a,b,c) a, b or c must be true
a true: then b,c,d,f,g must be false. So (b,d,f) is false
b true: then a,c,d,f,g,h must be false. So (a,d,e) forces e to be true,
and therefore g is false. But then (a,f,g) is false
c true: then a,b,d,e,g,h must be false. So (a,d,e) is false

Hope this helps.



Thanks once again.
This did help.

You might be interested to know that your expression
can be shortened. The last clause is not needed:

(a,b,c)(a,d,e)(a,f,g)(b,d,f)(c,e,g)(b,g,h)
n=8, m=6 (n=# of literals, m=# of clauses)

The expression above is unsatisfiable.

These are some of the shortest unsolvable
X3SAT expressions I have found so far:

Allowing literals and their negation:
(a,b,c)(~a,b,c) n=4, m=2 (n = # of literals, m = # of clauses)

Only allowing pure literals:
(a,b,c)(a,b,d)(a,c,d)(b,c,d) n=4, m=4

The graph for this example forms a tetradedron.

This still doesn't satisfy the conditions I asked for.
I wanted clauses where no two clauses share more
than one literal in common.

This requirement is equivalent to the following reduction rule:
Given two clauses, (a,b,c) and (a,b,d), we know d=c.
Replace every occurrence of d with c and delete redundant clauses.

Applying this rule to the tetrahedron we get:
(a,b,c)(a,b,d)(a,c,d)(b,c,d) n=4, m=4
d=c
(a,b,c)(a,b,c)(a,c,c)(b,c,c) n=4, m=4
(a,b,c)(a,c,c)(b,c,c) n=3, m=3
(a,c,c) -> a=T and c=F
(b,c,c) -> b=T and c=F
Substituting T and F:
(T,T,F)(T,F,F)(T,F,F)

The clause (T,T,F) means the instance is unsatisfiable.

The shortest expression meeting my requirements that I
have found so far is the example RickO's came up with
that uses only 8 literals and 6 clauses.
(a,b,c)(a,d,e)(a,f,g)(b,d,f)(c,e,g)(b,g,h) n=8, m=6

We can use a simple counting argument to prove
this expression is unsolvable.

Let each literal be represented by a vertex in a graph.
Assume there is an edge connecting any two literals
that appear together in a clause.
Assign a weight to each vertex equal to the number
of times this literal appears in the instance.
This is equal to d/2 where d is the degree of the vertex.
The X3SAT instance is solvable when all of the
following conditions are true.

1) There exists an Independent Set (IS) such that the sum of
weights of this set equals m, the number of clauses.

2) This IS is a maximal IS. This means no more vertices can
be added to the set and the set still be independent.

3) The Vertex Cover (VC) is the set of vertices not in the IS.
The sum of weights of vertices in the VC must equal 2m.

4) The VC must contain exactly one edge from each clause.


Given the expression:
(a,b,c)(a,d,e)(a,f,g)(b,d,f)(c,e,g)(b,g,h)

Count the number of times each literal occurs:
a(3)
b(3)
c(2)
d(2)
e(2)
f(2)
g(3)
h(1)

Find all the neighbors for each vertex.
A literal is a neighbor of another literal
if they appear together in a clause.
Sum the weights of vertices in the neighbor set:

Vertex / Neighbor Set (sum of weights)
a(3) / bcdefg (14)
b(3) / acdfgh (13)
c(2) / abeg (11)
d(2) / abef (10)
e(2) / acdg (10)
f(2) / abdg (11)
g(3) / abcefh (13)
h(1) / bg (6)

We have an instance with six clauses.
We want to find an IS that sums to 6,
and a VC that sums to 12.

If a vertex is in an IS,
it's neighbor set must be in the VC.

We see that vertices a, b, and g
can't be in any satisfying assignment
because their neighbor sets are too
large to be in the VC (bigger than 12).

We can remove the the rows for a, b, and g and
add "abg" to the neighbor sets of the remaining vertices.

Add up the sum of weights in the expanded neighbor sets:

c(2) / abeg (11)
d(2) / abefg (13)
e(2) / abcdg (13)
f(2) / abdg (11)
h(1) / abg (9)
Now, we can prove that d and e can't be in any solution.
Add "de" to the remaining neighbor sets.

c(2) / abdeg (13)
f(2) / abdeg (13)
h(1) / abdeg (13)
No vertex is in a satisfying assignment.
The instance is unsolvable.

I give a complete set of reductions rules at:
http://home.comcast.net/~logiclab/X3SAT2IS.htm


Russell
- 2 many 2 count


.



Relevant Pages

  • Re: Like
    ... those look like WHERE clauses. ... summarized values. ... Doug Steele, Microsoft Access MVP ... (no e-mails, please!) ...
    (microsoft.public.access.queries)
  • Re: Combine SQL statement
    ... --case the parts of the WHERE clauses that were differente from to 0 or 1 ... select sum(case when (Lastmodified IS NOT NULL AND Dateinitiated IS NOT ... >> AMB ...
    (microsoft.public.sqlserver.programming)
  • Re: Like
    ... those look like WHERE clauses. ... summarized values. ... usenet at dfenton dot com http://www.dfenton.com/DFA/ ...
    (microsoft.public.access.queries)