A Brief Introduction to SAT Solving

Luogo: Dipartimento di Matematica, via Sommarive, 14 - Povo (TN) - Aula Seminari "-1"
Ore: 16.00 

• Relatore: Roberto Sebastiani (Università degli Studi di Trento - DISI)

Abstract:
Propositional Satisfiability (SAT) is the problem of deciding the satisfiability of a Boolean formula. The ability of efficiently reasoning with Boolean values and operators is a core feature of many applications in various fields of Artificial Intelligence, Formal Verification and Digital Electronics, including, e.g., Automated Reasoning and Planning, Formal verification of Hardware and Software devices, Knowledge Representation and Reasoning. This brief tutorial aims at providing an overview of the state-of-the-art SAT solving techniques.

Prerequisites: a basic knowledge in Propositional (Boolean) logic is assumed.

Referente: Massimiliano Sala