LeanSAT is a collection of utilities for SAT work. This includes:
- Encoding utilities
- Solver APIs
- Printers and parsers for common file formats
This repository is an active research code base using the
Research Codebase Manifesto,
and the core library (in LeanSAT/) is not very stable yet.
We would love to hear from any projects using LeanSAT! Contact @JamesGallicchio by email or mastodon.
Add the following to your project's lakefile:
require «lean-sat» from git
"https://github.com/JamesGallicchio/LeanSAT" @ "main"
Then import LeanSAT will import everything in the library.
Everything in the library is under the LeanSAT namespace,
so we generally assume you have open LeanSAT at the top of your files.
Important types:
PropFun: The mathematical model of a propositional formula. TwoPropFuns are equal iff they have the same interpretation under all assignments.EncCNF: The encoding monad. This monad allows you to build up a CNF via do-notation. SeeExamples/Encodingfor example usage.VEncCNF: Verified encoding. Similar toEncCNF, constrained to provably encode some predicate over assignments. This connectsEncCNFto thePropFunmath model.Solver,Solver.ModelCount,Solver.ModelSample: Solver interfaces. These are each typeclasses. The idea is that you should have aninstanceof theSolvertypeclass in scope when you go to solve a CNF formula. SeeExamples/Cadical.leanfor how to declare a solver instance.
TODO(JG): describe available notation for PropFun, PropForm
- Support (verified?) encoding to non-CNF formulas (KNF, d-DNNF, XOR-CNF, ...)
- Add verified checkers for sat certificates
- Add verified model counting
- Add verified pre-processing
This project is licensed under the Apache 2.0 license (see LICENSE). If you want to use the library but need it to be released under different terms, please contact us or open an issue.
PRs are welcome and appreciated. That said, because the repository is quite unstable, please open an issue or comment on an existing one to let us know what you are working on!
@vtec234 @ccodel @JamesGallicchio