Full-length versions of these articles are available in arXiv, ECCC, and/or upon request.
Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, and Marc Vinyals. Proving Unsatisfiability with Hitting Formulas. To appear 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.
CDCL vs Resolution. Talk given at the UMass Amherst Theory Seminar, Online, September 2022. [Video]
CDCL vs Resolution. Talk given at the Satisfiability: Theory, Practice, and Beyond Reunion, Berkeley, June 2022.
CDCL vs Resolution. Talk given at the MIAO Seminar, Lund, May 2022.
Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity. Talk given at the Problems in Computer Science Workshop, Moscow, December 2021.
CDCL vs Resolution. Talk given at the Haifa SAT Seminar, Haifa, July 2021.
Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity. Talk given at the SPbU Seminar, Online, 2021.
Hard Examples for Common Variable Decision Heuristics. Talk given at the (Simons Workshop), Online, 2021.
Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity. Talk given at FOCS 2020, Online, November 2020. Video.
Improved Separations Between Regular and General Resolution Using Lifting. Talk given at SAT 2020, Online, July 2020. Video. Slides for the short version.
Hard Examples for Common Variable Decision Heuristics. Talk given at AAAI 2020, New York, February 2020.
Hard Examples for Common Variable Decision Heuristics. Talk given at the SAT and Interactions Workshop, Dagstuhl, February 2020.
Equality Alone Does not Simulate Randomness. [Video] Talk given at IAS, Princeton, January 2020.
Hard Examples for Common Variable Decision Heuristics. Talk given at the Proof Complexity Workshop, Banff, January 2020. Video
Lifting Applied to Proof Complexity. Talk given at the Proof Complexity Workshop, Banff, January 2020. Video
Lifting Applied to Proof Complexity. Talk given at the FSTTCS workshop on Extension Complexity and Lifting Theorems, Mumbai, December 2019.
Equality Alone Does not Simulate Randomness. Talk given at KU, Copenhagen, October 2019.
Equality Alone Does not Simulate Randomness. Talk given at UPC, Barcelona, September 2019.
Equality Alone Does not Simulate Randomness. Talk given at CCC 2019, New Brunswick, July 2019.
Equality Alone Does not Simulate Randomness. Talk given at TIFR STCS Days 2019, Mumbai, March 2019.
A Proof Complexity View of Pseudo-Boolean Solving. Talk given at the 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. Talk given at the Proof Complexity Workshop, Dagstuhl, February 2018.
CNFgen: A generator of crafted CNF formulas. Talk given at SAT 2017, Melbourne, August 2017.
In Between Resolution and Cutting Planes: Proof Systems for Pseudo-Boolean SAT Solving. Talk given at PoCR 2017, Melbourne, August 2017.
How Limited Interaction Hinders Real Communication (and What it Means for Proof and Circuit Complexity). Talk given at the Proof Complexity and Beyond Workshop, Oberwolfach, August 2017.
Hardness Escalation in Proof Complexity via Composition. Talk given at China Theory Week 2017, Shanghai, July 2017.
How Limited Interaction Hinders Real Communication (and What it Means for Proof and Circuit Complexity). Talk given at the Tata Institute of Fundamental Research, Mumbai, February 2017.
Cumulative Space in Black-White Pebbling and Resolution. Talk given at ITCS 2017, Berkeley, January 2017. Video.
How Limited Interaction Hinders Real Communication (and What it Means for Proof and Circuit Complexity). Talk given at the Theoretical Foundations of SAT Solving Workshop, Toronto, August 2016.
How Limited Interaction Hinders Real Communication (and What it Means for Proof and Circuit Complexity). Talk given at the University of Toronto, August 2016.
How Limited Interaction Hinders Real Communication (and What it Means for Proof and Circuit Complexity). Talk given at the Proof complexity workshop at the Special Semester Program on Computational Complexity, St Petersburg, May 2016.
The Size of Coefficients in Cutting Planes Proofs. Talk given at the Special Semester Program on Computational Complexity, St Petersburg, May 2016.
Hardness of Approximation in PSPACE and Separation Results for Pebble Games. Talk given at FOCS 2015, Berkeley, October 2015. Video.
Size-Space Bounds and Trade-offs for CDCL Proofs. Talk given at the 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.