Stream: new members
Topic: SAT in Lean
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.
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?
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.
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