# using_symmetries_to_lift_satisfiability_checking__a23c41f6.pdf

Using Symmetries to Lift Satisfiability Checking

Pierre Carbonnelle1, Gottfried Schenner2, Maurice Bruynooghe1, Bart Bogaerts3, Marc Denecker1

1KU Leuven, Belgium 2Siemens, Austria 3Vrije Universiteit Brussels, Belgium {pierre.carbonnelle, maurice.bruynooghe, marc.denecker}@kuleuven.be, gottfried.schenner@siemens.com, bart.bogaerts@vub.be

We analyze how symmetries can be used to compress structures (also known as interpretations) onto a smaller domain without loss of information. This analysis suggests the possibility to solve satisfiability problems in the compressed domain for better performance. Thus, we propose a 2-step novel method: (i) the sentence to be satisfied is automatically translated into an equisatisfiable sentence over a lifted vocabulary that allows domain compression; (ii) satisfiability of the lifted sentence is checked by growing the (initially unknown) compressed domain until a satisfying structure is found. The key issue is to ensure that this satisfying structure can always be expanded into an uncompressed structure that satisfies the original sentence to be satisfied. We present an adequate translation for sentences in typed first-order logic extended with aggregates. Our experimental evaluation shows large speedups for generative configuration problems. The method also has applications in the verification of software operating on complex data structures. Our results justify further research in automatic translation of sentences for symmetry reduction.

1 Introduction

In made-to-order manufacturing, the configuration problem is the problem of finding a configuration of components that satisfies the customer requirements and feasibility constraints (Felfernig et al. 2014). Such problems can be solved by choosing a formal vocabulary and by representing the customer requirements and the feasibility criteria as a logic sentence to be satisfied. A structure satisfying the sentence (a model) represents an acceptable configuration. Methods to solve configuration problems do not scale well, and various heuristics have been used to improve performance (Schenner and Taupe 2017). Configurations often have components that are interchangeable. They are the source of many redundancies in the search space that negatively impact performance. The standard approach is to add symmetry breaking rules (Crawford et al. 1996). Here, we use another approach: we reformulate the problem to reduce symmetries (Gent, Petrie, and Puget 2006). This approach has been less studied, and is more an art than a science.

Copyright 2024, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

We observed that solutions to configuration problems can be compressed in what we call a lifted model , and that the solution of the original problem can be obtained by expanding the lifted model. This suggested that configuration problems, and, more generally, satisfiability problems, could be solved in the compressed domain: if the compressed domain is significantly smaller, it could lead to better performance. As a toy example, consider the following pigeonhole problem: given 10 pigeons and 5 pigeonholes, assign each pigeon to a pigeonhole such that each hole has (at most) 2 pigeons. With the appropriate vocabulary, a solution is:

Pigeon tp1, . . . , p10u (1) Hole th1, . . . , h5u (2) is In tpp1, h1q, pp2, h2q, . . . , pp5, h5q, (3) pp6, h1q, pp7, h2q, . . . , pp10, h5qu

Note the symmetries: another solution is obtained by exchanging 2 pigeons or 2 holes in the interpretation of is In. This solution can be compressed to:

Pigeon tp1u (4) Hole th1u (5) mul tp1 ÞÑ 10, h1 ÞÑ 5u (6) is In tpp1, h1qu (7)

where the mul function indicates how many concrete domain elements each lifted domain element represents, and thus allows the domain compression. The lifted pigeon (resp. hole) represents 10 concrete pigeons (resp. 5 concrete holes). Even though the compressed structure only has 2 domain elements (p1, h1, excluding the naturals), it contains enough information to allow us to expand it into a model isomorphic to the original model. Following the theory we develop in Section 3, the expansion is as follows:

p1 p1, . . . , p10 h1 h1, . . . , h5 pp1, h1q tpp1, h1q, . . . , pp5, h5q, pp6, h1q, . . . , pp10, h5qu

Furthermore, in Section 4, we present a translation of sentences in typed first-order logic extended with aggregates into sentences that allow domain compression. We show that

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)

a sentence in that language is equisatisfiable with its translation, given the number of concrete elements in each type: if either one is satisfiable, the other one is too. This analysis allows us to solve satisfiability problems in the compressed domain. The novel method operates in two steps: (i) the sentence to be satisfied is automatically translated into a lifted sentence over the lifted vocabulary; (ii) satisfiability of the lifted sentence is checked by step-wise growing the compressed domain1 until a satisfying structure is found. Crucially, this satisfying structure can always be expanded into a model of the original sentence. Notice that the lifted model for a variation of the pigeonhole problem above with 100 times more pigeons and holes has the same number of lifted domain elements as the base case: the multiplicity of each lifted domain element is simply multiplied by 100. As a result, and unlike traditional symmetry breaking methods, our method solves that pigeonhole problem in constant time with respect to the domain size (excluding the naturals). We evaluate this method by comparing the time needed to find solutions for generative configuration problems discussed in the literature. Our method has significantly better performance than the traditional one for problems whose solution can be substantially compressed. Our paper is structured as follows: after introducing our notation, we analyze how symmetries can be used to compress structures onto a smaller domain without loss of information (Section 3), and describe how to lift a concrete sentence so that it is equisatisfiable with the lifted sentence (Section 4); we describe the method, evaluate it on generative configuration problems (Section 5), and discuss applications in Boolean Algebra of sets with Presburger Arithmetic (BAPA) (Section 6) before concluding with a discussion.

2 Preliminaries

This section introduces the logic language supported by our method, and the concept of permutation of a structure.

Typed First Order Logic With Aggregates

We call FO(Type, Aggregate) the language we support. We assume familiarity with first order logic (Enderton 1972). A vocabulary Σ is a set of type, predicate, and function symbols. Predicates and functions have a type signature (e.g. f : T Ñ T, where T denotes a tuple of types). Some symbols are pre-defined: type B (booleans), Q (rationals), equality, arithmetic operators and arithmetic comparisons. Terms and formulae are constructed from symbols according to the usual FO syntactic rules. We also allow sum aggregates (written as ř

x P T :ϕ t or as ř x P T pt if ϕq). A cardinality aggregate #t x P T | ϕu is a shorthand for a sum aggregate whose term t is 1. Quantification and aggregation can only be over finite types. Terms and formulas must be well-typed. A formula without free-variable is called a sentence. A Σ-structure I , consists of a domain and an interpretation of each symbol of vocabulary Σ. The interpretations

1An iterative method is required because the size of the compressed domain is not known in advance.

of types are disjoint and finite (except QI which is infinite). The interpretation p I of a predicate p is a set of tuples d of domain elements of appropriate types. The interpretation f I of a function f is a set of pairs p d, dq, also denoted by d ÞÑ d. An extended structure is a structure with a variable assignment, i.e., with a mapping from variable x to values d, denoted r x : ds. The value of a formula or term in an extended structure is computed according to the usual FO semantic rules, which require that the interpretation of function symbols be total functions over their domain. A Σ-structure is a model of a sentence if the value of the sentence is true in the structure, i.e., if it satisfies it. Satisfiability checking in typed FO logic is the problem of deciding whether a sentence has a model, given the interpretation of the types.

Permutations and Orbits

A permutation of a set is a bijection from that set to itself. We denote a permutation by π, and its inverse by π 1. The identity permutation, π0, maps every element of the set to itself. The order of a permutation is the smallest positive number n such that πn is the identity permutation. Hence, the nth permutation of an element is equal to its nth modulo the order permutation. Cycles are permutations that map elements in a cyclic fashion. A cycle is denoted by pd1d2 dnq. A permutation over a finite set has a unique decomposition into disjoint cycles. Its order is the least common multiple (lcm) of the length of its cycles. The permutation of a tuple of elements d is denoted by πp dq and is equal to pπpd1q, ..., πpdnqq. The π-orbit of an element d (resp. of a tuple of elements d) is the set of its repeated permutations oπpdq tπipdq | i P Nu (resp. oπp dq tπip dq | i P Nu).

3 Lossless Compression of Structures

In this section, we discuss how, and when, a concrete structure with symmetries can be compressed into a lifted structure over a smaller domain without loss of information, and how a lifted structure can be expanded into a concrete one. Symmetries in a structure I are described by a domain permutation π (Devriendt et al. 2016): it is a permutation of the domain of I that maps numbers to themselves, and other domain elements in T I to domain elements in T I. Since numbers are mapped to themselves by the permutation, and since types besides Q are finite, the permutation is composed of cycles. A domain permutation induces a structure transformation. The interpretation in the transformed structure, denoted πp Iq, is defined as follows:

the type of domain element d in πp Iq is its type in I;

a tuple d1 is in the transformed interpretation of predicate symbol p if and only if π 1p d1q is in the original interpretation of p: pπp Iq t d1 | π 1p d1q P p Iu tπp dq | d P p Iu;

a tuple p d1 ÞÑ d1q is in the transformed interpretation of function symbol f if and only if π 1p d1q ÞÑ π 1pd1q is

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)

in the original interpretation of f:

f πp Iq tp d1 ÞÑ d1q | pπ 1p d1q ÞÑ π 1pd1qq P f Iu

tpπp dq ÞÑ πpdqq | p d ÞÑ dq P f Iu

Definition 1 (Automorphism) A permutation π that transforms a structure into itself, i.e., such that I πp Iq, is an automorphism of the structure. Every structure has at least one automorphism: the identity domain permutation. Note that an automorphism maps the interpretation of any constant to itself, i.e., c Ipq πpc Ipqq. Thus, the length of the cycle containing c Ipq is 1. We introduce the new concept of backbone, which plays a critical role in the compression that we propose. Essentially, a backbone for an automorphism of I is a set of domain elements obtained by picking one element in each cycle, such that the interpretation of any symbol can be reconstructed from its interpretation restricted to the backbone, by applying the automorphism repeatedly. Formally: Definition 2 (Backbone) A backbone for an automorphism π of I is a subset S of the domain of I such that: each cycle C of π has exactly one element in S; for each predicate p{n P Σ, p I is the union of the πorbits of the tuples in p I X Sn, i.e.,

d Pp I XSn oπp dq tπip dq | d P p I X Sn, i P Nu

for each function f{n P Σ, f I is the union of the π-orbits of the tuples in f I X p Sn ˆ Sq, i.e,

p dÞÑdq Pf I Xp SnˆSq oπp d ÞÑ dq (9)

tπip d ÞÑ dq | p d ÞÑ dq P f I X p Sn ˆ Sq, i P Nu

Example 1 For the pigeonhole example in the introduction of the paper, a backbone of automorphism pp1 p10qph1 h5q is S tp1, h1u. Another is S tp2, h2u. In all structures, the set of domain elements is a trivial backbone for the identity automorphism. However, not all automorphisms have a backbone. Example 2 Let ta, bu be a (concrete) domain with one type T. In structure I1 (resp. I2), function symbol f : T Ñ T is interpreted as ta ÞÑ a, b ÞÑ bu (resp. ta ÞÑ b, b ÞÑ au). Permutation pabq is an automorphism of both structures. The only two subsets S satisfying the first condition of backbone for pabq are tau and tbu. Since f I1 can be reconstructed from f I1 X p S ˆ Sq for both subsets S, both subsets are backbones of I1. However, none is a backbone of I2 (because f I2 X p S ˆ Sq H for both candidate sets S). A backbone enables us to lift a structure into a structure with a smaller domain, as we now describe. Definition 3 (Lifted vocabulary) For a vocabulary Σ, its lifted vocabulary Σl consists of the symbols of Σ and, for any type T of Σ, a symbol mul T : T Ñ N, called the multiplicity function for T.

We will drop the subscript T in the function symbol mul T when this is unambiguous.

Definition 4 (Lifted structure) Let I be a Σ-structure with an automorphism π having backbone S. A lifted structure L derived from I is a Σl-structure such that:

its domain is S, called the lifted domain; for each type predicate T, T L T I X S; for each predicate symbol p{n, p L p I X Sn; for each function symbol f{n, f L f I X p Sn ˆ Sq; for each l P S, mul Lplq |oπplq|, the size of the π-orbit of l in I.

Example 3 Continuing the pigeonhole problem, the lifted structure is described by Equations 4-7.

Given the lifted structure L derived from I and the automorphism π on the concrete domain I, one can reconstruct I, i.e., one can expand the lifted interpretations of the type, predicate and function symbols, essentially by closing them under repeated application of π. Formally,

expπp T Lq ď

l PT L oπplq tπiplq | l P T L, i P Nu (10)

expπpp Lq ď

l Pp L oπp lq tπip lq | l P p L, i P Nu (11)

expπpf Lq ď

p lÞÑlq Pf L oπp l ÞÑ lq

tπip l ÞÑ lq | p l ÞÑ lq P f L, i P Nu. (12)

Example 4 Continuing the pigeonhole problem, the expansion of the lifted structure described by Equations 4-7 for automorphism pp1 p10qph1 h5q is the structure described by Equations 1-3.

In our approach, we need to find lifted structures that can be expanded into concrete ones. We observe that there is a simple construction to expand any lifted Σl-structure L with lifted domain S that results sometimes (but not always) in a concrete structure I with an automorphism π having backbone S. This construction is as follows.

Definition 5 (Expansion of lifted domain) An expansion of the domain S tli | i P Nu of the lifted Σl-structure L is a set D tdj i | Di, j P N : li P S 1 ď j ď Mul Lpliqu such that the dj i are distinct and @i : d1 i li.

We call d1 i a base element. Notice that lifted domain elements with multiplicity zero have no image in D.2 We define a permutation on the set D having the cycles pli, d2 i . . . d Mul Lpliq i q:

Definition 6 (Permutation of the expanded domain) The permutation of an expansion D of a lifted domain is the function π : D ÞÑ D such that πpdj iq dj 1 i for

1 ď j ă Mul Lpliq 1, and πpd Mul Lpliq i q d1 i .

2Null multiplicities will prove useful for iterative methods in Section 5

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)

The expansion of a lifted tuple l in a lifted structure is its π-orbit: expπp lq oπp lq tπip lq|i P Nu (13)

if none of the expansion of its elements is empty, and is empty otherwise. The concrete interpretation of symbols is obtained by expanding the tuples in their lifted interpretations, as in Equations (10-12). It follows from the correspondence between Definition 2 and Equations (10-12) that, if π and I are constructed from L in this way, and if I is actually a structure, then S is a backbone of π in I. When L only has strictly positive multiplicities, a lifted structure derived from the expansion of L will be isomorphic to L: in some sense, the compression is lossless. However, I may not be a structure because the interpretation of a function symbol in I might not be a total function on its domain, as the following example shows.

Example 5 Consider the lifted structure L with domain S ta, bu, with types AL tau, BL tbu, and for f : A ˆ A ÞÑ B, f L tpa, aq ÞÑ bu. Finally, let mulpaq mulpbq 2, The expanded domain is ta1, a2, b1, b2u with permutation pa1a2qpb1b2q. The expansion of f L is tpa1, a1q ÞÑ b1, pa2, a2q ÞÑ b2u. There is no entry for pa1, a2q, so the expansion is not a total function. Consider now the lifted structure L with domain S ta, bu, with type AL tau, BL tbu, for f : A ÞÑ B, f L ta ÞÑ bu. Finally, mulpaq 1, mulpbq 2. The expanded domain is ta1, b1, b2u with permutation pa1qpb1b2q. The expansion of f L is ta1 ÞÑ b1, a1 ÞÑ b2u. This expansion gives two different values for a1, so it is not a function.

To distinguish lifted structures that can be expanded into concrete ones from those that cannot, we introduce the notion of regularity.

Definition 7 (Regular function, regular lifted structure) The lifted interpretation of a function symbol is regular if its expansion defines a total function in the concrete domain, i.e., if it specifies exactly one image for every tuple in the concrete domain. A regular lifted structure is a lifted structure in which the interpretation of each function symbol is regular.

Now, we define the expansion of a regular lifted structure:

Definition 8 (Expansion of a regular lifted structure) Let L be a regular lifted structure over a lifted vocabulary. Then, I, the expansion of L, is the structure over the concrete vocabulary defined as follows:

its domain is the expansion of the lifted domain, having permutation π derived from L; for each type symbol T, T I expπp T Lq; for each predicate symbol p, p I expπpp Lq; for each function symbol f, f I expπpf Lq.

The expansion of a regular lifted structure does not involve any search. The time needed for this expansion is generally negligible (e.g., less than 0.1 sec for 10,000 concrete domain elements). To further characterize regular functions, we introduce the concept of regular tuples. We use Mulpl1, . . . , lnq (resp.

Lcmpl1, . . . , lnq) as a shorthand for the product of the multiplicities of li (resp. their least common multiple lcm). First, we observe that the size of the expansion (Equation 13) of a tuple l is finite: it is the order of the permutation defined by the cycles of its elements, i.e., Lcmpl1, . . . , lnq.3 Also, the expansion has at most Mulpl1, . . . , lnq tuples; it is then the cross-product of the expansions of its elements. When those two numbers are identical, we say that the tuple is regular.

Definition 9 (Regular lifted tuple) A lifted tuple is regular if and only if its expansion is the cross-product of the expansion of its elements.

Example 6 Let pa, bq be a tuple of two lifted domain elements with mulpaq 2 and mulpbq 4. Its expansion is tpa1, b1q, pa2, b2q, pa1, b3q, pa2, b4qu, of size Lcmp2, 4q 4. Note that, e.g., the tuple pa1, b2q does not belong to the expansion: thus, pa, bq is not regular. It is regular when mulpbq 0 (the expansion of b and of pa, bq are empty), or when, e.g., mulpbq 3 (the expansion is tpa1, b1q, pa2, b2q, pa1, b3q, pa2, b1q, pa1, b2q, pa2, b3qu), of size Lcmp2, 3q 6.

Nullary and unary tuples are always regular. An n-ary tuple is regular when one of its elements has multiplicity zero, or every pair of its elements have multiplicities that are coprime.

Proposition 1 (Regular function) A function f L is regular if, for all tuples l in the domain of f L, it holds that (i) l is regular, and (ii) the multiplicity of l is a multiple of the multiplicity of its image.

Proof 1 First, we show that the expansion of f L gives at least one value for every tuple d in the concrete domain of f. Each element di of d is in the expansion of a lifted domain element li P T L i . Tuple l pl1, , lnq P T L is in the lifted domain of f L as f L is total; it is regular by (i), hence d is in its expansion and f Ip dq is in expπpf Lp lqq. Next, we show that the expansion gives at most one value for every tuple d in the concrete domain of f. Let d be in the expansion of l, with Lcmp lq m Mulp lq by (i). We thus have 0 ă m. The expansion of f L contains the pairs πip l ÞÑ f Lp lqq and πi nˆmp l ÞÑ f Lp lqq, for any l in the domain of f L, and for any i and n. The first element of these two pairs are identical by definition of m; the second elements are identical by (ii).

4 Translation Into a Lifted Sentence We now present a translation of a sentence in FO(Type, Aggregate) into a sentence that allows domain compression, such that the translation is equisatisfiable with the original. The translation χpϕq of a sentence ϕ is the conjunction of (i) the transformed sentence χpϕq, and (ii) sentences expressing regularity conditions. The transformation χpeq of an expression e is defined recursively in Table ??. The left column shows the possible syntactical forms in the concrete sentence; the middle column shows the transformation; the third column shows the

3Taking the convention that the lcm of a tuple of numbers containing 0 is 0.

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)

regularity constraints added to the translation. The bottom part of the table shows the regularity constraints added for each function symbol in the vocabulary to ensure that the function interpretations are regular (Proposition 1). Note that sum aggregates and quantified formulas are transformed by specialized rules (Rules 18, 26, 27) when possible (see table footnote), and by general rules (Rules 19, 28, 29) otherwise. Generally, it is beneficial to do equivalence-preserving transformations of sentences to obtain sentences of the form allowing application of specialized rules. The specialized rules do not require the translation of pp t, sq by Rule 21, thus avoiding the regularity constraint RCpppχp t, sqqq. E.g., for the atom t s, this regularity constraint would enforce mulptq mulpsq 1 for each tuple pt, sq in the lifted equality relation, significantly reducing the possibility of compression. The transformation of a sentence consists of adding 0 ă Mulp xq filters (to cope with lifted domains elements with an empty expansion) and of multiplying the term t in an aggregate term with some decompression factor: in Rule 19, it is the number Mulp xq of possible concrete variable assignments; in Rule 18, it is that number multiplied by the fraction of concrete assignments that make pp t, sq true. The regularity condition added for an atom (Rule 21) ensures the translated atom is equisatisfiable with the original atom.

Example 7 The sentence at most 2 pigeons in each hole : @h P Hole : #tp P Pigeon | is Inpp, hqu ď 2. Its transformation by Rule 18 (with ϕ true) and 28 is:4 @h P Hole : 0 ă mulphq ñ ř p PPigeonp Lcmpp,hq

mulphq if 0 ă mulppq is Inpp, hqq ď 2.

Theorem 1 (Equisatisfiability) An FO(Type, Aggregate) sentence is equisatisfiable with its translation, given the number of concrete elements in each type.

If I is a model of the sentence, then L constructed by extending I by setting all multiplicities to one is a model of the translated sentence: indeed, the added constraints are trivially satisfied, and the translated sentence is equivalent to the original one. Proving the converse is long and complex. It is proved by structural induction of two invariants over the syntactic tree of the sentence to be satisfied: (i) a transformed formula χpϕq is true in L under some variable assignment r x : lxs if and only if ϕ is true in I under any variable assignments r x : dxs such that each dxi is in the expansion of lxi (ii) similarly, if a transformed term χptq has value l in the lifted structure L under some variable assignment r x : lxs, then, the expansion of the value l contains the value of the term t in I (the expansion of L), for any variable assignment r x : dxs such that each dxi is in the expansion of lxi. This property holds only when the regularity constraints given in Table ?? hold in the lifted structure. This explains why these constraints are added to the transformed sentence. The proof is in the supplementary material (Carbonnelle et al. 2023).

4Recall that a cardinality aggregate is a shorthand for a sum aggregate whose term is 1.

5 Evaluation of the Method

Implementation The goal of the evaluation is to show that there are satisfiability problems where substantial compression of the domain is possible, and that the lifted models can indeed be expanded into concrete ones. A problem is solved iteratively, starting with empty lifted domains. Given a domain, the lifted sentence is reduced to a propositional sentence and its satisfiability is determined with a standard satisfiability solver capable of arithmetic reasoning. If the sentence is unsatisfiable with this domain, the sentence is reduced to a minimal unsatisfiable formula (Lynce and Marques-Silva 2004), and the domains of the types used in that formula are extended with one element. This process is repeated until a model of the sentence is found (it does not terminate if the original sentence is unsatisfiable for any domain size, unless one imposes an upper limit on the size of lifted domains). In many experiments, it was sufficient to support the special Rules 18, 26-27 for the case where the atom p is of the form t1 s (e.g., hole Of ppq hq. Then, the transformation of a sum aggregate per Rule 18 simplifies to:

1 mulpχpsqq

x P T p Mulp xq ˆ χptq (32)

if 0 ă Mulp xq χpt1q χpsq χpϕqq

This formula does not use the lcm function, which is not supported natively by solvers. In other experiments, we used an interpretation table for lcm. Problems are expressed in FOp q5, a Knowledge Representation language with support for types, subtypes, and aggregates.6 A FOp q (lifted) sentence is translated by IDPZ3 (Carbonnelle et al. 2022) for use with the Z3 SMT solver (de Moura and Bjørner 2008). The overhead of this translation is negligible. The source code of our examples is available on Git Lab7. Tests were run using Z3 v4.12.1 on an Intel Core i7-8850H CPU at 2.60GHz with 12 cores, running Ubuntu 22.04 with 16 GB RAM. We run a modified version of IDP-Z3 v0.10.8 on Python 3.10.

Pigeonhole problem To validate the approach, we first consider the satisfiability problem of assigning each pigeon to one pigeonhole, such that each pigeonhole holds (at most) 2 pigeons. Function hole Of : Pigeon ÞÑ Hole is used to represent this relation. When there are twice as many pigeons as holes, the lifted solution has 1 lifted pigeon and 1 lifted hole, as shown in the introduction of the paper. As expected, the time needed to solve the lifted problem is almost constant when it is satisfiable. The correct multiplicities are found quickly by Z3 using a sub-solver specialized for arithmetic. For example, with 10,000 pigeons, the lifted sentence is solved in only

5https://fo-dot.readthedocs.io/ 6Subtypes are subsets of types, and are declared as unary predicates in FOp q. Subtypes can be used where types are used: in the type signature of a symbol and in quantification. 7https://gitlab.com/pierre.carbonnelle/idp-z3-generative

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)

Expression e Transformation χpeq Regularity condition Term

x x (14) cpq cpq (15) fp tq fpχp tqq (16) t1 t2, P t , , ˆ, u χpt1q χpt2q (17) ÿ

x P T :pp t,sq ϕ t(*) ř x P T p Mulp xq Lcmpχp tq,χpsqq

Lcmpχp tqqmulpχpsqq ˆ χptq if 0 ă Mulp xq ppχp tq, χpsqq χpϕqq (18)

x P T :ϕ t ř x P T p Mulp xq ˆ χptq if 0 ă Mulp xq χpϕqq (19)

ppq ppq (20) pp tq ppχp tqq RCpppχp tqqq(**) (21) t1 t2, P tă, ą, ď, ěu χpt1q χpt2q (22) ϕ1 â ϕ2, â P t , _, ñ, ôu χpϕ1q â χpϕ2q (23) ϕ χpϕq (24) T fi tt1, . . . , tnu ÿ

x PT mulpxq n (25)

@ x P T : pp t, sq ñ ϕ(*) @ x P T : 0 ă Mulp xq ppχp tq, χpsqq ñ χpϕq (26) D x P T : pp t, sq ϕ(*) D x P T : 0 ă Mulp xq ppχp tq, χpsqq χpϕq (27) @ x P T : ϕ @ x P T : 0 ă Mulp xq ñ χpϕq (28) D x P T : ϕ D x P T : 0 ă Mulp xq χpϕq (29)

for each function f : T Ñ T @ x P T : Mulp xq Lcmp xq (30)

@ x P T : Dn P N : Mulp xq n ˆ mulpfp xqq (31)

(*) Rules (18, 26, 27) are applied only when varsp tq Ď t xu and varspsq X t xu H; Rules (19, 28, 29) are applied otherwise. (**) RCpppχp tqqq is defined as @ x P T x : ppχp tqq ñ Mulp xq Lcmp xq _ Mulpχp tqq Lcmpχp tqq, where x varspppχp tqqq.

Table 1: Terms, formulas, and their translation

0.05 sec and the expansion of the lifted model into a concrete one in 0.1 sec. With the same solver and the original sentence, the solution time increases exponentially (4 sec to solve the problem for 30 pigeons). We are aware that symmetry breaking can reduce the complexity, but to the best of our knowledge, solving time is at least linear in the number of pigeons for the best symmetry breaking solvers. We also validated our method on pigeonhole problems where the relation between pigeon and holes is represented by a binary predicate. The translated sentence uses an interpretation table for lcm. Experiments confirm equisatisfiability, but the complexity is quadratic because of the lcm table. Finding a more efficient implementation has been left for future work.

Generative configuration problems Generative configuration problems (GCP) are configuration problems in which the number of some components has to be found: the number of elements in some types is not known in advance. An iterative method is thus always required to find them. When the compressed domain is smaller than the concrete domain, the number of iterations needed to solve the lifted sentence is smaller than the number of iterations for the original sentence, leading to better performance. Hence, GCP is a good application domain for our method.

We evaluate our solving method on three representative GCP discussed in the literature:

the House Configuration and Reconfiguration problem (Friedrich et al. 2011), the Organized Monkey Village (Reger, Suda, and Voronkov 2016) the Rack problem (Feinerer, Salzer, and Sisel 2011; Comploi-Taupe, Francescutto, and Schenner 2022),

These problems are expressed using only an equality predicate and unary symbols, and most regularity constraints introduced by our method are trivially satisfied. The top half of Table ?? shows results with Z3 (with automatic translation of the sentence), the bottom half with the OR-tools solver8 (with manual translation). A more detailed table is provided in the supplementary material (Carbonnelle et al. 2023). Solutions to problems with higher suffixes have more components than similar problems with lower ones. The table shows near constant time performance on the Rack ABCD problems. The lifted methods solve each of the 20 occurrences of the ABCD Racks problem in (Comploi-

8https://google.github.io/or-tools/, used via CPMpy (Guns 2019).

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)

Time # Lifted? Lifted Orig. Lifted Orig. HCP 1 0.2 0.2 6 10 HCP 3 0.22 1.5 6 27 HRP 1 0.27 0.23 7 10 HRP 3 0.30 6.41 8 25 Monkey 1 0.28 184.66 6 20 Monkey 4 0.27 T 6 52 Rack 2011 0.24 8.82 5 23 Rack A5 0.46 0.86 5 19 Rack A10 0.41 37.52 5 38 Rack A1000 0.54 T 4 2250 Rack ABCD4 1.55 4.37 13 20 Rack ABCD8 2.69 T 13 40 Rack ABCD20 3.31 T 13 100 Rack A1 0.61 0.75 5 7 Rack A2 0.64 1.54 5 9 Rack A3 0.62 3.69 5 11 Rack A4 0.65 36.9 5 13 Rack A5 0.65 T 5 19

Table 2: Wall clock time in seconds to solve configuration problems, and number (#) of used domain elements in models. Yes: lifted sentence, No: original sentence, T: timeout after 200 sec.

Taupe, Francescutto, and Schenner 2022) in less than 5 seconds (instead of 6 minutes on average in that paper, using an ASP solver). These results show that our method has significant merits for solving problems with symmetries and a preponderance of unary symbols.

6 Boolean Algebra of Sets with Presburger Arithmetic Lifted domain elements represent disjoint sets of concrete domain elements. A model search in the lifted domain can be seen as a model search involving sets. Hence, our work is highly related to Boolean Algebra of sets with Presburger Arithmetic (BAPA), a logic that can express constraints on the cardinality of sets, of their unions and of their intersections (Kuncak and Rinard 2007; Suter, Steiger, and Kuncak 2011; Bansal et al. 2016). Some problems from verification of properties of software operating on complex data structures contain fragments that belong to BAPA. A sample BAPA statement is |A| ą 1 A Ď B |B X C| ď 2, where A, B, C are sets, and |A| is the cardinality of A. The equivalent expression in FO(Type, Aggregate) is p#td : Apdqu ą 1q p@d : Apdq ñ Bpdqq p#td : Bpdq Cpdqu ď 2q, where A, B, C are now unary predicates over a (unique) type whose interpretation is to be found. This expression can be lifted and solved using our approach (see the theories/BAPA folder in our repository7). In general, any BAPA sentence can be converted to a concrete FO(Type, Aggregate) sentence that only uses unary predicates, and that can be lifted without regularity constraints. Hence, our approach offers a simple way to solve BAPA problems using any solver capable of reasoning over the rationals. The performance advantage should be evaluated in future work.

On the other hand, the conversion of a concrete FO(Type, Aggregate) sentence to BAPA logic is challenging because FO(Type, Aggregate) is more expressive: it allows n-ary relations, functions, sum aggregates, and product of cardinalities. Thus, a BAPA solver could not be used to solve, e.g., generative configuration problems. Still, extensions of BAPA solvers to handle finite n-ary relations have been implemented in CVC4 (Meng et al. 2017). A simple approach to represent structures in BAPA is to use disjoint subsets of the concrete domain, called Venn regions, so that the cardinalities of any set of interest is the sum of the cardinalities of its Venn regions. Unfortunately, the number of Venn regions grows exponentially with the number of sets of interest. Hence, various methods have been developed to reduce this growth, e.g., by creating new Venn regions lazily when required (Bansal et al. 2016). Venn regions are similar to our lifted domain elements, and the iterative method that creates new Venn region is similar, to some extent, to our iterative method that creates new lifted elements when required. Our method cannot prove the unsatisfiability of a sentence. By contrast, efficient methods have been proposed to prove the unsatisfiability of BAPA sentences (Suter, Steiger, and Kuncak 2011).

7 Discussion

Unlike the traditional approach of adding symmetry breaking conditions to a formula to accelerate satisfiability checking, we automatically translate the formula to a form with fewer symmetries. Our results demonstrate the benefits of this approach for problems with symmetries and a preponderance of unary symbols, and justify further research in automatic translation for symmetry reduction. Much work remains to be done in evaluating the method and determining problem areas where it is useful. Moreover, the relationship with BAPA logic is worth further exploration because, unlike our method, BAPA can identify unsatisfiable sentences and our method does not terminate for such problems. Efficient implementation of the lcm function is another area of research. Worth exploring is also the relevance for related areas such as model counting. Ideally, any compression of a model of a sentence (Section 3) should be a model of the lifted sentence. It is unlikely that this is achievable, as it requires a translation that avoids all regularity constraints apart from those for functions. This requires being able to predict the fraction of concrete variable assignments (in the expansion of a lifted assignment) that make a concrete formula true, given that the translated formula is true with the lifted assignment. In particular, filter formulas (in an aggregate) having both free and quantified variables are problematic. Still, many refinements of the translation in Table ?? are feasible. We have already worked out some refinements, but they cannot be presented within the current space constraints. They will be presented in the Ph D thesis of one of the authors (Carbonnelle 2024).

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)

Acknowledgments This research received funding from the Flemish Government under the Onderzoeksprogramma Artifici ele Intelligentie (AI) Vlaanderen programme.

References Bansal, K.; Reynolds, A.; Barrett, C.; and Tinelli, C. 2016. A new decision procedure for finite sets and cardinality constraints in SMT. In International Joint Conference on Automated Reasoning, 82 98. Springer. Carbonnelle, P. 2024. Standard, Interactive and Lifted Model Expansion using FO( ). Ph.D. thesis, KU Leuven, Belgium. Carbonnelle, P.; Schenner, G.; Bruynooghe, M.; Bogaerts, B.; and Denecker, M. 2023. Using Symmetries to Lift Satisfiability Checking. ar Xiv:2311.03424. Carbonnelle, P.; Vandevelde, S.; Vennekens, J.; and Denecker, M. 2022. IDP-Z3: a reasoning engine for FO(.). Co RR, abs/2202.00343. Comploi-Taupe, R.; Francescutto, G.; and Schenner, G. 2022. Applying incremental answer set solving to product configuration. In et al., A. F., ed., SPLC 22: 26th ACM Int l Systems and Software Product Line Conference, 150 155. ACM. Crawford, J. M.; Ginsberg, M. L.; Luks, E. M.; and Roy, A. 1996. Symmetry-Breaking Predicates for Search Problems. In Aiello, L. C.; Doyle, J.; and Shapiro, S. C., eds., Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR 96), Cambridge, Massachusetts, USA, November 5-8, 1996, 148 159. Morgan Kaufmann. de Moura, L.; and Bjørner, N. 2008. Z3: An Efficient SMT Solver. In et al., C. R. R., ed., Tools and Algorithms for the Construction and Analysis of Systems, 14th Int l Conference, volume 4963 of Lecture Notes in Computer Science, 337 340. Springer. Devriendt, J.; Bogaerts, B.; Bruynooghe, M.; and Denecker, M. 2016. On local domain symmetry for model expansion. Theory Pract. Log. Program., 16(5-6): 636 652. Enderton, H. B. 1972. A mathematical introduction to logic. Academic Press. ISBN 978-0-12-238450-9. Feinerer, I.; Salzer, G.; and Sisel, T. 2011. Reducing Multiplicities in Class Diagrams. In et al., J. W., ed., MODELS 2011., volume 6981 of Lecture Notes in Computer Science, 379 393. Springer. Felfernig, A.; Hotz, L.; Bagley, C.; and Tiihonen, J. 2014. Knowledge-based configuration: From research to business cases. Newnes. Friedrich, G.; Ryabokon, A.; Falkner, A. A.; Haselb ock, A.; Schenner, G.; and Schreiner, H. 2011. (Re)configuration using Answer Set Programming. In et al., K. M. S., ed., Proceedings of the IJCAI 2011 Workshop on Configuration, volume 755 of CEUR Workshop Proceedings. CEUR-WS.org. Gent, I. P.; Petrie, K. E.; and Puget, J.-F. 2006. Symmetry in constraint programming. Foundations of Artificial Intelligence, 2: 329 376.

Guns, T. 2019. Increasing modeling language convenience with a universal n-dimensional array, CPpy as pythonembedded example. In Proceedings of the 18th workshop on Constraint Modelling and Reformulation at CP (Modref 2019), volume 19. Kuncak, V.; and Rinard, M. C. 2007. Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic. In Pfenning, F., ed., CADE-21, 2007, volume 4603 of Lecture Notes in Computer Science, 215 230. Springer. Lynce, I.; and Marques-Silva, J. 2004. On Computing Minimum Unsatisfiable Cores. In SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004, Vancouver, BC, Canada, Online Proceedings. Meng, B.; Reynolds, A.; Tinelli, C.; and Barrett, C. W. 2017. Relational Constraint Solving in SMT. In de Moura, L., ed., CADE 26, 2017, volume 10395 of Lecture Notes in Computer Science, 148 165. Springer. Reger, G.; Suda, M.; and Voronkov, A. 2016. Finding Finite Models in Multi-sorted First-Order Logic. In et al., N. C., ed., Theory and Applications of Satisfiability Testing - SAT 2016, volume 9710 of Lecture Notes in Computer Science, 323 341. Springer. Schenner, G.; and Taupe, R. 2017. Techniques for solving large-scale product configuration problems with ASP. In Proceedings of the 19th International Configuration Workshop, 12 19. Suter, P.; Steiger, R.; and Kuncak, V. 2011. Sets with Cardinality Constraints in Satisfiability Modulo Theories. In et al., R. J., ed., VMCAI 2011, volume 6538 of Lecture Notes in Computer Science, 403 418. Springer.

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)