0:00 We discuss the purpose and input format for SAT solvers
28:20 We introduce the Limboole tool and how to use it on the Formal Methods Playground https://play.formal-methods.net/?check=SAT
46:00 We encode an example in propositional logic and see how to show semantic entailment https://play.formal-methods.net/?check=SAT&p=wrath-left-abide-veal
59:06 We introduce Role-Based Access Control and develop a manual encoding in SAT to check constraints
