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.

Release 1.8.0

Version 1.8.0

• Explicit Solver::clause functions to simplify clause addition.

• More fine-grained handling of printing proof size information by
  adding bool print = false flags to the flush_proof_trace and
  the close_proof_trace API calls. The former prints the number
  of addition and deletion steps, while the latter prints the size
  of the proof size (and the actual number of bytes if compressed).
  The main effect is that by default printing of proof size disabled
  for API usage but enabled for the stand-alone solver.

Release 1.7.5

Version 1.7.5

• Decreased verbosity level for printing proof size.