The SatMate download contains a statically linked binary called
"satmate" and an examples directory to illustrate the usage of
Satmate.

-------------------------------------------------------------------
USING SatMate 

Running satmate on EDIMACS examples:

./satmate examples/edimacs/dead-dnd01.ncnf
./satmate examples/edimacs/test3.in


Running satmate on ISCAS examples:

./satmate examples/iscas/ph7_8.iscas --iscas
./satmate examples/iscas/small2.iscas --iscas


Running satmate on CNF examples in DIMACS format:

./satmate examples/cnf/add32.cnf --cnf
./satmate examples/cnf/prime2209.cnf --cnf


NOTE: Only AND/OR/NOT gates are allowed in the EDIMACS or ISCAS inputs
currently. 


References:

1. EDIMACS format. http://www.satcompetition.org/2005/edimacs.pdf
2. If you want to cite satmate please use the following bibtex entry:

@inproceedings{jbc06,
  author    = {Himanshu Jain and Constantinos Bartzis and Edmund Clarke},
  title     = {Satisfiability Checking of Non-clausal Formulae using General Matings},
  booktitle = {SAT},
  year      = {2006}
}

-------------------------------------------------------------------

Please email Himanshu Jain to report bugs or benchmarks that satmate
cannot handle.

--------------------------------------------------------------------