Tata Institute of Fundamental Research
Building strategies into QBF proofs
STCS Colloquium
Speaker:
Meena Mahajan (The Institute of Mathematical Sciences
CIT Campus, Chennai)
Organiser:
Prahladh Harsha
Date:
Friday, 15 Feb 2019, 15:30 to 16:30
Venue:
A-201 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
Quantified Boolean Formulas (QBF) are a natural extension of the SAT problem, with more sophisticated semantics: functions witnessing the truth of a QBF can be interpreted as strategies in a two-player game. A lot has been written regarding the extraction of strategies from QBF proofs, in various proof systems. Here we devise a new system - Merge Resolution - in which strategies are built explicitly within the proofs themselves. We investigate some advantages of Merge Resolution over existing systems; in particular, we find that it lifts naturally to DQBF, a further extension of QBF.
Joint work with Olaf Beyersdorff and Joshua Blinkhorn. To appear in STACS 2019.
| Speaker: | Meena Mahajan (The Institute of Mathematical Sciences CIT Campus, Chennai) |
| Organiser: | Prahladh Harsha |
| Date: | Friday, 15 Feb 2019, 15:30 to 16:30 |
| Venue: | A-201 (STCS Seminar Room) |
(Scan to add to calendar)
Abstract:
Quantified Boolean Formulas (QBF) are a natural extension of the SAT problem, with more sophisticated semantics: functions witnessing the truth of a QBF can be interpreted as strategies in a two-player game. A lot has been written regarding the extraction of strategies from QBF proofs, in various proof systems. Here we devise a new system - Merge Resolution - in which strategies are built explicitly within the proofs themselves. We investigate some advantages of Merge Resolution over existing systems; in particular, we find that it lifts naturally to DQBF, a further extension of QBF.
Joint work with Olaf Beyersdorff and Joshua Blinkhorn. To appear in STACS 2019.
Joint work with Olaf Beyersdorff and Joshua Blinkhorn. To appear in STACS 2019.