Department of Electrical and Computer Engineering

The Computer Engineering and Systems Group

Boolean Satisfiability

 

Boolean Satisfiability (SAT) is a core NP-complete problem. We are keenly interested in approaches to deliver faster SAT solvers. In the past, we have developed both custom IC and FPGA based SAT solver engines. The FPGA based engine was prototyped, and achieved about 17X speedup over the best known software SAT solver. The custom IC approach yielded over 3 orders of magnitude speedup. Both engines were designed with scalability as a key requirement.

 

We have also developed a GPU based SAT solver. This consists of an exact solver (MiniSAT) running on the CPU, whose variable scoring heuristic is guided by a GPU-based survey-sat engine. The completeness of the procedure is guaranteed by the fact that the complete procedure runs on the CPU, and only receives variable scoring advise from the GPU based survey SAT solver. We obtained an average speedup of 2.35X.

We are also working on a SAT solver that is based on noise-based logic. In this solver, the traditional search is averted. Literals are encoded as uncorrelated noise sources. The instance is satisfiable iff the output of the solver has a non-zero DC average value. Satisfiability checks take n steps (where n is the number of variables in the instance). The worst case duration of any step is exponential.

Publications, patents and artefacts:

  • “Boolean Satisfiability using Noise Based Logic”, Lin, Mandal, Khatri. ArXiv:1110.0550v1. In this paper, we formulate the problem of solving SAT using noise based logic. This yields a SAT based solution without traditional search, in n steps (where n is the number of variables in the problem). We are currently implementing this approach to compare it with traditional SAT solvers on large problems.
  • “Boolean Satisfiability on a Graphics Processor”, Gulati, Khatri. Great Lakes Symposium on VLSI (GLS-VLSI) 2010. Providence, RI. May 16-18, 2010. In this paper, we implement Boolean Satisfiability on a GPU, using a technique which achieves a significant speedup over MiniSAT, a leading CPU based SAT solver while retaining the completeness of the search.
  • “FPGA-Based Hardware Acceleration for Boolean Satisfiability”, Gulati, Paul, Khatri, Patil, Jas. ACM Transactions on Design Automation of Electronic Systems (TODAES). Vol 14, number 2, Mar 2009. Among the top 10 downloaded papers for the journal in 2010. Nominated for best paper for the journal (2010). This paper presents an FPGA based scalable SAT solver. The SAT instance is partitioned up-front, and the FPGA solves one partition at a time, with the ability to do non-chronological backtrack within as well as across partitions, and operates about 17X faster than MiniSAT, a very powerful software based solver.
  • “An Efficient, Scalable Hardware Engine for Boolean Satisfiability and Unsatisfiable Core Extraction”, Gulati, Waghmode, Khatri, Shi. IET Computers and Digital Techniques, vol. 2, number 3, May 2008, pp. 214-229. A shorter version of this paper appeared in the IEEE International Conference on Computer Design (ICCD) 2006 as well. This paper is a custom-IC based design of a SAT solver. The solution is designed to scale elegantly, and provides over three orders of magnitude speedup over software based approaches.