Cube-and-Conquer approach for SAT solving on grids

Biró, Csaba, Kovásznai, Gergely, Biere, Armin, Kusper, Gábor, Geda, Gábor (2013) Cube-and-Conquer approach for SAT solving on grids Annales Mathematicae et Informaticae. 42. pp. 9-21. ISSN 1787-5021 (Print), 1787-6117 (Online)

[img] pdf
AMI_42_from9to21.pdf

Download (755kB)

Absztrakt (kivonat)

Our goal is to develop techniques for using distributed computing re- sources to efficiently solve instances of the propositional satisfiability problem (SAT). We claim that computational grids provide a distributed computing environment suitable for SAT solving. In this paper we apply the Cube and Conquer approach to SAT solving on grids and present our parallel SAT solver CCGrid (Cube and Conquer on Grid) on computational grid infrastructure. Our solver consists of two major components. The master application runs march_cc, which applies a lookahead SAT solver, in order to partition the input SAT instance into work units distributed on the grid. The client application executes an iLingeling instance, which is a multi-threaded CDCL SAT solver. We use BOINC middleware, which is part of the SZTAKI Desktop Grid package and supports the Distributed Computing Application Programming Interface (DC-API). Our preliminary results suggest that our approach can gain significant speedup and shows a potential for future investigation and development. Keywords: grid, SAT, parallel SAT solving, lookahead, march_cc, iLingeling, SZTAKI Desktop Grid, BOINC, DC-API

Mű típusa: Folyóiratcikk
Szerző:
Szerző neveMTMT azonosítóORCID azonosítóKözreműködés
Biró, CsabaNEM RÉSZLETEZETTNEM RÉSZLETEZETTSzerző
Kovásznai, GergelyNEM RÉSZLETEZETTNEM RÉSZLETEZETTSzerző
Biere, ArminNEM RÉSZLETEZETTNEM RÉSZLETEZETTSzerző
Kusper, GáborNEM RÉSZLETEZETTNEM RÉSZLETEZETTSzerző
Geda, GáborNEM RÉSZLETEZETTNEM RÉSZLETEZETTSzerző
Kapcsolódó URL-ek:
Nyelv: angol
Kötetszám: 42.
ISSN: 1787-5021 (Print), 1787-6117 (Online)
Felhasználó: Tibor Gál
Dátum: 26 Feb 2019 18:13
Utolsó módosítás: 26 Feb 2019 18:13
URI: http://publikacio.uni-eszterhazy.hu/id/eprint/2910
Műveletek (bejelentkezés szükséges)
Tétel nézet Tétel nézet