is kissat non-deterministic?

[jwaldmann]

The following may sound a bit strange, but ...

I think kissat (3.1.1) found a model for a CNF (roughly 200k vars, 1m clauses), using --sat --quiet 1, after perhaps 15 min, but I am unable to reproduce it, in several tries, giving more than 1 hour each. So - was I hallucinating? Or was kissat just lucky?

The --help text includes

  --sat      target satisfiable instances ('--target=2 --restartint=50')
  --target=0..2              target phases (1=stable,2=focused) [1]
  --randec=<bool>            random decisions [true]
  --randecstable=<bool>      random decisions in stable mode [false]
  --randecfocused=<bool>     random decisions in focused mode [true]

meaing that it was random?

Assuming yes: what's the best strategy to find a model (again)? Just run repeatedly, with timeout? Or run once, without timeout? (of course I will try both.)

[arminbiere]

It should be deterministic across machines, operating systems and configurations. Well there is one issue if the file has options in it and you have compiled with --embedded which is default for debugging (-g) and some other configurations. In the default configuration these options in DIMACS files are ignored though and then you get strange Heisenbugs for the debugging configuration. Otherwise this could be also a hardware glitch.

[jwaldmann]

interesting, and confirmed by: kissat --sat --decisions=1000000 my.cnf several times where statistics (printed at the end) are identical (e.g., number of propagations).

then what is the meaning of "random" in the options descriptions I cited? is it "deterministic pseudo-random"? where does the seed come from?

"hardware glitch" - ah. where can I buy more of these ... I am pretty sure the model was correct (my application is like a bitblasting SMT solver, and it did check the model after conversion from bits).

[arminbiere]

$ kissat --help|grep seed
  --seed=0...                random seed [0]

[arminbiere]

Probably I should also add a --thanks=<string-hashed-to-seed>, e.g., --thanks=bad\ mood which then as in Vampire prints at the end

s UNSATISFIABLE
c thanks to bad mood

[jwaldmann]

... meanwhile, I did rediscover the "lost" model. There were several moving parts (different machines, different kissat versions, changes in my bit-blaster)

https://git.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/blob/master/proof/Standard/Gebhardt/13.log (arctic matrix interpretation, encoding/method see https://doi.org/10.29007/qqvt , now solving an open problem. You read it here first!)

[arminbiere]

Good, then I close this.