BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Liverpool Computer Science Seminar System//v2//EN
BEGIN:VEVENT
DTSTAMP:20260920T212525Z
UID:Seminar-pizza-1181@lxserverM.csc.liv.ac.uk
ORGANIZER:CN=Qiyi Tang:MAILTO:Qiyi.Tang@liverpool.ac.uk
DTSTART:20240202T140000
DTEND:20240202T150000
SUMMARY:Friday Lunch and Talk Series
DESCRIPTION:Dr Friedrich Slivovsky: From SAT to QBF Solving\n\nPropositional satisfiability (SAT) is the canonical NP-complete decision problem. Despite its theoretical hardness, there has been significant progress in practical solving, and SAT solvers have become a standard tool in areas such as formal methods and electronic design automation. However, the increasing complexity of specifications in these domains can lead to prohibitively large encodings that are unmanageable for even the most efficient SAT solvers. This challenge has prompted research into more succinct logics, such as Quantified Boolean Formulas (QBF), which extend propositional logic with universal and existential quantification over the Boolean domain. This talk will provide an introduction to SAT solving and an overview of the current state of QBF solving, including challenges and future research directions.\n\nhttps://www.csc.liv.ac.uk/research/seminars/abstract.php?id=1181
LOCATION:
END:VEVENT
END:VCALENDAR