Ricerc@Sapienza

In this note we show two results about k-DNF resolution. First we prove that there are CNF formulas which require exponential length refutations in resolution extended with parities of size k, but have polynomial length refutations in k-DNF resolution. Then we show that small proofs in tree-like k-DNF resolution and narrow proofs in dag-like resolution have the same proving power, over CNFs. This latter result is clearly implicit in Krajíček (1994) [24] but this direct proof is focused on resolution and provides information about refutation width.

We show the close connection between the enumeration of cliques in a k-clique free graph G and the length of tree-like resolution refutations for formula Clique(G,k), which claims that G has a k-clique. The length of any such tree-like refutation is within a "fixed parameter tractable" factor from the number of cliques in the graph. We then proceed to drastically simplify the proofs of the lower bounds for the length of tree-like resolution refutations of Clique(G,k) shown in [Beyersdorff et at. 2013, Lauria et al. 2017], which now reduce to a simple estimate of the number of cliques.

We introduce a new way of composing proofs in rule-based proof systems that generalizes tree-like and dag-like proofs. In the new definition, proofs are directed graphs of derived formulas, in which cycles are allowed as long as every formula is derived at least as many times as it is required as a premise. We call such proofs circular. We show that, for all sets of standard inference rules, circular proofs are sound.

In this paper it is shown how to obtain a low-cost, high-resolution and fault-robust position sensing system for permanent magnet synchronous motor drives operating in safety-critical systems, by combining high-frequency signal injection with binary Hall-effect sensors. It is shown that the position error signal obtained via high-frequency signal injection can be merged easily into the quantization-harmonic-decoupling vector tracking observer used to process the Hall-effect sensor signals.

We show that if a k-CNF requires width w to refute in resolution, then it requires space square root of √ω to refute in polynomial calculus, where the space of a polynomial calculus refutation is the number of monomials that must be kept in memory when working through the proof. This is the first analogue, in polynomial calculus, of Atserias and Dalmau's result lower-bounding clause space in resolution by resolution width.

We investigate the space complexity of refuting 3-CNFs in Resolution and algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random 3-CNF ? in n variables requires, with high probability, distinct monomials to be kept simultaneously in memory. The same construction also proves that every Resolution refutation of ? requires, with high probability, clauses each of width to be kept at the same time in memory. This gives a lower bound for the total space needed in Resolution to refute ?.