=Paper=
{{Paper
|id=Vol-2396/tutorial1
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-2396/tutorial1.pdf
|volume=Vol-2396
|dblpUrl=https://dblp.org/rec/conf/cilc/Dovier19
}}
==None==
<pdf width="1500px">https://ceur-ws.org/Vol-2396/tutorial1.pdf</pdf>
<pre>
The SATisfiability problem and its impact

                           Agostino Dovier

        Dept. of Mathematics, Computer Science, and Physics,
                        University of Udine
                    agostino.dovier@uniud.it



Abstract. The tutorial will deal with the problem of establishing the
satisfiability of a propositional logical formula (in short, SAT). Its im-
portance will be investigated both theoretically and practically.
As far as the importance in theoretical computer science and mathemat-
ics are concerned, the role of SAT in the P-vs-NP problem (one among
the 7 Millennium Problems listed by the Clay Mathematics Institute)
will be clarified.
On the practical side, a brief history of the main computational tech-
niques for solving it will be presented. The impact of SAT in real life
applications will be highlighted by showing that any NP problem can be
reduced to it, and therefore, worked out by exploiting the efficiency of
modern SAT solvers.
The talk will be concluded by recalling a logic programming language
with the same expressivity of SAT.

</pre>