On Minimum Representations of Matched Formulas (Extended Abstract)

On Minimum Representations of Matched Formulas (Extended Abstract)

Ondřej Čepek, Štefan Gurský, Petr Kučera

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Journal track. Pages 4980-4984. https://doi.org/10.24963/ijcai.2017/706

A Boolean formula in conjunctive normal form (CNF) is called matched if the system of sets of variables which appear in individual clauses has a system of distinct representatives. We present here two results for matched CNFs: The first result is a shorter and simpler proof of the fact that Boolean minimization remains complete for the second level of polynomial hierarchy even if the input is restricted to matched CNFs. The second result is structural --- we show that if a Boolean function f admits a representation by a matched CNF then every clause minimum CNF representation of f is matched.
Keywords:
Constraints and Satisfiability: Constraint Optimisation
Constraints and Satisfiability: Satisfiability