readme

命题逻辑的求解器,2004年SAT竞赛第一名的求解器

=====================Legal Notice===========================
Disclaimer: The author and Princeton University shall not be hold 
responsable for any damage caused by using or unable to use this
software. The software and documentation is provided "AS IS"

This software is for research and educational purpose only. No 
commercial use is allowed without written permission from 
Princeton University.
============================================================

This is the first public release of the source code for ZChaff. This
code is a preliminary version and will be replaced soon. I am currently
working on another version which (hopefully) will be much more complete
and offer more options. This version shall only be regarded as a
prototype. I don't have any documentations. But if you have any 
questions about it, you can ask me and I will try to answer them ASAP.

Because this is basically a development snapshot (I ripped off some 
experimental options). It may have some redundent data structures and
all kinds of stupidities (they may have served some purpose once). However,
You should able to reproduce the quoted performance data with this
version. (more or less)

You should have no problem compile it under x86 Linux and Sun Solaris
using g++. For other platforms, you may need to modify Makefile a 
little bit. The code is fairly simple, and basically implemented what
was discribed in the paper. 

If you want to incoporate Chaff into your own enviroment, you need
to read SAT.h to find out the usage of the interface. You can also
look at sat_solver.cpp to find out how is the interface being called.

EVERYTHING IN THIS VERSION IS SUBJECT TO CHANGE. So, don't be surprised
if next version don't have some of the options and/or have uncompatible
functions. It's only served as a demontration why Chaff has less cache
miss rate and why it's fast etc. Still, we (well, I) believe that this
version is as good as most other public domain SAT solvers out there 
(program quality wise). You can use this to do some serious jobs already.

Known bug: 
1. The parser of sat_solver.cpp was taken from GRASP. It does
not check the syntex very strictly, if the input has wrong format, 
the solver may generate segementation falut.

2. Some counters may overflow for big examples. I have some patches
somewhere but can't find them now. The result should be correct, though, 
even if you found some negative counter numbers. 

Please report bugs to [e-mail]

Lintao Zhag
Princeton University
2001.6.15