source: vis_dev/zchaff/README @ 25

Last change on this file since 25 was 10, checked in by cecile, 13 years ago

Zchaff

File size: 5.2 KB
Line 
1[2008.10.12]
2This is the same as 2007.3.12 but can be compiled with g++-4.3
3
4[2007.3.12]
5Fixed the inefficiency bug in zverify_df. Thanks to Allen Van Gelder and
6Tjark Weber.
7
8[2004.11.15 Simplified]
9This is just a simplified version of 2004.5.13. Many portions of dead
10codes are removed. Some of codes are re-written and re-formatted for
11easy reading. You might experience a little speedup. Please switch back
12to 2004.5.13 if the functionalities you need are removed in the simplified
13version.
14
15[2004.5.13]
16Some performace update. This is the version we used for SAT04 competition.
17Please consult our website for the detailed description.
18
19[2003.12.04]
20Fixed:
211. Various bugs in add_clause_incr(). We would like to thank Alexander
22   Smith from University of Toronto for his suggestion and experiments on
23   this issue.
242. SAT_HOOK added.
253. unset_force_terminate added.
26
27[2003.11.04]
28Fixed:
291. Compile under g++ 3.3 and above
302. Assertion error for certain instances in core extraction
313. A typo in run_till_fix. Now it takes the second argument as the max
32number of iterations to run as intended.
33
34[2003.10.09]
35Fixes in this release:
361. Bug fixed for time overflow after 2147 seconds.
372. The Perl script run_till_fix is updated such that it works for cnf
38files located in other directory.
393. zverify_df.cpp now also verifies the conflict clause given in
40resolve_trace with the one constructed by zverify itself using the
41information given in resolve_trace.
42[2003.7.22]
43NOTE: If your code is in C instead of C++, please use SAT_C.h instead of
44SAT.h as the header file.
45
46This is a new (as of June, 2003)  release of zchaff, a SAT solver from
47Princeton University. The main difference between this one and the
48previous (2001.2.17) version are listed in the following:
491. This version of zchaff has incremental SAT solving capability
50   In practice, many SAT instances are related in the sense that they only
51   differ in a small number of clauses. Zchaff can solve a set of
52   such instances incrementally, leveraging the knowledge (clauses) learned
53   from previous runs to help current runs. This feature can only be invoked
54   through the functional call interface. Please read SAT.h for more
55   information about assigning clauses with Group IDs and how to delete
56   clause or add clauses by groups.
57                                                                               
58                                   
592. This version of zchaff is certifiable
60   Now zchaff can produce a verifiable trace that can be checked by a third
61   party checker. To invoke this, modify zchaff_solver.cpp and uncomment
62   #define VERIFY_ON and compile again. Now zchaff will produce a trace
63   called resolution_trace after each run and this can be checked by
64   zverify_bf or zverify_df, which are two checkers based on breadth-first
65   and depth-first search.
66                                                                               
67                                   
683. This version of zchaff can produce an unsatisfiable core from an
69   unsatisifable formula Unsatisfiable core extraction can be useful for
70   some applications. This version of zchaff implement the idea presented
71   in our SAT 2003 paper about extracting unsat cores.
72                                                                               
734. This version can compile under gcc 3.x.
74                                   
755. This version fixed a couple of serious bugs in the previous version.
76   (But may have introduced other bugs :().
77                                                                               
78                                   
79How to Install:
80  Use "make" to compile, or "make all" to compile zchaff with extra utilities
81  (e.g. core extractor, verifier). It should work without any problem
82  under Linux, Cygwin or Solaris.
83
84  To compile a native Windows executable, Open Visual Studio .Net, create
85  a project, and add these files into the project:
86  zchaff_base.cpp,
87  zchaff_cpp_wrapper.cpp (this can be obtained by rename
88  zchaff_wrapper.wrp to zchaff_cpp_wrapper.cpp and delete all occurance of
89  "EXTERN" in the file.)
90  zchaff_dbase.cpp
91  zchaff_solver.cpp
92  zchaff_utils.cpp
93  sat_solver.cpp
94
95  Also, modify files that contain headers "sys/*.h". Delete those troublesome
96  headers, replace them with "#include <time.h>", and replace the code for
97  function get_cpu_time() with:
98
99        double get_cpu_time(void) {
100                return  (double)clock()/(double)(CLOCKS_PER_SEC);
101        }
102  This function will overflow after 2147 seconds. So the reported time
103  may not be correct. This is a temporary solution and hopefully we will fix it in
104  the future.
105 
106  MSVC will report a lot of warnings. Hopefully none is serious. :(. As
107  you suspected, zchaff is not tested under native Windows enviroment.
108  But anyway, this is the hack.
109
110How to use:
111  the main executable is zchaff. The command line is
112                zchaff CNF_FILE [TimeLimit]
113  Other executables will print out a help info when executed with no
114  argument.
115
116  run_till_fix can obtain a small core by iteratively run core extraction.
117  Do turn
118  VERIFY_ON in zchaff_solver.cpp when compile.
119
120For any questions or bug reports, please send email to
121Yogesh Mahajan at yogism@Princeton.EDU
122
123Thanks.
124
125The SAT Group at Princeton University
Note: See TracBrowser for help on using the repository browser.