|
Welcome to the High-Level Satisfiability Group at the University of
California, Santa Barbara
The Satisfiability Problem is a well known NP-Complete
problem. Its theoretical importance is well known in
the theory of computation. It also plays a very important role in real
world applications such as Model Checking, Software Verification,
Electronic Design Automation and Verification.
Most real-world applications use high-level descriptions to represent
arithmetic and Boolean operations. It is often desirable that
satisfiability checking should be done on these high-level
descriptions rather than on a Boolean translation of the problem.
Several theorem provers, and satisfiability checkers like
ICS,
CVC-Lite,
Math-SAT, and
UCLID attempt to solve this problem.
Our approach to this problem integrates interval arithmetic and
Boolean SAT solving under a branch-and-bound framework called
HDPLL. We have encouraging preliminary results (here) on some
combinational RTL benchmarks.
The first release of HDPLL is available for
download. We have provided compiled binaries for x86 Linux.
Please contact us if you have any suggestions or
find any bugs. If you require the source code and/or binaries for
other platforms, please contact the maintainers.
The CAD Research Group is led
by
Professor Kwang-Ting Cheng in the Electrical and Computer Engineering
Department, University of California at Santa
Barbara.
Please contact the
maintainers for comments and suggestions.
|