Improving Pseudo-Boolean Solving and Integer Linear Programming
This is a project aimed at trying to go beyond state-of-the-art in pseudo-Boolean SAT solving and optimization, which is a special case of integer linear programming. We are going to try out a number of different new ideas, inspired by mathematical research, that have not been implemented before in practice. To evaluate how well they perform, we will need to run extensive experiments and measure resources such as running time (primarily), memory usage, et cetera. This research is part of the ERC Starting Independent Research Grant "Understanding the Hardness of Theorem Proving" and is also supported by a "breakthrough research grant" from the Swedish Research Council (VR).