REAL

Formula partitioning revisited

Mann, Zoltán Ádám and Papp, Pál András (2014) Formula partitioning revisited. In: Fifth Pragmatics of SAT workshop.

[img]
Preview
Text
epic829256805.pdf - Published Version

Download (404kB) | Preview

Abstract

Dividing a Boolean formula into smaller independent sub-formulae can be a useful technique for accelerating the solution of Boolean problems, including SAT and #SAT. Nevertheless, and despite promising early results, formula partitioning is hardly used in state-of-the-art solvers. In this paper, we show that this is rooted in a lack of consistency of the usefulness of formula partitioning techniques. In particular, we evaluate two existing and a novel partitioning model, coupled with two existing and two novel partitioning algorithms, on a wide range of benchmark instances. Our results show that there is no one-size-fits-all solution: for different formula types, different partitioning models and algorithms are the most suitable. While these results might seem negative, they help to improve our understanding about formula partitioning; moreover, the findings also give guidance as to which method to use for what kinds of formulae.

Item Type: Conference or Workshop Item (Lecture)
Subjects: Q Science / természettudomány > QA Mathematics / matematika > QA75 Electronic computers. Computer science / számítástechnika, számítógéptudomány
Depositing User: Dr. Zoltán Ádám Mann
Date Deposited: 22 Sep 2014 21:32
Last Modified: 03 Apr 2023 08:16
URI: http://real.mtak.hu/id/eprint/16017

Actions (login required)

Edit Item Edit Item