Offers
[TAKEN] Memory-efficient multi-threaded SAT backend for MallobSat[TAKEN] Memory-efficient multi-threaded SAT backend for MallobSat
Note: This topic has been taken / reserved.
The task of this bachelor/master thesis is to integrate Gimsatul, a shared-memory parallel SAT solver that physically shares clauses among threads, into the Mallob system as a first “natively multi-threaded” SAT backend. We expect this to result in a substantial reduction of Mallob’s memory footprint.
Notable challenges include the development of a sound and efficient interface for importing and exporting clauses to/from a Gimsatul backend and the implementation of a reasonable strategy regarding which clauses to export and to import.
The thesis includes algorithmic design, software architecture considerations, implementation, large-scale experiments, and analysis of experimental data.
Contact: dominik.schreiber@kit.edu
Cooperation partner: Prof. Armin Biere, University of Freiburg