Accelerated SAT-based scheduling of control/data flow graphs

Seda Ogrenci Memik, Farzan Fallah

Research output: Contribution to journalArticlepeer-review

23 Scopus citations


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 languageEnglish (US)
Article number65
Pages (from-to)395-400
Number of pages6
JournalProceedings-IEEE International Conference on Computer Design: VLSI in Computers and Processors
StatePublished - 2002

ASJC Scopus subject areas

  • Hardware and Architecture
  • Electrical and Electronic Engineering


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

Cite this