In complexity theory, it is well known that IP = PSPACE (Shamir's Theorem). It is not hard to see why IP is contained in PSPACE, so it suffices to show that PSPACE is contained in IP, which is done by constructing an interactive proof for TQBF (IP is closed under polynomial-time Karp reductions). This project contains an implementation of the above mentioned interactive proof protocol for TQBF presented in Shamir's paper, with the use of the linearization operator introduced by Shen in this paper. For example, this project can be used to obtain a concrete interactive transcript of the communication between the prover and the verifier (see below for more details).
Apart from the implementation of the protocol itself, this project contains a clean, detailed & generic renderer of a video animation for the entire protocol. The goal of this animation is to visualize how exactly everything works in the protocol, both before as well as during the communication. Concretely, the following stages are animated:
- Arithmetization, that is, the conversion of the QBF matrix into a polynomial
- Communication between the prover and the verifier, that is, how the prover shows the validity of the QBF sentence and how the verifier interactively checks that the proof being presented is indeed correct.
Overall, this project is intended to be used for educational purposes. See this blog post for a clear description of the protocol, the visualizations generated using this project, the relevant notation and details.
Python version: 3.9.5 or newer
Required python dependencies:
For the installation of the above libraries, make sure you follow the official guide available on the corresponding website. The Manim CE library is used only for the animation rendering, you don't have to install it if you are not planning to render animations.
To execute the interactive protocol, run
python tqbfip.py [seed]in the src directory. Here, by replacing [seed] with some integer, it is possible to adjust the verifier's random number generator seed. This is useful when we want to execute the protocol multiple times without having the numbers the verifier chooses at random change every time. In case this parameter is omitted, a default hardcoded seed will be used.
By default, the protocol will be executed for the formula generated by default_example_formula() in src/formulas.py. To execute the protocol for a custom QBF sentence, construct it using the QBF class and pass it as an argument to tqbfip(qbf, seed). You can find examples of formulas and the way they can be constructed in src/formulas.py. Please note that the QBF class supports only formulas already in prenex normal form with matrix in CNF. If this is not the case for your formula, first convert it into NNF, then bring quantifiers out and finally apply Tseitin's transformation to ensure that the matrix is in CNF.
Once the protocol execution has finished, you will find the interactive transcript of the communication in logs/protocol.log. More advanced prover-related information, such as the list of composed operator polynomials, is written to logs/prover.log.
To render the animation showing how the QBF matrix is arithmetized, run
python anim_arithmetization.pyfrom the src directory. This will render the animation in Full HD using default manim rendering options. Alternatively, you can render the animation by calling manim directly, that is, with the
manim -pql anim_arithmetization.pycommand. Here, -pql stands for play, after rendering in quality low mode. If you don't want the animation to be automatically played once rendering is complete, remove p. The rendering quality can be also changed from low to medium or high. For more information regarding the manim command, see the official Manim CE documentation.
The resulting animation will build the arithmetizing polynomial step-by-step resulting in, for example,
at the end of the video. You can view the complete arithmetization animation produced for this formula on YouTube here.
Analogously to the above commands, the interactive proof can be animated by running
python anim_protocol.pyor, alternatively,
manim -pql anim_protocol.pyin the src directory. Rendering this animation will take considerably more time compared to the arithmetization animation discussed above. If you only need to animate a few first rounds, you can specify the amount of rounds to be animated via the rounds_limit parameter in the ProtocolScene constructor (anim_protocol.py module). If this parameter is set to 0 which is the default value, all interactive rounds will be animated.
Likewise, the formula for which the protocol is to be visualized can be specified via the qbf parameter, which by default is the above example formula qbf=default_example_formula().
Here are some screenshots from the animation that gets produced for the same formula that was arithmetized above:
The entire animation for this example is available on YouTube.
Note: This post contains both all the formal notation used in the visualization as well as a description of what each part of the animation means.
Warning: It is not recommended to animate arithmetization or the interactive proof when the QBF sentence contains more than 4 variables or clauses. The reason is that all parts of the animation may simply no longer fit on the screen.
Copyright (c) 2022 Alexander Mayorov.
This project is licensed under the MIT License. Please leave a license and copyright notice if you use this software. See the LICENSE file for more details.