Sat4j
  1. Sat4j
  2. SAT-37

Unit clauses not propagated again when doing multiple calls to the SAT solver

    Details

    • Type: Bug Bug
    • Status: Resolved
    • Priority: Major Major
    • Resolution: Fixed
    • Affects Version/s: 2.2.2, 2.2.3, 2.3.0
    • Fix Version/s: 2.3.1
    • Component/s: core
    • Security Level: Public (Everybody can see)
    • Labels:
      None

      Description

      The issue was described by Axel on SAT4J forum:
      http://forge.ow2.org/forum/message.php?msg_id=118089

      The short story is that unit clauses, after being propagated once, are no longer propagated on successive calls to the SAT solver because qhead was not reset to 0 but to trail.last().

        Activity

        Hide
        Daniel Le Berre added a comment -

        Proposed fix in r1029.

        Show
        Daniel Le Berre added a comment - Proposed fix in r1029.
        Hide
        Daniel Le Berre added a comment -

        The fix is ok for lazy data structures (i.e SAT with WL or HT), but does not work for non lazy ones (e.g. Pseudo-Boolean constraints).
        We need another way to check that the already propagated literals may falsify some constraints.

        Show
        Daniel Le Berre added a comment - The fix is ok for lazy data structures (i.e SAT with WL or HT), but does not work for non lazy ones (e.g. Pseudo-Boolean constraints). We need another way to check that the already propagated literals may falsify some constraints.
        Hide
        Daniel Le Berre added a comment -

        New fix in r1036. Verified using extensive functional testing.

        Show
        Daniel Le Berre added a comment - New fix in r1036. Verified using extensive functional testing.
        Hide
        Daniel Le Berre added a comment -

        Fix to be released in 2.3.1.

        Show
        Daniel Le Berre added a comment - Fix to be released in 2.3.1.

          People

          • Assignee:
            Daniel Le Berre
            Reporter:
            Daniel Le Berre
          • Votes:
            0 Vote for this issue
            Watchers:
            0 Start watching this issue

            Dates

            • Created:
              Updated:
              Resolved:

              Development