BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.39.1//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:d3ce4cc4-4d6e-4bf8-8223-5538abf3335c
X-WR-CALNAME:[MTV] Philipp Czerner (TUM) - Making IP = PSPACE Practical: Ef
ficient Interactive Protocols for BDD Algorithms
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
BEGIN:STANDARD
TZNAME:CET
DTSTART:20231029T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20241027T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20230326T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20240331T020000
RDATE:20250330T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:d3ce4cc4-4d6e-4bf8-8223-5538abf3335c
DTSTAMP:20241010T164855Z
CLASS:PUBLIC
DESCRIPTION:We show that interactive protocols between a prover and a verif
ier\, a well-known tool of complexity theory\, can be used in practice to
certify the correctness of automated reasoning tools.\n\nTheoretically\, i
nteractive protocols exist for all PSPACE problems. The verifier of a prot
ocol checks the proverâ€™s answer to a problem instance in probabilistic pol
ynomial time\, with polynomially many bits of communication\, and with exp
onentially small probability of error. (The prover may need exponential ti
me.) Existing interactive protocols are not used in practice because their
provers use naive algorithms\, inefficient even for small instances\, tha
t are incompatible with practical implementations of automated reasoning.
\n\nWe bridge the gap between theory and practice by means of an interacti
ve protocol whose prover uses BDDs. We consider the problem of counting th
e number of assignments to a QBF instance (#CP)\, which has a natural BDD-
based algorithm. We give an interactive protocol for #CP whose prover is i
mplemented on top of an extended BDD library. The prover has only a linear
overhead in computation time over the natural algorithm.\n\nWe have imple
mented our protocol in blic\, a certifying tool for #CP. Experiments on st
andard QBF benchmarks show that blic is competitive with state-of-the-art
QBF-solvers. The run time of the verifier is negligible\, and the error pr
obability is less than one millionth of a percent (and can easily be reduc
ed further).\n
DTSTART;TZID=Europe/Paris:20240215T130000
DTEND;TZID=Europe/Paris:20240215T140000
LOCATION:salle 178\, zoom: https://bordeaux-inp-fr.zoom.us/j/89508306159
SEQUENCE:0
SUMMARY:[MTV] Philipp Czerner (TUM) - Making IP = PSPACE Practical: Efficie
nt Interactive Protocols for BDD Algorithms
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR