Release 2.1.1

Version 2.1.1

• 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.

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.