Jakob Nordström / Software

Software

On this webpage you find the most important pieces of software produced by the MIAO group with collaborators. In addition to what is listed below, you can always check out our GitLab repository gitlab.com/MIAOresearch/software. All of this is research-grade software, with some more rough edges than would ideally be the case, but if you need bleeding-edge technology, perhaps it could be worth checking out. 😉

Also, if you have any questions about our tools, or any bug reports, or anything else, please don't hesitate to let us know. Although we are a research group, and have very limited resources for software maintenance, we are still trying to do our best to produce high-quality code.

RoundingSat

RoundingSat is a solver and optimization engine for pseudo-Boolean formulas, i.e., 0-1 integer linear programs.

The basic pseudo-Boolean solver combines conflict-driven search based on the cutting planes proof system with techniques from integer linear programming (ILP) such as linear programming relaxations and cut generation. The optimization engine implements linear SAT-UNSAT search (a.k.a. model-improving search) and core-guided search using the solver as an oracle.

Some publications that describe features available in the public version of RoundingSat, and that we would ask you to cite if you use RoundingSat in your work, are listed below. (Please note that the name of the solver is RoundingSat and nothing else — there is no version of the solver called "HYBRID" or anything else, although for some mysterious reason some other reasearch papers have invented this name for the optimization engine based on RoundingSat.)

Jan Elffers and Jakob Nordström. Divide and Conquer: Towards Faster Pseudo-Boolean Solving. In Proceedings of the 27th International Joint Conference on Artificial Intelligence (IJCAI '18), pages 1291-1299, July 2018.
Jo Devriendt. Watched Propagation of 0-1 Integer Linear Constraints. In Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP '20), Lecture Notes in Computer Science, volume 12333, pages 160-176, September 2020.
Jo Devriendt, Stephan Gocht, Emir Demirović, Jakob Nordström, and Peter Stuckey. Cutting to the Core of Pseudo-Boolean Optimization: Combining Core-Guided Search with Cutting Planes Reasoning. In Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI '21), pages 3750-3758, February 2021.
Jo Devriendt, Ambros Gleixner, and Jakob Nordström. Learn to Relax: Integrating 0-1 Integer Linear Programming with Conflict-Driven Pseudo-Boolean Search. Constraints, January 2021. (Special issue for CPAIOR '20.)

Some experimental features that have not (or at least not yet) made it into the main branch of the solver are described in the following papers:

Jan Elffers and Jakob Nordström. A Cardinal Improvement to Pseudo-Boolean Solving. In Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI '20), pages 1495-1503, February 2020.
Buser Say, Jo Devriendt, Jakob Nordström, and Peter Stuckey. Theoretical and Experimental Results for Planning with Learned Binarized Neural Network Transition Models. In Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP '20), Lecture Notes in Computer Science, volume 12333, pages 917-934, September 2020.

VeriPB

VeriPB is a verifier for pseudo-Boolean proofs. The proof format is based on the cutting planes proof system studied in proof complexity, enhanced with some extension rules to support derivation steps like definitions of new variables. This proof system turns out to be quite a convenient foundation for so-called certifying solvers in combinatorial solving and optimization paradigms like:

Boolean satisfiability (SAT) solving, including advanced techniques for which there is no support for efficient proof logging using other tools
MaxSAT solving and (linear) pseudo-Boolean optimization
Subgraph solving algorithms (for, e.g., clique, subgraph isomorphism, and maximum common subgraph)
Constraint programming solvers
Presolving in 0-1 integer linear programming

Since 2023, VeriPB has been used as one of the proof checkers in the SAT Competition, and in 2024 it was also used in the Pseudo-Boolean Competition.

All of this is a very active area of research, and the MIAO group with collaborators have so far published the following papers:

Jan Elffers, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Justifying All Differences Using Pseudo-Boolean Reasoning. In Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI '20), pages 1486-1494, February 2020.
Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Subgraph Isomorphism Meets Cutting Planes: Solving with Certified Solutions. In Proceedings of the 29th International Joint Conference on Artificial Intelligence (IJCAI '20), pages 1134-1140, July 2020.
Stephan Gocht, Ross McBride, Ciaran McCreesh, Jakob Nordström, Patrick Prosser, and James Trimble. Certifying Solvers for Clique and Maximum Common (Connected) Subgraph Problems. In Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP '20), Lecture Notes in Computer Science, volume 12333, pages 338-357, September 2020.
Stephan Gocht and Jakob Nordström. Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs. In Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI '21), pages 3768-3777, February 2021.
Stephan Gocht, Ruben Martins, Jakob Nordström, and Andy Oertel. Certified CNF Translations for Pseudo-Boolean Solving. In Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing (SAT '22), Leibniz International Proceedings in Informatics (LIPIcs), volume 236, pages 16:1-16:25, August 2022. SAT '22 best paper award.
Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. An Auditable Constraint Programming Solver. In Proceedings of the 28th International Conference on Principles and Practice of Constraint Programming (CP '22), Leibniz International Proceedings in Informatics (LIPIcs), volume 235, pages 25:1-25:18, August 2022.
Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, and Dieter Vandesande. Certified Core-Guided MaxSAT Solving. In Proceedings of the 29th International Conference on Automated Deduction (CADE-29), Lecture Notes in Computer Science, volume 14132, pages 1-22, July 2023.
Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified Dominance and Symmetry Breaking for Combinatorial Optimisation. Journal of Artificial Intelligence Research, volume 77, pages 1539-1589, August 2023. Full-length version of conference paper receiving AAAI '22 distinguished paper award.
Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, and Yong Kiam Tan. End-to-End Verification for Subgraph Solving. In Proceedings of the 38th AAAI Conference on Artificial Intelligence (AAAI '24), pages 8038-8047, February 2024.
Alexander Hoen, Andy Oertel, Ambros Gleixner, and Jakob Nordström. Certifying MIP-based Presolve Reductions for 0-1 Integer Linear Programs. In Proceedings of the 21st International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR '24), pages 310-328, May 2024.
Matthew McIlree, Ciaran McCreesh, and Jakob Nordström. Proof Logging for the Circuit Constraint. In Proceedings of the 21st International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR '24), pages 38-55, May 2024.
Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen, and Jakob Nordström. Certified MaxSAT Preprocessing. In Proceedings of the 12th International Joint Conference on Automated Reasoning (IJCAR '24), pages 396-418, July 2024.
Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Tobias Paxian, and Dieter Vandesande. Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability. In Proceedings of the 30th International Conference on Principles and Practice of Constraint Programming (CP '24), pages 4:1-4:28, September 2024.
Emir Demirović, Ciaran McCreesh, Matthew McIlree, Jakob Nordström, Andy Oertel, and Konstantin Sidorov. Pseudo-Boolean Reasoning About States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms. In Proceedings of the 30th International Conference on Principles and Practice of Constraint Programming (CP '24), pages 9:1-9:21, September 2024.

The most detailed technical documentaiton of VeriPB is what was submitted for the SAT Competition in 2023:

Bart Bogaerts, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, and Yong Kiam Tan. Documentation of VeriPB and CakePB for the SAT Competition 2023 . March 2023.

However, since the tool is being being developed and extended very dynamically, the most up-to-date description is what can be found in the VeriPB repository.

CNFgen

CNFgen is a tool for generating combinatorial (a.k.a. crafted) formulas in conjunctive normal form (CNF) in the standard DIMACS format used by SAT solvers. The formulas produced by CNFgen have been collected from the proof complexity literature, and many of them encode combinatorial principles that are known to be tricky, or even very hard, for conflict-driven clause learning (CDCL) solvers. The main developer and maintainer of CNFgen is Massimo Lauria, a former postdoc in our research group who is now a professor at Sapienza Università di Roma.

If you use CNFgen, please cite the paper:

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 '17), Lecture Notes in Computer Science, volume 10491, pages 464-473, August 2017.