Sub-SAT: A formulation for relaxed Boolean satisfiability with applications in routing

Hui Xu, Robin A Rutenbar, Karem Sakallah

Research output: Contribution to conferencePaperpeer-review

Abstract

Advances in methods for solving Boolean satisfiability (SAT) for large problems have motivated recent attempts to recast physical design problems as Boolean SAT problems. One persistent criticism of these approaches is their inability to supply partial solutions, i.e, to satisfy most but not all of the constraints cast in the SAT style. In this paper we present a formulation for "subset satisfiable" Boolean SAT: we transform a "strict" SAT problem with N constraints into a new, "relaxed" SAT problem which is satisfiable just if not more than k≪N of these constraints cannot be satisfied in the original problem. We describe a transformation based on explicit thresholding and counting for the necessary SAT relaxation. Examples from FPGA routing show how we can determine efficiently when we can satisfy "almost all" of our geometric constraints.

Original languageEnglish (US)
Pages182-187
Number of pages6
StatePublished - Jan 1 2002
EventISPD-2002: International Symposium on Physical Design - Del Mar, CA, United States
Duration: Apr 7 2002Apr 10 2002

Other

OtherISPD-2002: International Symposium on Physical Design
CountryUnited States
CityDel Mar, CA
Period4/7/024/10/02

Keywords

  • Algorithms

ASJC Scopus subject areas

  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Sub-SAT: A formulation for relaxed Boolean satisfiability with applications in routing'. Together they form a unique fingerprint.

Cite this