Release 2.1.3

Version 2.1.3

• New interface to support propagation of assumptions. The following functions
  are available now:

  • propagate (): Applies unit propagation on the assumptions given to the
    solver previously (supposed to be called instead of solve ()).

  • get_entrailed_literals (std::vector<int> &): In case propagate ()
    returned 0 (UNKNOWN), this function returns (the subset of) those
    literals that were assigned based on the assumptions and propagation.
    Those assigned literals that are tainted on the reconstruction stack
    (due to some preprocessing) are not returned, thus it is safe to
    combine it with the formula simplifications.

• LIDRUP proofs now include information about queries that returned with
  UNKNOWN result.

Release 2.1.2

Version 2.1.2

• Fixed version number.

• Reentrant multi-threaded writing of compressed files fixed
  with 'closeform' (using 'pipe|fork|exec|closefrom') on Linux.

• New IPASIR-UP options, with the same default as in 1.1:

  • exteagerreasons where the solver eagerly asks for reasons before
    analysing conflicts instead of being lazy (default: eager)

  • exteagerrecalc where the solver recalculates the levels on the
    trail before conflict analysis (default: on). Mostly useful if
    the solver provides many propagations in a lazy fashion. Requires
    exteagerreasons to be on to have any effect.

• Fix performance regression for incremental SAT solving due to too
  eager garbage collection before any incremental call in favor of
  only doing it during variable elimination

• Fix performance regression for the SAT anniversary track.

• Slight memory usage reduction expected thanks to not allocating some
  internal array only used for proof and external propagator.

• Mobical deterministic compiled with or without logging.

• Fixed memory corruption and leaks when allocation of arena fails
  and further added support in fuzzer to trigger such bad allocations.

Release 2.1.0

• Major IPASIR-UP increment. Please be aware that some of these
  changes affect the syntax of the API, and thus updating to this
  version of CaDiCaL requires to modify the consuming code to
  accommodate to the new syntax:

  • Notification of assignments is batched into arrays and no more fixed
    flags are passed during notification (breaking change)

  • Allow clauses learned from the propagator to be deleted (see
    is_forgettable parameter and are_reasons_forgettable Boolean flag)
    (breaking change)

  • Added support to generate incremental proofs (LIDRUP) while
    using IPASIR-UP

  • Users can force to backtrack during cb_decide (see function
    force_backtrack)

  • Removed unnecessary notifications of backtrack during
    inprocessing (supposed to solve issue #92).

  • Call again cb_propagate if during final model checking a new
    clause is added.

• Added a new interface FixedAssignmentListener: Eagerly calls a
  callback whenever a variable is fixed during search.

Release 2.0.0

Release matching the CAV'24 tool paper on CaDiCaL 2.0.

• We have now a contrib directory and for starters there our
  CadiCraig interpolator, which goes through the Tracer API.

• We moved back to use the C99 flexible array member feature in
  Clause which however is not supported by all C++ compiler
  configurations, particularly if compiling in pedantic mode.
  Therefore the configure script checks for support of flexible
  array members and also has a new --no-flexible option.

• Added Dockerfile to support docker containers.

• Added --no-status to skip printing s SATISFIABLE or s UNSATISFIABLE.
  This is useful for online proof checking.

Release 1.9.5

Version 1.9.5

• Removes an unexpected performance regression on the anniversary track
  due to marking forward strengthened redundant clauses as used.

Release 1.9.4

Version 1.9.4

• Simplified code by removing reimply again (but keeping ILB).

Release 1.9.3

Version 1.9.3

• Fixed bogus notification if a user propagator is connected
  with ILB and after local search preprocessing and a second incremental
  call lead to an inconsistent trail to assumption mapping, which might
  have lead to an infinite loop (in very rare cases).

Release 1.9.2

Version 1.9.2

• Important fixes for ILB, trail-reuse and external propagation with
  assumptions.

• Restored effectiveness of Mobical and improved external mock
  propagator.

• Forced garbage collection of binary clauses before restore.

• Merge internal status and state encodings and made them consistent.

• Disabled non-verbose message if empty clause found in input.

• Improved support for IDRUP.

Release 1.9.1

Release 1.9.1

• Fixed position of 'idrup' option.

Release 1.9.0

Version 1.9.0

• Clause IDs in binary LRAT proofs are now always signed.

• Internal CNF regression suite also checks LRAT proofs now.

• Improving the OTFS heuristic (properly bumping literals and
  considering that the conflict clause is updated).

• Making progress to formal 1.9 release with minor fixes for
  different platforms and compilers.