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
MaxSAT solving and (linear) pseudo-Boolean optimization
Subgraph solving algorithms (for, e.g., clique, subgraph isomorphism, and maximum common subgraph)
Constraint programming solvers

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.
Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified Symmetry and Dominance Breaking for Combinatorial Optimisation. In Proceedings of the 36th AAAI Conference on Artificial Intelligence (AAAI '22), pages 3698-3707, February 2022. AAAI '22 distinguished paper award.
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.

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 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.

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.