科技回声

why is it so common to talk about how SAT-solvers work _inside_, but there's almost no texts about how to work *with* them?<p>with all respect to Knuth's volume 4b (which felt like the only congregating text even touching the subject, when I looked into it some years ago) - but even his work doesn't go into loads of nooks and crannies of SAT encodings that gave invaluable speedups in specific contexts, so are useful as "ideas" - not as recipies<p>(and Knuth's descriptions of counters' encodings would've been greatly improved by pictures, imo)

I'd love an article like this enumerating and explaining all the different techniques used, instead of just dumping them there. I don't mean CDCL, that is explained everywhere. I mean more advanced stuff like all the preprocessing and inprocessing techniques (e.g. bounded clause elimination), how to apply them efficiently, how to collaborate with a local search based solver (e.g. walksat), stuff like that.

I remember putting together a bibliography about standard techniques a few years ago: <a href="https://arxiv.org/abs/1802.05159" rel="nofollow">https://arxiv.org/abs/1802.05159</a>

The majority of this article is scratch notes. How is this getting upvotes?

Any suggestions for a good parallel open source SMT solver? It seems to me like contests are full of documentation-less entries that are setup to just run the contests and may or may not be generally usable.

I remember putting together a bibliography about standard techniques a few years ago: <a href="https://arxiv.org/abs/1802.05159" rel="nofollow">https://arxiv.org/abs/1802.05159</a>

The majority of this article is scratch notes. How is this getting upvotes?

SAT Solver Etudes I

5 条评论

SAT Solver Etudes I

5 条评论