Цейтинские формулы и однопроходные ветвящиеся программы

Пусть $G$ — связный неориентированный граф с нечетным числом вершин, каждое ребро графа помечено нулем или единицей, мы рассмотрим две задачи: в первой задаче требуется проверить, верно ли что для всех вершин графа сумма пометок инцидентных им ребер четна. Во второй задаче требуется найти вершину, в которой сумма пометок инцидентных ей ребер четна. В докладе пойдет речь о том, как связаны сложности этих задач, если их решать однопроходными ветвящимися программами, а также о связи этих задач со сложностью вывода цейтинских формул в некоторых системах доказательств.