Comments (9)
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.
from sat3.
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.
from sat3.
Vladimir Romanov confirmed that his own implementation also built non-empty HSS for x1_16.shuffled.cnf
from sat3.
Are you guys working on any solution to this problem, or is it a done deal?
from sat3.
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.
from sat3.
It's August 21, more than 3 months (1/4 of a year) after this bug was discovered. Any progress?
from sat3.
@pete6 I don't know, I haven't discussed this with Vladimir Romanov since that time.
from sat3.
You definitely should. Proving P=NP will make you McMillionares!!!!!
from sat3.
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.
from sat3.
Related Issues (5)
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from sat3.