*SAT 1.3 Release notes

*SAT 1.3 features two different caching mechanisms:
  • bit-matrix based caching; its distinguishing features are:
    • it can store sets of formulas encoded as sets of integers
    • it can query for subsets (supersets)
    • it can be bounded in size and, if bounded, it allows to use a FIFO politic to discharge obsolete reults
  • hash-table based caching; its distinguishing features are:
    • it can store sets of formulas encoded as sets of integers
    • features a simple and fast exact-matching access
    • it never forgets results


*SAT 1.2.3 Release notes

*SAT 1.2.3 features new defaults for the execution. Techniques like early pruning, optimized CNF conversion and caching run without the user specifying any command line parameters.


*SAT 1.2.2 Release notes

*SAT 1.2.2 features a bug fix in the normal form conversion activated with -n and automatically performed by -k1. Previous versions could not deal very well with formulae having agents other than R0 (they become R0 inadvertently).


*SAT 1.2.1 Release notes

*SAT 1.2.1 features a bug fix in the building of GLU libraries. Previous versions could not complete the installation of the libraries unless "bash" was used instead of "sh".


*SAT 1.2 Release notes

*SAT 1.2 contains some new features w.r.t older version :
  • An optimized internal CNF conversion; the *SAT command-line option -k1 activates the optimized conversion; default is to use a standard (non-optimized) conversion.
  • An emulation of Boehm's splitting heuristic; the *SAT command-line options -s2 -l21 activate the heuristic.
  • An improved algorithm for memoizing in logic K; the *SAT command-line option -m<n> makes different choices of memoizing strategies available to the user (refer to the help or to the manual for more details).
  • A parser for the TPTP-like syntax used in Tableaux99 competion; the parser may be selected at compile-time (see the manual for more details).
  • A trimmed-down, i.e. lacking bdd packages, version of the GLU library of data types (version 1.3) is bundled in the distribution package. A new shell script takes care of making and installing (locally!) the library object code and the header files needed by *SAT.
  • SATO version 3.2 featuring an improved memory handling

NOTICE!! In *SAT 1.0 the number of recursive calls (and consequently the CPU timings) are unnecessarily increased. If you are running version 1.0 of *SAT you may want to upgrade to later versions!



Back to the *SAT download page