BEGIN:VCALENDAR
VERSION:2.0
PRODID:icalendar-ruby
CALSCALE:GREGORIAN
METHOD:PUBLISH
BEGIN:VTIMEZONE
TZID:Europe/Vienna
BEGIN:DAYLIGHT
DTSTART:20170326T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=3
TZNAME:CEST
END:DAYLIGHT
BEGIN:STANDARD
DTSTART:20171029T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10
TZNAME:CET
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20260428T112233Z
UID:58a2df0f4136d129982287@ist.ac.at
DTSTART:20170405T170000
DTEND:20170405T180000
DESCRIPTION:Speaker: Markus Rabe\nhosted by Tom Henzinger\nAbstract: Many o
 f the challenging problems in verification and synthesis algorithms are na
 turally phrased in terms of quantified formulas.  Our ability to solve the
 se problems\, however\, is still unsatisfactory. Even when we take a look 
 at the most basic logical theory with quantification\, quantified boolean 
 formulas (QBF)\, the most effective approach are CEGAR-style algorithms. B
 ut CEGAR is a generic algorithmic scheme\, which means that we are not yet
  able to exploit the structure of quantified problems.\n\nIn this talk I w
 ill discuss some of the fundamental limits of CEGAR-style algorithms and p
 resent a novel approach to solve quantified boolean formulas (currently re
 stricted to one quantifier alternation\, i.e. 2QBF). The algorithm adds ne
 w constraints to the formula until the constraints describe a unique Skole
 m function - or until the absence of a Skolem function is detected. Backtr
 acking is required if the absence of Skolem functions depends on the newly
  introduced constraints. The algorithm can be best understood when compare
 d to search algorithms for SAT. We will discuss how to lift propagation\, 
 decisions\, and conflicts from values (SAT) to Skolem functions (QBF). The
  algorithm significantly improves over the state of the art in terms of th
 e number of solved instances\, solving time\, and the size of certificates
 .
LOCATION:Mondi Seminar Room 2\, Central Building\, ISTA
ORGANIZER:abonvent@ist.ac.at
SUMMARY:Markus Rabe: A New Approach to Quantified Boolean Formulas
URL:https://talks-calendar.ista.ac.at/events/406
END:VEVENT
END:VCALENDAR