satmate logo  
 Satisfiability Checking using General Matings   
About
SatMate  is a new SAT solver based on a technique called General Matings. It can decide the satisfiability of propositional (Boolean) formulas that are not necessarily in conjunctive normal form (CNF or clausal form). This is done without translating the given formula to CNF.  Currently, non-clausal input formula can be described in EDIMACS or ISCAS form.    

For questions about SatMate, contact Himanshu Jain or Constantinos Bartzis.



News
May 20, 2006: The x86 Linux binary of SatMate released.  

 


Documentation

 
  • Satisfiability Checking of Non-clausal Formulae using General Matings. (pdf) (ps)
    Himanshu Jain, Constantinos Bartzis, Edmund Clarke.
    In Ninth International Conference on Theory and Applications of Satisfiability Testing (SAT 2006). 
  • A more detailed version of the above paper (pdf) (ps)

 

Download

We currently distribute binaries for x86 Linux.

This research was sponsored by the 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.