Showing 1–1 of 1 results for author: Peitl, T

Co-Certificate Learning with SAT Modulo Symmetries

Authors: Markus Kirchweger, Tomáš Peitl, Stefan Szeider

Abstract: We present a new SAT-based method for generating all graphs up to isomorphism that satisfy a given co-NP property. Our method extends the SAT Modulo Symmetry (SMS) framework with a technique that we call co-certificate learning. If SMS generates a candidate graph that violates the given co-NP property, we obtain a certificate for this violation, i.e., `co-certificate' for the co-NP property. The c… ▽ More We present a new SAT-based method for generating all graphs up to isomorphism that satisfy a given co-NP property. Our method extends the SAT Modulo Symmetry (SMS) framework with a technique that we call co-certificate learning. If SMS generates a candidate graph that violates the given co-NP property, we obtain a certificate for this violation, i.e., `co-certificate' for the co-NP property. The co-certificate gives rise to a clause that the SAT solver, serving as SMS's backend, learns as part of its CDCL procedure. We demonstrate that SMS plus co-certificate learning is a powerful method that allows us to improve the best-known lower bound on the size of Kochen-Specker vector systems, a problem that is central to the foundations of quantum mechanics and has been studied for over half a century. Our approach is orders of magnitude faster and scales significantly better than a recently proposed SAT-based method. △ Less

Submitted 21 June, 2023; v1 submitted 17 June, 2023; originally announced June 2023.

Comments: To appear in the Proceedings of IJCAI 2023, the 32nd International Joint Conference on Artificial Intelligence, August 19-25, 2023, Macao, S.A.R. This update fixes a formatting glitch with references