I have found that many satisfiable problems as according to the SATLIB SAT instances are infact unsatisfiable as they all contain one or more clauses that have an exact anticlause against them. For instance the below download link for SATLIB cnf clauses for 20 variables, 91 clauses - 1000 instances, all satisfiable
has the 1st file itself which has the clauses 7th and 86th as exact inverse of each other so this equation can never be unsat. I have already posted a question here regarding this but did not got any reply so farOld question on P=NP Any comments at all are really welcome as I would really like to know if Benchmark problems are still used for competitions or not as if they are then those competitions are useless indeed. So, my question is : Am I correct in determining these errors and exposing them to the public and asking for comments or not? Also are these findings any useful? I have sent few emails asking for reply from the benchmark problems website's admin but still no reply after 2 months is making me feel bad.
I could not find a proper definition oft anticlause, so I have to speculate a bit.
Two clauses of size > 1 were each literal is inverted are not a contradiction by themself. Given the clauses
1 2 3 0
-1 -2 -3 0
We can find multiple solutions that satisfy both clauses as we only need to fulfil one literal per clause. Some partial solutions are
1 -2
-1 2
2 -3
...
For these clauses wie only need to select one positiv and one negative literal.