Non-empty HSS for UNSAT instance has been built

[dmitrygusev]

We have found several examples where non-empty HSS for UNSAT instances was built. This shouldn't happen according to Theorem 1 (assuming its correct). Here are the instances:

• (sat-2002-beta\submitted\zhang-lintao\xor-chain\x1_16.shuffled.cnf) from SAT Competition 2002 Benchmark
• http://logic.pdmi.ras.ru/~hirsch/benchmarks/hgen8-n260-01-S1597732451.shuffled-as.sat03-885.cnf

Until someone find an error in Theorem 1 we consider this is a bug in implementation.

[Tesseractic]

Please ask Vladimir Romanov to run these instances on his own implementation of the algorithm. If Romanov's implementation fails on these as well, it would seem more likely that there's a basic problem with the approach. On the other hand, if his program succeeds for these instances, we can have a little more confidence in the paper.

[dmitrygusev]

It works on Romanov's implementation as it supposed to, the formula classified as UNSAT. I've just tried to run the test case with x1_16.shuffled.cnf.

Though Romanov's own implementation doesn't write complete log about what its doing. And I'm not familiar with its code enough to investigate whether the HS was built empty. I will ask him to verify this example by himself.

Our implementation also classifies these formulas as UNSAT, because while its searching satisfying set it reduces HS to elementary HS (this is also polynomial-time operation), and if the formula is SAT this will lead to satisfying set. If it won't be able to reduce HS to elementary one it will throw an EmptyStructureException - which will be interpreted in our implementation as UNSAT.

So the answer is still correct, though during finding the solution we have some contradiction to the theory.

[dmitrygusev]

Vladimir Romanov confirmed that his own implementation also built non-empty HSS for x1_16.shuffled.cnf

[realazthat]

Are you guys working on any solution to this problem, or is it a done deal?

[dmitrygusev]

It is more likely that the issue is not in the implementation, but in the filtration procedure as its defined in the article (http://romvf.wordpress.com/2011/01/19/open-letter/#comment-99):
"A shortcoming possibly exists in the filtration procedure which requires an amendment."

I know Vladimir Romanov works on this.

As for the implementation, I don't think I'll do any commits for this issue until we release a new version of the article where the fix will be introduced.

P.S.
I also tried to understand the structure of x1_16.shuffled.cnf and here is what I got (thanks to Luigi Salemi):

   ( 1 Xor  2 Xor 33)
   ( 1 Xor 22 Xor 40)
   ( 2 Xor  7 Xor 24)
   ( 3 Xor 18 Xor 35)
   ( 3 Xor 26 Xor 34)
   ( 4 Xor 17 Xor 44)
   ( 4 Xor 21 Xor 31)
   ( 5 Xor 13 Xor 16)
Not( 5 Xor 30 Xor 36)
   ( 6 Xor 27 Xor 35)
Not( 6 Xor 32 Xor 42)
   ( 7 Xor 17 Xor 43)
Not( 8 Xor 25 Xor 29)
   ( 8 Xor 37 Xor 42)
Not( 9 Xor 15 Xor 46)
   (-9 Or -16 Or  47)   ; CNF
   (-9 Or -16 Or -47)   ; CNF
   ( 9 Or  16 Or  48)   ; CNF
   ( 9 Or  16 Or -48)   ; CNF
   (10 Xor 12 Xor 41)
Not(10 Xor 32 Xor 33)
Not(11 Xor 14 Xor 39)
Not(11 Xor 15 Xor 34)
Not(12 Xor 20 Xor 30)
Not(13 Xor 14 Xor 24)
Not(18 Xor 22 Xor 43)
Not(19 Xor 20 Xor 38)
Not(19 Xor 21 Xor 31)
Not(23 Xor 26 Xor 44)
Not(23 Xor 27 Xor 28)
Not(25 Xor 37 Xor 40)
   (28 Xor 36 Xor 39)
   (29 Xor 38 Xor 45)
Not(41 Xor 45 Xor 46)

Every variable presents exactly in 8 clauses (in CNF) except for two irrelevant variables: 47 and 48 that were added to complete the formula to 3-SAT.

I also want to find smaller instance built with the same construction rules that will reproduce this issue, but I really don't have enough time for this right now.

[pete6]

It's August 21, more than 3 months (1/4 of a year) after this bug was discovered. Any progress?

[dmitrygusev]

@pete6 I don't know, I haven't discussed this with Vladimir Romanov since that time.

[pete6]

You definitely should. Proving P=NP will make you McMillionares!!!!!

[dmitrygusev]

Publication with the new version of this algorithm has been published today:

http://romvf.wordpress.com/2013/09/25/development-of-the-concept/

It is much simpler now (no more hyperstructures) and the part that caused this issue is now absent.

This issue will remain open, because it still applied to the previous publication.