mSAT
mSAT copied to clipboard
Gbury
A modular sat/smt solver with proof output.
I want to use mSAT to solve (a lot of) quite small CNFs (~40 variables), but I want to get non-deterministic solutions (e.g. a uniform pick from the set of...
on pigeon/hole9.cnf it's quite clear. possibly caused by the bitfield for polarity saving that might be erased when we clear the whole bitfield (even though the default polarity might be...
- use a bool flag in the variable to save last phase - use `false` by default (corresponds to this flag being cleared)
Currently coq proof can be quite slow (and even fail to check within reasonable time/memory). One solution would be to change the structure of coq output from a srie of...
Hi, Commit ab4d1cbec98bd3bc92e6833d08999853eea7dc95 solves an annoying issue where Msat_tseitin sometimes fails to put into CNF formulas such as `Not (True True)`. It is however not included in the current opam...
