zchaff64/README

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