sub-SAT: a formulation for relaxed Boolean satisfiability with applications in routing

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<