Satisfiablity Checking of Non-Clausal Formulas using DPLL, Graphs, and Watched Cuts: NFLSAT Homepage
nflsat logo
Non-clausal Formulas Satisfiability Checker
About
Boolean satisfiability (SAT) solvers are used heavily in hardware and
software verification tools for checking satisfiability of Boolean
circuits. NFLSAT is a new SAT solver that operates on the negation
normal form (NNF) of the given Boolean circuits. The input to NFLSAT
is a Boolean circuit in
And
Inverter Graph (AIG) format or ISCAS format.
For
questions (source code access) about NFLSAT, contact Himanshu Jain and Edmund M. Clarke.
Papers/Documentation
- Efficient SAT Solving for Non-Clausal Formulas using DPLL, Graphs, and Watched Cuts (pdf) (bibtex)
DAC 2009, To appear in 46th Design Automation Conference .
- Verification Using Satisfiability Checking, Predicate Abstraction, and Craig Interpolation (pdf) (bibtex)
CMU CS technical report (CMU-CS-08-146).
Chapter 4 presents the main ideas behind NFLSAT. The basic concepts are described in Chapter 2.
Download
We currently distribute binaries
for x86 Linux.
This research was sponsored by the Semiconductor Research Corporation (SRC), Gigascale Systems
Research Center (GSRC), the National Science Foundation (NSF) , the
Office of Naval Research (ONR), the Naval Research Laboratory (NRL), and
by the Defense Advanced Research Projects Agency, and the Army Research
Office (ARO). The views and conclusions contained in this document are
those of the author and should not be interpreted as representing the
official policies, either expressed or implied, of GSRC, NSF, ONR, NRL,
DOD, ARO, or the U.S. government.