Sat4j
  1. Sat4j
  2. SAT-39

Add the possibility to create a constraint k among n in IProblem

    Details

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

      Description

      In the pseudo boolean competition, and in many situations, it is important to be able to create a constraint that satisfies exactly k variables among n.

      The current way to proceed in Sat4j is to create both a <= and a >= constraints.

      That's fine. However, there are possibilities to encode directly such kind of constraints in the solver.

      As such, it would be great to provide a new method for that in the API, even if the current implementation remains unchanged.

        Activity

        Hide
        Daniel Le Berre added a comment -

        Added code on head r1041 to provide both both ISolver and IPBSolver an exactly constraint.

        To be more elegant, methods addAtMost and addAtLeast are now overloaded in the PB solver with coeffs which should make life easier for the end user.

        Note that in order to crete ConstGroup objects in the class Solver, it was necessary to move ConstGroup from org.sat4j.tool to org.sat4j.specs, which might break some end user code.

        Note that the Xplain and XplainPB classes need to be properly implemented now (sharing the same new variable for the two constraints used to implement an exactly constraint).

        Show
        Daniel Le Berre added a comment - Added code on head r1041 to provide both both ISolver and IPBSolver an exactly constraint. To be more elegant, methods addAtMost and addAtLeast are now overloaded in the PB solver with coeffs which should make life easier for the end user. Note that in order to crete ConstGroup objects in the class Solver, it was necessary to move ConstGroup from org.sat4j.tool to org.sat4j.specs, which might break some end user code. Note that the Xplain and XplainPB classes need to be properly implemented now (sharing the same new variable for the two constraints used to implement an exactly constraint).
        Hide
        Daniel Le Berre added a comment -

        Implemented in r1041.

        Show
        Daniel Le Berre added a comment - Implemented in r1041.

          People

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

            Dates

            • Created:
              Updated:
              Resolved:

              Development