Ruben Martins — accepted AI-conference papers

2025

The Impact of Literal Sorting on Cardinality Constraint Encodings

Joseph E. Reeves, João Filipe, Min-Chien Hsu, Ruben Martins, Marijn J. H. Heule

AAAI 2025technical

The effectiveness of satisfiability solvers strongly depends on the quality of the encoding of a given problem into conjunctive normal form. Cardinality constraints are prevalent in numerous problems, prompting the development and study of various types of encoding. We present a novel approach to op…

Cited by 3 Source ↗PDF ↗code ↗Scholar ↗

2023

Certified CNF Translations for Pseudo-Boolean Solving (Extended Abstract).

Stephan Gocht, Ruben Martins, Jakob Nordström, Andy Oertel

IJCAI 2023poster

The dramatic improvements in Boolean satisfiability (SAT) solving since the turn of the millennium have made it possible to leverage conflict-driven clause learning (CDCL) solvers for many combinatorial problems in academia and industry, and the use of proof logging has played a crucial role in incr…

Cited by 0 Source ↗PDF ↗Scholar ↗