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.