8000 Releases · arminbiere/cadical · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Releases: arminbiere/cadical

Release 2.2.0-rc2

13 Apr 06:24
@arminbiere arminbiere
rel-2.2.0-rc2
01e33a8
Compare
Choose a tag to compare
Release 2.2.0-rc2 Pre-release
Pre-release

Second release candidate for 2.2.0

It has the following new features on-top of 2.1.3

  • Renamed get_entrailed_literals by implied.

  • Congruence closure: detect AND-, XOR-, and ITE-gates encoded into
    the formula and merges equivalent outputs.

  • Bounded Variable Addition.

    • reverse of BVE, searches for clause sets with a certain structure,
      factors out common variables and uses extended resolution with a
      new variable to derive equisatisfiable clauses which replace the old ones.

    • breaking change to incremental usage. To incrementally add new
      variables to the solver, either use vars (), reserve_vars ()
      or reserve_difference (), see specification in cadical.hpp.
      As a hot-fix, disable with set ('factor', 0)

  • Clausal Sweeping.

    • introducing the 'kitten' solver to cadical. Enables semantic search
      for equivalences in sub-parts of the formula.

  • Ticks.

  • Improved lucky, by allowing it to do several conflicts.

  • New light preprocessing round on with lucky, congruence, factor, and
    a new (very limited) BVE (fast elim). Fast elimination is never run
    again and normal BVE is used instead. Lucky is run before and after
    preprocessing.

  • Small extension to gate extraction in BVE, now able to extract
    semantic definitions using 'kitten'
    (off by default set ('elimdef', 1) to enable).

Loading

Release 2.1.3

10 Feb 15:45
@arminbiere arminbiere
rel-2.1.3
f13d744
Compare
Choose a tag to compare
Release 2.1.3 Latest
Latest

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.

Important (behavior changing) bug-fix #108: val now follows the IPASIR-UP interface. This changes the return value for negative literals.

Assets 2
Loading

Release 2.1.2

19 Dec 14:20
@arminbiere arminbiere
rel-2.1.2
3ff42f0
Compare
Choose a tag to compare
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.

Loading

Release 2.1.0

09 Oct 05:37
@arminbiere arminbiere
rel-2.1.0
31f9aae
Compare
Choose a tag to compare
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.

Loading

Release 2.0.0

18 Jun 11:43
@arminbiere arminbiere
rel-2.0.0
2df7b7f
Compare
Choose a tag to compare
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.

Loading

Release 1.9.5

01 Mar 09:39
@arminbiere arminbiere
rel-1.9.5
1462073
Compare
Choose a tag to compare
Release 1.9.5
10482

Version 1.9.5

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

Release 1.9.4

05 Jan 10:01
@arminbiere arminbiere
rel-1.9.4
e71bd58
Compare
Choose a tag to compare
Release 1.9.4

Version 1.9.4

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

Release 1.9.3

18 Dec 18:28
@arminbiere arminbiere
rel-1.9.3
3d346f7
Compare
Choose a tag to compare
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).
Loading

Release 1.9.2

17 Dec 16:16
@arminbiere arminbiere
rel-1.9.2
ac48dd6
Compare
Choose a tag to compare
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.

Loading

Release 1.9.1

28 Nov 18:21
@arminbiere arminbiere
rel-1.9.1
24d0475
Compare
Choose a tag to compare
Release 1.9.1

Release 1.9.1

  • Fixed position of 'idrup' option.
Loading
0