Accelerated SAT-based scheduling of control/data flow graphs

Seda Ogrenci Memik; Farzan Fallah

doi:10.1109/ICCD.2002.1106801

Accelerated SAT-based scheduling of control/data flow graphs

Seda Ogrenci Memik, Farzan Fallah

Electrical and Computer Engineering

Research output: Contribution to journal › Article › peer-review

23 Scopus citations

Abstract

In this paper we present a satisfiability-based approach to the scheduling problem in high-level synthesis. We formulate the resource constrained scheduling as a satisfiability (SAT) problem. We present experimental results on the performance of the state-of-the-art SAT solver, Chaff, and demonstrate techniques to reduce the SAT problem size by applying bounding techniques on the scheduling problem. In addition, we demonstrate the use of some transformations on control data flow graphs such that the same lower bound techniques can operate on them as well. Our experiments show that Chaff is able to outperform the Integer Linear Program (ILP) solver CPLEX in terms of CPU time by as much as 59 fold. Finally, we conclude that the satisfiability-based approach is a promising alternative for obtaining optimal solutions to NP-Complete scheduling problem instances.

Original language	English (US)
Article number	65
Pages (from-to)	395-400
Number of pages	6
Journal	Proceedings-IEEE International Conference on Computer Design: VLSI in Computers and Processors
DOIs	https://doi.org/10.1109/ICCD.2002.1106801
State	Published - Jan 1 2002

ASJC Scopus subject areas

Hardware and Architecture
Electrical and Electronic Engineering

Access to Document

10.1109/ICCD.2002.1106801

Fingerprint Dive into the research topics of 'Accelerated SAT-based scheduling of control/data flow graphs'. Together they form a unique fingerprint.

Cite this

@article{84143d0bb9d1481a873c2987edd99041,

title = "Accelerated SAT-based scheduling of control/data flow graphs",

abstract = "In this paper we present a satisfiability-based approach to the scheduling problem in high-level synthesis. We formulate the resource constrained scheduling as a satisfiability (SAT) problem. We present experimental results on the performance of the state-of-the-art SAT solver, Chaff, and demonstrate techniques to reduce the SAT problem size by applying bounding techniques on the scheduling problem. In addition, we demonstrate the use of some transformations on control data flow graphs such that the same lower bound techniques can operate on them as well. Our experiments show that Chaff is able to outperform the Integer Linear Program (ILP) solver CPLEX in terms of CPU time by as much as 59 fold. Finally, we conclude that the satisfiability-based approach is a promising alternative for obtaining optimal solutions to NP-Complete scheduling problem instances.",

author = "Memik, {Seda Ogrenci} and Farzan Fallah",

year = "2002",

month = jan,

day = "1",

doi = "10.1109/ICCD.2002.1106801",

language = "English (US)",

pages = "395--400",

journal = "Proceedings - IEEE International Conference on Computer Design: VLSI in Computers and Processors",

issn = "1063-6404",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

}

TY - JOUR

T1 - Accelerated SAT-based scheduling of control/data flow graphs

AU - Memik, Seda Ogrenci

AU - Fallah, Farzan

PY - 2002/1/1

Y1 - 2002/1/1

N2 - In this paper we present a satisfiability-based approach to the scheduling problem in high-level synthesis. We formulate the resource constrained scheduling as a satisfiability (SAT) problem. We present experimental results on the performance of the state-of-the-art SAT solver, Chaff, and demonstrate techniques to reduce the SAT problem size by applying bounding techniques on the scheduling problem. In addition, we demonstrate the use of some transformations on control data flow graphs such that the same lower bound techniques can operate on them as well. Our experiments show that Chaff is able to outperform the Integer Linear Program (ILP) solver CPLEX in terms of CPU time by as much as 59 fold. Finally, we conclude that the satisfiability-based approach is a promising alternative for obtaining optimal solutions to NP-Complete scheduling problem instances.

AB - In this paper we present a satisfiability-based approach to the scheduling problem in high-level synthesis. We formulate the resource constrained scheduling as a satisfiability (SAT) problem. We present experimental results on the performance of the state-of-the-art SAT solver, Chaff, and demonstrate techniques to reduce the SAT problem size by applying bounding techniques on the scheduling problem. In addition, we demonstrate the use of some transformations on control data flow graphs such that the same lower bound techniques can operate on them as well. Our experiments show that Chaff is able to outperform the Integer Linear Program (ILP) solver CPLEX in terms of CPU time by as much as 59 fold. Finally, we conclude that the satisfiability-based approach is a promising alternative for obtaining optimal solutions to NP-Complete scheduling problem instances.

UR - http://www.scopus.com/inward/record.url?scp=0036398348&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0036398348&partnerID=8YFLogxK

U2 - 10.1109/ICCD.2002.1106801

DO - 10.1109/ICCD.2002.1106801

M3 - Article

AN - SCOPUS:0036398348

SP - 395

EP - 400

JO - Proceedings - IEEE International Conference on Computer Design: VLSI in Computers and Processors

JF - Proceedings - IEEE International Conference on Computer Design: VLSI in Computers and Processors

SN - 1063-6404

M1 - 65

ER -