search

msoos / cryptominisat

An advanced SAT solver
https://www.msoos.org
Other
817 stars 181 forks source link

Does CMS classify clauses? #678

Closed Geremia closed 2 years ago

Geremia commented 2 years ago

@msoos

§1.19 "Classes of easy expressions", Handbook of Satisfiability (2nd ed.) pp. 27-32, mentions the following classes of expressions:

Does CMS classify clauses? Is this shown in its output somewhere?

msoos commented 2 years ago

No it does not do any of that. No SAT solver I know of does that. Looking forward to the pull requests that will support them!

Geremia commented 2 years ago

@msoos I see kissat has "autarky reasoning".

Handbook of Satisfiability says they're simple algorithms to determine many of these classes.

msoos commented 2 years ago

That's great! Please create the respective pull request so CryptoMiniSat could do it too!