Pseudo-Boolean Constraints — at-most/at-least/exact `K-out-of-N`

[Fe-r-oz]

If this request is about a new feature, please describe what you would like to see implemented.

How about adding built-in support for pseudo-boolean constraints in Satisfiability.jl, similar to the PbEq, PbLe, and PbGe functionality available in the Z3 theorem prover. I would be pleased to work on this, should you approve the feature request.

These constraints allow users to efficiently express conditions such as:

• PbEq: Exactly $K$ out of $N$ are true — $\text{PbEq}(((x_1, 1), (x_2, 1), \ldots, (x_N, 1)), K)$ — $x_1 + x_2 + \cdots + x_N = K$
• PbLe: At most $K$ out of $N$ are true — $\text{PbLe}(((x_1, 1), (x_2, 1), \ldots, (x_N, 1)), K)$ — $x_1 + x_2 + \cdots + x_N \leq K$
• PbGe: At least $K$ out of $N$ are true — $\text{PbGe}(((x_1, 1), (x_2, 1), \ldots, (x_N, 1)), K)$ — $x_1 + x_2 + \cdots + x_N \geq K$

Proposed syntax example

To express these constraints in Julia, maybe we could use the following syntax. Please let me know your feedback, is this the reasonable API:

• PbEq (exactly K true):

  assert!(solver, PbEq([(x[i], 1) for i in 1:N], K))

• PbLe (at most K true):

  assert!(solver, PbLe([(x[i], 1) for i in 1:N], K))

• PbGe (at least K true):

  assert!(solver, PbGe([(x[i], 1) for i in 1:N], K))

If this request is about an existing feature, what is the current behavior and what is the use case for changing the behavior?

Currently,Satisfiability.jldoes not provide a dedicated API for pseudo-boolean constraints . Users must encode pseudo-boolean constraints manually by introducing auxiliary variables and additional constraints, which can be tedious and less efficient. According to this discussion, to express a 1-out-of-N constraint, one can manually assert that at least one variable is true (or(x₁, ..., xₙ)) and that at most one variable is true (not(and(xᵢ, xⱼ)) for all pairs of distinct indices i and j). While there are various ways to manually encode such constraints (including for K-out-of-N), having built-in support in the solver maybe efficient than encoding them manually. Built-in support would therefore simplify problem modeling particularly for large-scale problems.

Additional context

Inspiration: https://stackoverflow.com/questions/43081929/k-out-of-n-constraint-in-z3py

SMT-LIB syntax: Is there a way to access PbEq/PbLe/PgGe via smt-lib?

Ways to manually express the 1-out-of-N and K-out-of-N constraints Encoding 1-out-of-n constraint for SAT solvers

Some python examples for API cross-reference:

from z3 import *

x1, x2, x3, x4 = Bools('x1 x2 x3 x4')

s = Solver()
s.add(PbEq([(x1, 1), (x2, 1), (x3, 1), (x4, 1)], 2))
print(s.check())  # Output: sat
print(s.model())  # Example: {x1: True, x2: True, x3: False, x4: False}

output

sat
[x3 = False, x2 = True, x1 = False, x4 = True]

import z3

# Function to create and solve the solver with given constraints
def solve_pseudo_boolean_constraint(constraint_type, bvars, K):
    s = z3.Solver()
    
    if constraint_type == "PbEq":
        # Exactly K variables should be true
        s.add(z3.PbEq([(x, 1) for x in bvars], K))
    elif constraint_type == "PbLe":
        # At most K variables should be true
        s.add(z3.PbLe([(x, 1) for x in bvars], K))
    elif constraint_type == "PbGe":
        # At least K variables should be true
        s.add(z3.PbGe([(x, 1) for x in bvars], K))
    else:
        raise ValueError("Invalid constraint type. Use 'PbEq', 'PbLe', or 'PbGe'.")
    
    # Check satisfiability
    result = s.check()
    if result == z3.sat:
        model = s.model()
        print(f"{constraint_type} is SAT")
        for var in bvars:
            print(f"{var} = {model[var]}")
    else:
        print(f"{constraint_type} is UNSAT")

# Create 10 boolean variables
bvars = [z3.Bool(f"Var {i}") for i in range(5)]

# Example 1: Exactly 3 of the variables should be true (PbEq)
solve_pseudo_boolean_constraint("PbEq", bvars, 3)

# Example 2: At most 3 of the variables should be true (PbLe)
solve_pseudo_boolean_constraint("PbLe", bvars, 3)

# Example 3: At least 3 of the variables should be true (PbGe)
solve_pseudo_boolean_constraint("PbGe", bvars, 3)

output

PbEq is SAT
Var 0 = True
Var 1 = True
Var 2 = True
Var 3 = False
Var 4 = False
PbLe is SAT
Var 0 = True
Var 1 = True
Var 2 = True
Var 3 = False
Var 4 = False
PbGe is SAT
Var 0 = True
Var 1 = True
Var 2 = True
Var 3 = False
Var 4 = False

[elsoroka]

This makes sense to me. I appreciate that someone is taking an interest in this package and making these suggestions.
One question here is that it looks like Z3 has introduced the syntactic sugar at-most and at-least for these operations, but they can be expressed in other solvers using less concise operations. So there is a choice here:

• Translate PbEq, PbLe and PbGe to Z3's at-most/at-least/exact functions, which won't be supported by other solvers
• Translate to the more unwieldy SMT format understood by all solvers (may be hard to verify this is done correctly).

I think adding a way for Satisfiability.jl to know what functions are supported by what solvers would be interesting, but hasn't been implemented yet. So there isn't a wrong answer here, just which seems more feasible.

[jchanke]

@Fe-r-oz thanks for suggesting this, and thanks @elsoroka for explaining the options! It seems like we have a layer of abstraction between

the raw Julia code <=> the AbstractExpr syntax tree <=> the generated SMT-LIB code

It seems to me like the first translation happens in the *Expr.jl files (e.g. BoolExpr.jl, IntExpr.jl) and the second happens in the smt and smt! functions in smt_representation.jl.

So one idea is to have a common layer handling the translation to an AbstractExpr, and handle different translation strategies in a single place (the smt function in smt_representation.jl).