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

Mus computation does not work when input file contains duplicated contiguous clauses (aka MUS competition bug)

    Details

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

      Description

      During the SAT 2011 competition MUS track, Sat4j MUS was found incorrect (i.e. the solution found was not an UNSAT core).

      Those instances do contain unit clauses, so it is probably the case that Sat4j MUS does not output the unit clauses in the solution line because unit clauses are handled specifically in the solver.

      That issue should not be difficult to handle.
      Incorrect answers were found on the following benchmarks:

      mus/marques-silva/product-configuration/C168_FW_UT_851.cnf
      mus/marques-silva/design-debugging/c5315-bug-gate-0.dimacs.seq.filtered.cnf
      mus/marques-silva/design-debugging/c7552-bug-gate-0.dimacs.seq.filtered.cnf
      mus/marques-silva/equivalence-checking/c2670.cnf

        Activity

        Hide
        leberre Daniel Le Berre added a comment -

        Need to be fixed before 2.3.1 release.

        Show
        leberre Daniel Le Berre added a comment - Need to be fixed before 2.3.1 release.
        Hide
        leberre Daniel Le Berre added a comment -

        Fixed in r1031. The issue was not related to unit clauses but to contiguous duplicated entries in the input file:
        $ cat ~/Bureau/C168_FW_UT_851.cnf | wc
        7492 36655 129499
        $ cat ~/Bureau/C168_FW_UT_851.cnf | uniq | wc
        7491 36652 129487
        $ cat ~/Bureau/C168_FW_UT_851.cnf | uniq -d
        -758 -134 0

        The Xplain engine removes by default duplicated contiguous entries. The new code disable that feature for MUS computation.

        Show
        leberre Daniel Le Berre added a comment - Fixed in r1031. The issue was not related to unit clauses but to contiguous duplicated entries in the input file: $ cat ~/Bureau/C168_FW_UT_851.cnf | wc 7492 36655 129499 $ cat ~/Bureau/C168_FW_UT_851.cnf | uniq | wc 7491 36652 129487 $ cat ~/Bureau/C168_FW_UT_851.cnf | uniq -d -758 -134 0 The Xplain engine removes by default duplicated contiguous entries. The new code disable that feature for MUS computation.

          People

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

            Dates

            • Created:
              Updated:
              Resolved: