Uploaded image for project: 'Sat4j'
  1. Sat4j
  2. SAT-41

Use a specific data structure to locate efficiently the weight associated to a literal in a counter based constraint

    Details

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

      Description

      After checking the reason for inefficiency of Sat4j on specific benchmarks, it turns out that large counter based constraints have a bottleneck:

      // finding the index for p in the array of literals
      int indiceP = 0;
      while ((lits[indiceP] ^ 1) != p)
      indiceP++;

      Using an auxiliary array or map to store the location of the literals instead of going through that loop will probably make the propagation and undo much faster.
      (hint: use an array when the size of the constraint contains at least half of the variables, else use a map).

        Activity

        Hide
        leberre Daniel Le Berre added a comment -

        Actually, the main point is not to locate the literal itself, but to locate its weight to update the slack.
        The point is thus to provide an efficient way to retrieve the weight associated to a literal.

        Show
        leberre Daniel Le Berre added a comment - Actually, the main point is not to locate the literal itself, but to locate its weight to update the slack. The point is thus to provide an efficient way to retrieve the weight associated to a literal.
        Hide
        leberre Daniel Le Berre added a comment -

        Fix available in r1060. Waiting for functional tests results.

        Show
        leberre Daniel Le Berre added a comment - Fix available in r1060. Waiting for functional tests results.
        Hide
        leberre Daniel Le Berre added a comment -

        Functional tests passed.

        Show
        leberre Daniel Le Berre added a comment - Functional tests passed.

          People

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

            Dates

            • Created:
              Updated:
              Resolved: