Full-length versions of these articles are available in arXiv, ECCC, and/or upon request.
arXiv preprint, March 2026.
Heiko Dietrich, Melissa Lee, Andre Nies, and Marc Vinyals: On the trivial units property and the unique product property. arXiv preprint, March 2026.
Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, and Marc Vinyals. Practically Feasible Proof Logging for Pseudo-Boolean Optimization. In Proceedings of the 31st International Conference on Principles and Practice of Constraint Programming (CP 2025), August 2025.
Susanna F. de Rezende and Marc Vinyals. Lifting with Colourful Sunflowers. In Proceedings of the 40th Computational Complexity Conference (CCC 2025), July 2025.
Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, and Marc Vinyals. Proving Unsatisfiability with Hitting Formulas. In Proceedings of the 15th Innovations in Theoretical Computer Science (ITCS 2024) conference, January 2024.
Marc Vinyals, Chunxiao Li, Noah Fleming, Antonina Kolokolova, Vijay Ganesh. Limits of CDCL Learning via Merge Resolution. In Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), July 2023.
Yuval Filmus, Edward Hirsch, Sascha Kurz, Ferdinand Ihringer, Artur Riazanov, Alexander Smal, and Marc Vinyals. Irreducible subcube partitions. The Electronic Journal of Combinatorics, September 2023.
Chunxiao Li, Jonathan Chung, Soham Mukherjee, Marc Vinyals, Antonina Kolokolova, Noah Fleming, Alice Mu and Vijay Ganesh. On the Hierarchical Community Structure of Practical SAT Formulas. In Proceedings of the 24th International Conference on Theory and Applications of Satisfiability Testing (SAT 2021).
Neta Dafni, Yuval Filmus, Noam Lifshitz, Nathan Lindzey, and Marc Vinyals. Complexity Measures on the Symmetric Group and Beyond. In Proceedings of the 12th Innovations in Theoretical Computer Science (ITCS 2021) conference, January 2021.
Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals. A Simplified Proof of the Space Complexity of Random 4-CNF Formulas in Polynomial Calculus. To appear.
Susanna F. de Rezende, Or Meir, Jakob Nordström, Tonian Pitassi, Robert Robere, and Marc Vinyals. Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity. In Proceedings of the 61st Annual IEEE Symposium on Foundations of Computer Science (FOCS 2020).
Yuval Filmus, Meena Mahajan, Gaurav Sood, and Marc Vinyals. MaxSAT Resolution and Subcube Sums. ACM Transactions on Computational Logic (TOCL), January 2023.
Chunxiao Li, Noah Fleming, Marc Vinyals, Toniann Pitassi, and Vijay Ganesh. Towards a Complexity-theoretic Understanding of the Power of Restart in SAT solvers. In Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT 2020),
Marc Vinyals, Jan Elffers, Jan Johannsen and Jakob Nordström. Improved Separations Between Regular and General Resolution Using Lifting. In Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT 2020),
Marc Vinyals. Hard Examples for Common Variable Decision Heuristics. In Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI 2020), February 2020.
Arkadev Chattopadhyay, Shachar Lovett, and Marc Vinyals. Equality Alone does not Simulate Randomness. In Proceedings of the 34th Computational Complexity Conference (CCC 2019), July 2019.
Jan Elffers, Jesús Giráldez-Cru, Jakob Nordström, and Marc Vinyals. Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers. In Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing (SAT 2018), July 2018.
Marc Vinyals, Jan Elffers, Jesús Giráldez-Cru, Stephan Gocht, and Jakob Nordström. In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving. In Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing (SAT 2018), July 2018.
Massimo Lauria, Jan Elffers, Jakob Nordström, and Marc Vinyals. CNFgen: A generator of crafted benchmarks. In Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT 2017), August 2017.
Full-length versions of these articles are included in my thesis.
Joël Alwen, Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals. Cumulative Space in Black-White Pebbling and Resolution. In Proceedings of the 8th Innovations in Theoretical Computer Science (ITCS 2017) conference, January 2017.
Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals. How Limited Interaction Hinders Real Communication (and What It Means for Proof and Circuit Complexity). In Proceedings of the 57th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2016), October 2016.
Jan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard, Jakob Nordström and Marc Vinyals. Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers. In Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016), July 2016.
Siu Man Chan, Massimo Lauria, Jakob Nordström, and Marc Vinyals. Hardness of Approximation in PSPACE and Separation Results for Pebble Games. In Proceedings of the 56th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2015), October 2015.
Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals. From Small Space to Small Width in Resolution. ACM Transactions on Computational Logic (TOCL), November 2015.
Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals. Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds. In Proceedings of the 40th International Colloquium on Automata, Languages and Programming (ICALP 2013), July 2013.
QUBO, Pseudo-Boolean and SAT Solving. CNRS@CREATE, Singapore, March 2026.
A Pseudo-Boolean Solver Interface. (Workshop), Banff, January 2026.
QUBO, Pseudo-Boolean and SAT Solving. PRICAI 2025 Workshop on Quantum Computing for Search and Optimization Problems, Wellington, November 2025.
Lifting with Colourful Sunflowers. MIAO Seminar, Lund, October 2025.
Lifting with Colourful Sunflowers. CCC 2025, Toronto, July 2025.
Proof logging for RoundingSat. Sloppy 2024 Workshop, Lund, November 2024.
SAT and Proof Complexity Tutorial. (Workshop), Dagstuhl, 2024.
CDCL vs Resolution. UCSD, November 2023.
Understanding algorithms through proofs. IIT Jodhpur, September 2023.
Limits of CDCL Learning via Merge Resolution. SAT 2023, Alguer, July 2023.
Limits of CDCL Learning via Merge Resolution. Satisfiability: Theory, Practice, and Beyond Reunion, Berkeley, April 2023.
Understanding algorithms through proofs. MUN CS Seminar, MUN, 2022.
Theoretical limits of 1UIP Learning. (Workshop), Dagstuhl, 2022.
CDCL vs Resolution. UMass Amherst Theory Seminar, Online, September 2022. [Video]
CDCL vs Resolution. Satisfiability: Theory, Practice, and Beyond Reunion, Berkeley, June 2022.
CDCL vs Resolution. MIAO Seminar, Lund, May 2022.
Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity. Problems in Computer Science Workshop, Moscow, December 2021.
CDCL vs Resolution. Haifa SAT Seminar, Haifa, July 2021.
Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity. SPbU Seminar, Online, 2021.
Hard Examples for Common Variable Decision Heuristics. (Simons Workshop), Online, 2021.
Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity. FOCS 2020, Online, November 2020. Video.
Improved Separations Between Regular and General Resolution Using Lifting. SAT 2020, Online, July 2020. Video. Slides for the short version.
Hard Examples for Common Variable Decision Heuristics. AAAI 2020, New York, February 2020.
Hard Examples for Common Variable Decision Heuristics. SAT and Interactions Workshop, Dagstuhl, February 2020.
Equality Alone Does not Simulate Randomness. [Video] IAS, Princeton, January 2020.
Hard Examples for Common Variable Decision Heuristics. Proof Complexity Workshop, Banff, January 2020. Video
Lifting Applied to Proof Complexity. Proof Complexity Workshop, Banff, January 2020. Video
Lifting Applied to Proof Complexity. FSTTCS workshop on Extension Complexity and Lifting Theorems, Mumbai, December 2019.
Equality Alone Does not Simulate Randomness. KU, Copenhagen, October 2019.
Equality Alone Does not Simulate Randomness. UPC, Barcelona, September 2019.
Equality Alone Does not Simulate Randomness. CCC 2019, New Brunswick, July 2019.
Equality Alone Does not Simulate Randomness. TIFR STCS Days 2019, Mumbai, March 2019.
A Proof Complexity View of Pseudo-Boolean Solving. Theory and Practice of Satisfiability Solving Workshop, Casa Matemática Oaxaca, August 2018. Video.
In Between Resolution and Cutting Planes: Proof Systems for Pseudo-Boolean SAT Solving. Proof Complexity Workshop, Dagstuhl, February 2018.
CNFgen: A generator of crafted CNF formulas. SAT 2017, Melbourne, August 2017.
In Between Resolution and Cutting Planes: Proof Systems for Pseudo-Boolean SAT Solving. PoCR 2017, Melbourne, August 2017.
How Limited Interaction Hinders Real Communication (and What it Means for Proof and Circuit Complexity). Proof Complexity and Beyond Workshop, Oberwolfach, August 2017.
Hardness Escalation in Proof Complexity via Composition. China Theory Week 2017, Shanghai, July 2017.
How Limited Interaction Hinders Real Communication (and What it Means for Proof and Circuit Complexity). Tata Institute of Fundamental Research, Mumbai, February 2017.
Cumulative Space in Black-White Pebbling and Resolution. ITCS 2017, Berkeley, January 2017. Video.
How Limited Interaction Hinders Real Communication (and What it Means for Proof and Circuit Complexity). Theoretical Foundations of SAT Solving Workshop, Toronto, August 2016.
How Limited Interaction Hinders Real Communication (and What it Means for Proof and Circuit Complexity). University of Toronto, August 2016.
How Limited Interaction Hinders Real Communication (and What it Means for Proof and Circuit Complexity). Proof complexity workshop at the Special Semester Program on Computational Complexity, St Petersburg, May 2016.
The Size of Coefficients in Cutting Planes Proofs. Special Semester Program on Computational Complexity, St Petersburg, May 2016.
Hardness of Approximation in PSPACE and Separation Results for Pebble Games. FOCS 2015, Berkeley, October 2015. Video.
Size-Space Bounds and Trade-offs for CDCL Proofs. Proof complexity workshop at the Summer of Logic, Vienna, July 2014.
Proof Complexity Zoo. A community-editable database of proof systems, formulas, and relations. Old, static version. Old sources.
Solver Geometry Heatmaps. An alternative way of visualizing SAT solver relative strengths. This is work in progress; suggestions and bugfixes are appreciated.
CNFgen Formula Generator. A collection of “crafted” formula generators, including many formulas with interesting hardness properties. Maintained by Massimo Lauria, I contribute regularly.
TextbookSAT. A modular SAT solver that can be used to experiment with different heuristics and even make choices interactively.