search

arminbiere / kissat

MIT License
459 stars 85 forks source link

is kissat non-deterministic? #49

Closed jwaldmann closed 7 months ago

jwaldmann commented 7 months ago

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 commented 7 months ago

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 commented 7 months ago

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 commented 7 months ago 
$ kissat --help|grep seed
  --seed=0...                random seed [0]
arminbiere commented 7 months ago

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 commented 7 months ago

... 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 commented 7 months ago

Good, then I close this.