Till innehåll på sidan

Mladen Miksa: On Complexity Measures in Polynomial Calculus

Tid: Må 2016-09-12 kl 13.15

Plats: Room 4523, Lindstedtsvägen 5, KTH CSC

Medverkande: Mladen Miksa: KTH Royal Institute of Technology

Exportera till kalender

Abstract:

If we want to show that a formula in propositional logic is unsatisfiable, we can present a proof of this fact in some formal proof system. Propositional proof systems give us rules on how to derive new lines of the proof, starting from the original propositional formula, until we finally deduce a line that is an obvious contradiction. The most well studied proof system is resolution in which lines are clauses and there is only one inference rule. One stronger proof system is polynomial calculus, in which clauses are replaced with polynomial equations and which can therefore reason more efficiently about polynomial constraints than resolution can. In both of these proof systems we can naturally define the size and space of the proof. These two measures can be tied to the running time and memory usage of SAT solvers that use these proof systems. In this talk I will survey some recent results related to the size and space measures in polynomial calculus, and compare these results to similar results for resolution.