kissat problem with larger instances

gsgs2 commented 2 months ago

Kissat had problems with some larger instances, generated by the same program as the smaller ones.

Some instances take very long time starting at about 600 variables and 1 hour running time.

I do not see this with clasp running on the same instances.

I'm using kissat 3.1.0 on Linux-Ubuntu

here the timings in seconds for 12 instances with exactly one solution and with 650 variables about 5850 clauses , 13300 literals , 1 thread :

kissat:5177,1545,440,78600,22004,260471,6520,29460,4500,2760,1440,30861

and the clasp-timings (4 threads, nondeterministic) clasp4:1600,175,1605,2507,1896,4694,2285,359,1300,1700,1483,548

it's even worse when I exclude the solution as an additional clause and let it search the whole instance to confirm that there is no solution:

kissat: 148,246,99,381,122,563,88,310,67,53,232,214 clasp4: 6,5,8,6,7,8,4,9,6,5,7,7

seconds * 1000 , including the time needed to find the solution which then is "excluded" in a 2nd run

I do not see this problem with smaller instances of the same kind. (exact-cover-problems, exactly-one-clauses)

maybe this is some bug easily to be corrected ?!

arminbiere commented 2 months ago

Can you share some instances, where this happens? Also you might want to try the new Version 4.0.0 first.

gsgs2 commented 2 months ago

430 is the one which took >72h on a ryzen9 with 5GHz

gsgs2 commented 2 months ago

ahh, I think the effect also occurs in clasp running on one thread, but not (yet) in clasp running on 4 threads. It's probably less obvious,less severe than with kissat, it's slow to test it at this level.Maybe I can post timings later.

I haven't tested it, but I assume the same problem happens with just random (regular,balanced) exact-cover problems near the phase-transition, converted to SAT-instances with exactly-one-clauses.

It now reminds me to what we called "the triangle bug" with the Hamiltonian Cycle problem. It's maybe the reason why some of the solvers have a restart-"feature". They do not detect that some small substructure (e.g. a triangle with only one exit) can never be completed.

There could be small SAT-substructures in a SAT-instance which cannot be completed to a solution but the SAT-solver doesn't detect this and evaluates all possible extensions, which takes so mch time. This happens rarely at small sizes but the probability increases at larger instances.

Here is a file with 59 random unsatisfyable "x9-" instances (s=130 stations,650 variables,520 exactly-one-clauses with 4-6 literals) http://magictour.free.fr/x9-130n.sat and the kissat-3.1.0 timings : http://magictour.free.fr/x9-130n.l1d

And btw. I think kissat should not stop when other valid instances follow in the file but should rather continue to process it. That makes it easier to test multiple instances in one run.

and ignore an end-of-file-character (ascii-26) at the end

gsgs2 commented 2 months ago

it seems that the problem is not present in kissat-4.0.0 I get 20fold increased speed in these 12 instances as compared to kissat-3.1.0. It's almost as fast on one thread as clasp-3.3.5 on 4 threads

arminbiere commented 2 months ago

Excellent! This is probably due to the new BVA (factor) code.

arminbiere / kissat