Skip to content

Performance improvement idea for cardinality constraint encoders #1

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Performance improvement idea for cardinality constraint encoders #1

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0cc8e39
Use itertools.combinations generator for subsets_of_size_k
drasive Jan 16, 2023
534da82
Optimize encode_at_most_k_constraint_binomial
drasive Jan 16, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 5 additions & 27 deletions cscl/cardinality_constraint_encoders.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,35 +8,16 @@
import itertools


def subsets_of_size_k(collection, k):
def subsets_of_size_k(collection: list, k: int):
"""
Computes all subsets of size k.

:param collection: A list.
:param k: A non-negative integer.
:return: A list containing all size-k subsets of collection.
"""
# Potential optimization: make this a generator

assert(k >= 0)

# Base cases:
if k > len(collection):
return []
if k == 0:
return [[]]
if k == len(collection):
return [collection]

next_smaller_subsets = subsets_of_size_k(collection[1:], k-1)
next_subsets = subsets_of_size_k(collection[1:], k)

def extend_list(lst, item):
lst_copy = lst[:]
lst_copy.append(item)
return lst_copy

return next_subsets + list(map(lambda x: extend_list(x, collection[0]), next_smaller_subsets))

return map(list, itertools.combinations(collection, k))


def encode_at_most_k_constraint_binomial(lit_factory: CNFLiteralFactory, k: int, constrained_lits: list):
Expand All @@ -53,10 +34,7 @@ def encode_at_most_k_constraint_binomial(lit_factory: CNFLiteralFactory, k: int,
:return: The constraint in CNF clausal form, a list of lists of literals.
"""

result = []
for subset in subsets_of_size_k(constrained_lits, k+1):
result.append(list(map(lambda x: -x, subset)))
return result
return subsets_of_size_k([ -x for x in constrained_lits], k+1)


def encode_at_most_k_constraint_ltseq(lit_factory: CNFLiteralFactory, k: int, constrained_lits: list):
Expand Down Expand Up @@ -208,7 +186,7 @@ def encode_at_most_k_constraint_commander(lit_factory: CNFLiteralFactory, k: int
for idx, group in enumerate(groups):
group_with_commanders = group + [-c for c in commanders[idx]]
group_constraints += encode_exactly_k_constraint(lit_factory, k, group_with_commanders,
encode_at_most_k_constraint_binomial)
list(encode_at_most_k_constraint_binomial))

# Break symmetries by ordering the commander literals:
order_commanders = [[-group_commanders[i], group_commanders[i+1]]
Expand Down