SAT in Lean

Stream: new members

[Vaibhav Karve]

I did some searches on both the Lean as well as Mathlib repos for "SAT" (aka boolean satisfiability) and "CNF" (aka Conjunctive Normal Form). However, I came up empty handed. Are sat/unsat/cnfs/clauses not already defined in Lean?

I was surprised because I know that several people in the community work on SAT-related questions.

[Kevin Buzzard]

I don't know if "SAT" is explicitly mentioned in the source code but sure you can write statements in CNF in Lean. What in particular do you want to know about these things / do with them? Are there theorems you want to prove about such things?

[Vaibhav Karve]

Yes, just basic stuff. Want to be able to write theorems about the class of all (un)satisfiable CNFs etc. I will get to work defining these. Just wanted to make sure that I am not duplicating effort in case these already exist in the Lean library.

[Kevin Buzzard]

I guess I only really know about Lean's maths library, you probably want to speak to a computer scientist about this. I guess Lean doesn't know whether a general proposition is in CNF so I suppose you have to start by implementing your own little theory of and and or etc. But I should shut up really and let someone who knows what's going on chime in.