kissat problem with larger instances

[gsgs2]

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]

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

[gsgs2]

I found kissat 4.0.0 at
http://github.com/arminbiere/kissat/releases/download/rel-4.0.0/kissat-4.0.0-linux-amd64.zip
it takes 33min on 211.sat which took 440 sec with kissat 3.1
I uploaded the 12 instances with the timings above (in this order) to
http://magictour.free.fr/003.sat
http://magictour.free.fr/117.sat
http://magictour.free.fr/211.sat
http://magictour.free.fr/421.sat
http://magictour.free.fr/040.sat
http://magictour.free.fr/430.sat
http://magictour.free.fr/246.sat
http://magictour.free.fr/187.sat
http://magictour.free.fr/200.sat
http://magictour.free.fr/621.sat
http://magictour.free.fr/730.sat
http://magictour.free.fr/733.sat

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

[gsgs2]

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]

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]

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

[gsgs2]

seconds spent on the 40 sterten instances
by the 14 solvers of the main_track in the 2024-SAT-competition
these are made from Hamiltonian-Cycle-problems
as exact-cover-problems

7745 ,kissat-sc2024
20739 ,hKis-bva
25370 ,AMSAT
25770 ,AMSAT_RGC
27643 ,BreakID-Kissat
30864 ,Cadical_ESA
32677 ,hCaD-bva
39816 ,Kissat_MAB_ESA
41369 ,Kissat_MAB_Binary
41627 ,hCaD-pbva
59343 ,Kissat_MAB-DC
64469 ,CaDiCaL
87108 ,hKis-pbva
272756 ,IsaSAT

as we have seen above, kissat 3.1.0 had also
problems with the larger ones of these instances