Automated Reasoning: satisfiability

This course introduces the foundations of satisfiability (SAT), one of the most important problems in computer science and automated reasoning. You will explore how logical formulas can be represented and analysed, and how SAT solvers are used to determine whether a set of logical constraints can be satisfied. The course covers both theoretical concepts and practical applications, demonstrating how SAT techniques are used in fields such as software verification, artificial intelligence, planning, and optimization. 

What you will learn:

• Fundamentals of propositional logic and satisfiability problems.  
• Representation of logical formulas in conjunctive normal form (CNF).  
• Core algorithms and techniques used by modern SAT solvers.  
• Methods for solving complex constraint satisfaction and decision problems.  
• Applications of SAT in verification, planning, scheduling, and artificial intelligence.  
• The role of SAT solving in automated reasoning and formal methods. 

Follow the ‘go to course’ and sign up!