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.