The concept of redundancy in SAT lead to more expressive and powerful proof search techniques, e.g. able to express various inprocessing techniques, and to interesting hierarchies of proof systems [Heule et.al’20, Buss-Thapen’19].
We propose a general way to integrate redundancy rules in MaxSAT, that is we define MaxSAT variants of ... more >>>

The matching and linear matroid intersection problems are solvable in quasi-NC, meaning that there exist deterministic algorithms that run in polylogarithmic time and use quasi-polynomially many parallel processors. However, such a parallel algorithm is unknown for linear matroid matching, which generalizes both of these problems. In this work, we propose ... more >>>

We design a deterministic subexponential time algorithm that takes as input a multivariate polynomial $f$ computed by a constant-depth circuit over rational numbers, and outputs a list $L$ of circuits (of unbounded depth and possibly with division gates) that contains all irreducible factors of $f$ computable by constant-depth circuits. This ... more >>>