Zulip Chat Archive

Stream: new members

Topic: SAT in Lean


view this post on Zulip Vaibhav Karve (Feb 04 2020 at 20:08):

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.

view this post on Zulip Kevin Buzzard (Feb 04 2020 at 20:18):

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?

view this post on Zulip Vaibhav Karve (Feb 04 2020 at 20:20):

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.

view this post on Zulip Kevin Buzzard (Feb 04 2020 at 20:22):

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.


Last updated: May 08 2021 at 10:12 UTC