[Proof Complexity] MIAO seminar Fri Jan 12 at 14:00 CET with Ning Luo: Proving UNSAT in zero knowledge

[Jakob Nordström]

Dear all,

As we prepare for the holidays, this is just to let you know that after New Year's the MIAO seminars will resume operation on Friday January 12 at 14:00 CET. We will then have the pleasure of listening to a talk by Ning Luo from Northwestern University titled "Proving UNSAT in zero knowledge". You find the abstract at the bottom of this message.

This will be a video seminar at https://lu-se.zoom.us/j/61925271827. Please feel free to share this information with colleagues who you think might be interested. We are also hoping to record the seminar and post on the MIAO Research YouTube channel https://youtube.com/@MIAOresearch for people who would like to hear the talk but cannot attend.

Most of our seminars consist of two parts: first a 50-55-minute regular talk, and then after a break a ca-1-hour in-depth technical presentation with (hopefully) a lot of interaction. The intention is that the first part of the seminar will give all listeners a self-contained overview of some exciting research results, and after the break people who have the time and interest will get an opportunity to really get into the technical details. (However, for those who feel that the first part was enough, it is perfectly fine to just discretely drop out during the break. No questions asked; no excuses needed.)

More information about upcoming MIAO seminars can be found at http://www.jakobnordstrom.se/miao-seminars/. In particular, note that tomorrow Tuesday we have our last seminar for the autumn semester titled "Top-down lower bounds for depth-4 circuits" with Anastasia Sofronova from EPFL.

And since it is that time of the year, let me also say that I would be most grateful for any help in spreading information about some current openings in Copenhagen and Lund, namely:
- Postdoc positions in Copenhagen in TCS with deadline January 10: http://www.jakobnordstrom.se/openings/Postdoc-UCPH-240110.html
- PhD positions in Copenhagen in TCS and/or combinatorial optimization with deadline January 10: http://www.jakobnordstrom.se/openings/PhD-UCPH-240110.html
- A tenure-track assistant professorship in Lund with a focus on logic and automated reasoning with deadline January 26: http://www.jakobnordstrom.se/openings/AsstProf-Lund-240126.html
- And also postdoc and PhD positions in Lund, which should be posted in late 2023 or early 2024: https://derezende.github.io/openpositions/

If you do not wish to receive these announcements, or receive several copies of them, please send a message to jn at di.ku.dk.

Best regards,
Jakob Nordström

**********

Friday Jan 12 at 14:00 CET on Zoom
Proving UNSAT in zero knowledge
(Ning Luo, Northwestern University)

Zero-Knowledge (ZK) protocols have been extensively researched in recent years, with a focus on finding efficient protocols for problems in NP, such as proving the satisfiability of a Boolean formula. However, less attention has been given to proving the unsatisfiability of a given formula without revealing any related proofs or even the formula itself. In this talk, I will talk about our work on a highly efficient zero-knowledge protocol for proving the unsatisfiability of Boolean formulas in propositional logic. Our protocol is based on polynomial equivalence checking, which allows for the verification of a resolution proof of unsatisfiability in a zero-knowledge setting. We have implemented this protocol and have demonstrated its effectiveness by checking the unsatisfiability of real-world formulae used for verifying system drivers within just 300 seconds. This work was published in CCS 2022 and was awarded a distinguished paper award. In addition, I will talk about our recent progress that extended the ZKUNSAT framework to handle SMT formulas.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +46 70 742 21 98
http://www.jakobnordstrom.se