Improving Pseudo-Boolean Solving and Integer Linear Programming

Dnr:

SNIC 2017/1-30

Type:

SNAC Medium

Principal Investigator:

Jakob Nordström

Affiliation:

Kungliga Tekniska högskolan

Start Date:

2017-01-30

End Date:

2018-02-01

Primary Classification:

10201: Datavetenskap (= Datalogi)

Webpage:

http://www.csc.kth.se/~jakobn/project-proofcplx/

Allocation

Abstract

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