arXiv subjects

Matthäus Micun

Publications and source records attributed to Matthäus Micun.

2 recordsLinked to original sources

arXiv2026

Restructuring Tree Decision Diagrams

Tree Decision Diagrams (TDDs) are a data structure recently introduced by Capelli et al. (SAT 2026). They are structured along a vtree and the size of their canonical form lies between Ordered Binary Decision Diagrams (OBDDs) and deterministic structured DNNF circuits (d-SDNNFs). While the succinctness gap between TDD and d-SDNNF is exponential, only a quasipolynomial separation between OBDD and TDD has been shown and it was left as open question whether this is optimal. We answer this question affirmatively by showing that every TDD can be transformed to an equivalent OBDD of quasipolynomial size. Although this might be seen as a weakness, our second result shows that TDDs share another desirable property with OBDDs that is not known to hold for d-SDNNF: Given a TDD and another target vtree, it is possible to construct the minimal and canonical TDD respecting the new vtree in time polynomial in the input and output. As a result we also obtain that the equivalence test between TDDs over different vtrees can be done in polynomial time.

cs.CC↗

arXiv2026

Proof Systems Based on Structured Circuits

Since their introduction by Atserias, Kolaitis, and Vardi in 2004, proof systems where each line is represented by an ordered binary decision diagram (OBDD) have been intensively studied as they allow to compactly represent Boolean functions. We extend this line of work by considering representation formats that can be even more succinct than OBDDs and have gained a lot of attention in the area of knowledge compilation: sentential decision diagrams (SDDs) and deterministic structured DNNF circuits (d-SDNNFs). We show that both variants can provide strictly smaller refutations of unsatisfiable CNFs than their OBDD counterparts. Furthermore, we investigate the relative strength of these systems depending on which of the three fundamental derivation rules join, reordering, and weakening are allowed. Here we obtain several separations and identify interesting open problems. To streamline our proofs we establish a sat-to-unsat lifting theorem that might be of independent interest: it turns satisfiable CNFs that are hard to represent by SDDs and d-SDNNFs into unsatisfiable CNFs that are hard to refute in the corresponding proof system.

cs.CC↗