I.

People utter sentences at contexts, which we represent as pairs <w, t>.

Our reply

On the contextualist analysis, (9) expresses proposition (10) at Context B:

(10) that it is no longer the case that Lance Armstrong won the Tour de France in 2000 according to declaration β.

Our reply

On the contextualist analysis, (9) expresses proposition (10) at Context B:

(10) that it is no longer the case that Lance Armstrong won the Tour de France in 2000 according to declaration β.

 However, (10) has a presupposition that is false in the circumstance of Context B, namely: that it was once the case that Armstrong won the Tour de France in 2000 according to declaration β.

Conclusion Conclusion

 The attempts to block our conclusion do not work. So, maybe, the past can really change.

Conclusion

 The attempts to block our conclusion do not work. So, maybe, the past can really change.

 One should stop asking whether the past can change and start to think how this could be.

Conclusion

 The attempts to block our conclusion do not work. So, maybe, the past can really change.

 One should stop asking whether the past can change and start to think how this could be.

 How to make sense of this idea? Suggestions are welcome!

  Armstrong won the Tour de France seven times from 1999 to 2005. He was later stripped of those titles for doping. So, Armstrong never won any Tour de France in the end.

	More precisely More precisely More precisely Our reply Our reply
	 A temporally specific sentence S that is about the  A temporally specific sentence S that is about the  If (3) implied (1), adding to (3) the sentence  Having come to know that Armstrong's titles  Having come to know that Armstrong's titles
	past in a context c is true in c if and only if the time the proposition p expressed by S in c is about has, relative to the past of c, the property that p past in a context c is true in c if and only if the time the proposition p expressed by S in c is about 'Armstrong never won any Tour de France in the end' have been revoked by declaration β, you assert have been revoked by declaration β, you assert should result in a contradiction, given that the latter sentence and (1) are incompatible. (9) at Context B: (9) at Context B:
	ascribes to it. (9) It is no longer the case that Lance (9) It is no longer the case that Lance
	(7) that Lance Armstrong won the Tour de Armstrong won the Tour de France in 2000. Armstrong won the Tour de France in 2000.
	France in 2000 according to the declaration
	of Context A (Declaration α)
	(8) that Lance Armstrong won the Tour de
	France in 2000 according to the declaration
	of Context B (Declaration β)

II. Sentences express propositions at contexts. III. A sentence S is temporally specific if and only if, for any context c, the proposition expressed by S at c is about a specific time.

IV. A sentence S is about the past in a context c if and only if the proposition expressed by S at c is about a time that precedes c. has, relative to the past of c, the property that p ascribes to it.

 'Obama was born in 1961' is true in <@, 1 st Sept 2014> if and only if, relative to the past of <@, 1 st Sept 2014>, the year 1961 has the property of being a time in which Obama was born.

 However, (

6

) is perfectly consistent! (6)

 (9) is true in Context B.

 If (3) implied (1), adding to (3) the sentence 'Armstrong never won any Tour de France in the end' should result in a contradiction, given that the latter sentence and (1) are incompatible.

 The verb phrase 'win the Tour de France in 2000' is context-sensitive.

 (1) expresses different propositions at Context A and Context B:

 (1) expresses different propositions at Context A and Context B: (7) that Lance Armstrong won the Tour de France in 2000 according to the declaration of Context A (Declaration α)


Thomas Vigouroux

Cristian Ene

David Monniaux

Laurent Mounier

Marie-Laure Potet

Formal Methods in Computer-Aided Design 2022 BAXMC: a CEGAR approach to Max#SAT

Max#SAT is an important problem with multiple applications in security and program synthesis that is proven hard to solve. It is defined as: given a parameterized quantifierfree propositional formula, compute parameters such that the number of models of the formula is maximal. As an extension, the formula can include an existential prefix.

We propose a CEGAR-based algorithm and refinements thereof, based on either exact or approximate model counting, and prove its correctness in both cases. Our experiments show that this algorithm has much better effective complexity than the state of the art.

I. INTRODUCTION

#SAT is the problem of counting the solutions of a quantifier-free propositional formula, the counting version of the SAT problem. Max#SAT is the problem of optimizing, according to some propositional variables, the number of solutions according to the others. We generalize this problem to allow an existential prefix in the formula.

This problem has many practical applications in diverse areas of computer science such as quantitative program analysis and program synthesis [START_REF] Fremont | Maximum model counting[END_REF]. Most approaches for quantitative information flow analysis use approximations, with fast yet imprecise solutions. Adaptive attacker synthesis [START_REF] Saha | Incremental attack synthesis[END_REF] would also benefit from advances in Max#SAT efficiency, mainly by being able to avoid the use of imprecise heuristics.

Unfortunately, Max#SAT has high complexity [START_REF] Monniaux | NP #p = ∃PP and other remarks about maximized counting[END_REF], [START_REF] Torán | Complexity classes defined by counting quantifiers[END_REF], and practical solving methods remain costly. At the time of writing, only one solver is publicly available off-the-shelf [START_REF] Fremont | Maximum model counting[END_REF].

Earlier work on the Max#SAT problem proposed two approaches. The first is a probabilistic solving method [START_REF] Fremont | Maximum model counting[END_REF], which unfortunately degrades to exhaustive search when seeking precise answers to the problem. The second approach [START_REF] Audemard | Identifying soft cores in propositional formulae[END_REF] solves the problem exactly, but scales poorly.

We present in this paper a new approach to Max#SAT, leveraging ideas from CEGAR solvers, and show its effectiveness on various benchmarks used in previous publications on the subject. We also present improvements of our algorithm based on previous work about symmetry breaking in SAT solvers [START_REF] Metin | Cdclsym: Introducing effective symmetry breaking in sat solving[END_REF].

Our contributions are the following:

• An effective algorithm to compute maximal solutions for the projected model counting problem (Sections III and IV). This algorithm relies either on an exact projected model counter as a subprocedure, or on an approximated one, which should be the case most times in practice for

This work was partially supported by the French ANR project TAVA (ANR-20-CE25-0009) and by the LabEx PERSYVAL-Lab (ANR-11-LABX-0025-01) funded by the French program Investissements d'avenir. scalability reasons. A complete correctness proof of this algorithm is given for both cases.

• The extension of our algorithm with SAT symmetry breaking techniques (Section V) and heuristics (Section VI), to further improve its efficiency. • The implementation of this algorithm in the tool BAXMC [START_REF]Baxmc website[END_REF], together with a set of experimental results (Section VII), showing the accuracy and performances of our Max#SAT algorithm on various benchmarks, with respect to the only other available tool.

II. PRELIMINARIES

We set our problem in standard Boolean logic. Throughout the paper, Greek letters (φ, ψ, . . . ) denote Boolean formulas, uppercase calligraphic Latin letters (V, X , Y, Z, . . . ) denote sets of variables, simple uppercase Latin letters (V , X, Y , Z, . . . ) denote variables, lowercase variants of these letters (x, y, z, . . . ) denote valuations for these sets of variables.

Let B = {true, false}. A literal is a variable or its negation and the set of literals derived from a set of variables V is denoted by V = V ∪ ¬V. Let φ(V) be a Boolean formula over V a set of variables. A valuation v : V → B is a model of φ if φ evaluates to true over v; this is denoted by v |= φ.

We say that a formula φ is satisfiable if there exists v such that v |= φ. Otherwise, φ is deemed unsatisfiable. Determining whether a formula is satisfiable or unsatisfiable is called the satisfiability problem, also known as SAT.

The restriction of a valuation v : V → B to E ⊆ V is denoted by v| E . We say that two valuations v 1 and v 2 agree on E, denoted by v 1 ∼ E v 2 , if their restrictions to E are equal.

A. Base definitions

Definition II.1 (Equivalence class). Given a valuation v and a set E, we call equivalence class of v over E the set of valuations that agree with v over E, that is:

[v] E = {v ′ | v ′ ∼ E v}
We call v| E partial valuations, and v complete valuations. The elements of [v] E are called the extensions or v| E .

Definition II.2. Given propositional formula φ(V) and E ⊆ V, M E (φ) = {v| E | v |= φ} denotes the set of models projected over E.

Remark II.1. We omit the set E when it contains all the variables of φ. That is M (φ) = M V (φ).

Definition II.3. Given a valuation v, we define the update of the variable V ∈ V to b as:

v[V → b](X) = v(X) if X = V b otherwise
Definition II.4. Given two formulas φ(V) and ψ(V), we say that φ entails ψ (denoted by φ |= ψ) if M (φ) ⊆ M (ψ).

B. Domain-specific definitions

In the remaining of the paper we consider a partition of V over three sets X , Y and Z, respectively called witness, counting and intermediate variables. Given a Boolean formula φ(X , Y, Z), we define Max#SAT as an optimization problem stated as follows: find x m ∈ M X (φ) such that the projected model counting over Y of the formula (which will be defined later) is maximal.

Definition II.5 (Induced set). Given a formula φ(X , Y, Z) and x ∈ M X (φ), the set of models over Y induced by x is:

I φ (x) = {y ∈ M Y (φ) | ∃z . (x, y, z) |= φ}
We extend this definition to partial witnesses as follows:

I φ (x| E ) = x ′ ∈[x] E I φ (x ′ ).
Definition II.6 (Model counting). Given a formula φ(X , Y, Z), the count of a witness x is defined by the size of the set it induces

|φ (x, Y, Z)| = |I φ (x)|.
We extend this definition to partial witnesses as follows

|φ (x| E , Y, Z)| = |I φ (x| E )|.
Definition II.7 (Max#SAT). Given formula φ(X , Y, Z), we can state the Max#SAT problem more formally as finding x m ∈ M X (φ) such that:

|φ (x m , Y, Z)| = max x∈MX (φ) |φ (x, Y, Z)|
Property II.1. Given a formula φ(X , Y, Z), the count of a partial witness is an upper-bound of the count of its extensions:

∀x ′ ∈ [x] E , |φ (x ′ , Y, Z)| ≤ |φ (x| E , Y, Z)|
Proof. This follows directly from Definition II.5 on induced sets.

Property II.2 (Monotony of model counting). Given a propositional formula φ(X , Y, Z), A ⊆ B ⊆ X , and x ∈ M X (φ), the count of partial witnesses is monotonous:

|φ (x| B , Y, Z)| ≤ |φ (x| A , Y, Z)|
Proof. First, following Definition II.1 we have:

[x] B ⊆ [x] A
Hence, following Definition II.5:

I φ (x| B ) ⊆ I φ (x| A )
And that finishes the proof.

Property II.3. Given a Boolean formula φ(X , Y, Z) such that x ∈ M X (φ), E ⊆ X and X i ∈ X , we have:

|φ (x| E , Y, Z)| ≤ φ x| E-{Xi} , Y, Z ≤ |φ (x| E , Y, Z)| + |φ (x| E [X i → ¬x(X i )], Y, Z)|
Proof. The first inequality is a direct consequence of Property II.2. The last inequality follows from Definition II.5.

Property II.4. For a given φ(X , Y, Z) and φ ′ (X , Y, Z) such that φ |= φ ′ , a witness x, and E ⊆ X we have:

|φ (x| E , Y, Z)| ≤ |φ ′ (x| E , Y, Z)|
Proof. For any y ∈ I φ (x| E ), as y |= φ, and φ |= φ ′ , we get y |= φ ′ and hence

I φ (x| E ) ⊆ I φ ′ (x| E ).
Property II.5. Given φ(X , Y, Z), ψ(X ) and x |= ψ, we have:

|φ(x, Y, Z)| = |(φ ∧ ψ)(x, Y, Z)|
Proof. Since x |= ψ and ψ does not depend on Y and Z, (x, y, z) |= φ if and only if (x, y, z) |= φ ∧ ψ.

III. SOLVING MAX#SAT

This section presents the main algorithm we propose to solve the Max#SAT problem.

A. The main algorithm

Algorithm 1 takes as input a formula φ(X , Y, Z) and computes a pair (x m , n m ) such that x m is a solution to Max#SAT for φ with model counting n m . Together with the formula, the algorithm takes multiple precision parameters:

• (ǫ i ) that are called tolerance parameters [START_REF] Chakraborty | A scalable approximate model counter[END_REF];

• (δ i ) that are called confidence parameters [START_REF] Chakraborty | A scalable approximate model counter[END_REF];

• κ that is called the persistence parameter. Further explanations about these parameters will be given later.

Roughly speaking, this algorithm consists in iterating over possible witnesses x of φ. If the model count for x is less than the current best solution, it blocks generalizations of x such that all extensions of these generalizations are worse than the current best solution (Lines 14 and 16), hence removing a chunk of the search space at each iteration. Otherwise, it saves the candidate, which is then the new maximum, and blocks it (Lines 10 and 16), removing only one candidate from the search space.

We use two kinds of oracles in this algorithm. At Line 7 we call a SAT solver. Calls to an existing #SAT oracle (Lines 5, 8 and 17) can be performed using either an exact or an approximate model counter. In the latter case the precision parameters taken as input of the algorithm are used to configure the oracle, and influence the correctness of the returned value (in the former case, simply assume that they are all 0).

Definition III.1. Given φ(X , Y, Z), x ∈ M X (φ) we say that E ⊆ X is n-bounding if |φ (x| E , Y, Z)| ≤ n.
The GENERALIZE function used in Algorithm 1 at Line 14 is proved to return n m -bounding sets in both the exact (Theorem IV.1) and the approximate case (with probability 1δ, Algorithm 1 Pseudocode for the BAXMCalgorithm 1: function BAXMC ǫ0,ǫ1,δ0,δ1,δ2,κ (φ(X , Y, Z))

2: φ s ← φ 3: x m ← ⊤ 4: n m ← 0 5: N ← MC ǫ0,δ0 (φ (∅, Y, Z)) 6: while n m < N 1+κ do 7: x $ ← -M X (φ s ) ⊲ Pick a new candidate 8: c ← MC ǫ1,δ1 (φ s (x, Y, Z)) 9:
if c > n m then ⊲ New maximum 10:

x m ← x 11:

n m ← c 12: E ← X 13:
else ⊲ Find generalization 14:

E ← GENERALIZE δ2 (x, φ s , n m ) 15:
end if 16:

φ s ← φ s ∧ ¬ (x| E ) ⊲ Block 17: N ← MC ǫ0,δ0 (φ s (∅, Y, Z)) 18:
end while

19:
return x m , n m 20: end function Theorem IV.2). The GENERALIZE function is called Algorithm 2 in this paper and it will be presented in Section IV.

B. Termination and correctness with an exact #SAT oracle

In this subsection, each i-indexed variable of the algorithm denotes its value at the end of the i-th iteration of the main loop. In the exact version of the algorithm, all precision parameters are assumed to be equal to 0 and all calls to MC 0,0 (φ (x, Y, Z)) return |φ (x, Y, Z)|.

Theorem III.1 (Termination with an exact #SAT oracle). Algorithm 1 always terminates.

Proof. By construction of (φ si ) i we have:

∀i > 0, 0 ≤ M X φ s i+1 < |M X (φ s i )|
The sequence (n mi ) i is obviously increasing. From Property II.4, the sequence (N i ) i is decreasing and hence

(N i -n mi ) i is decreasing. Putting all this together, (|M X (φ si )| + (N i -n mi )) i is strictly decreasing.
One can easily see that whenever |M X (φ s i )| = 0 it follows that N i = 0 and N in mi ≤ 0. Hence in all cases, after some iteration k, N kn mk ≤ 0 and the termination follows.

Remark III.1. The worst case complexity of Algorithm 1 is reached when it iterates over all the witnesses of the formula.

Let k be the number of iterations performed when Algorithm 1 terminates, then we have n mk ≥ N k .

Lemma III.1. At every iteration i of Algorithm 1, we have:

M X (φ si ) = M X (φ) - j<i [x i ] Ei
Proof. This follows by construction of φ s i .

Lemma III.2. At every iteration i of Algorithm 1, and assuming GENERALIZE(x, φ, n) returns n-bounding generalizations of x (as defined in Definition III.1) we have:

∀x ′ ∈ j≤i [x j ] Ej , |φ (x ′ , Y, Z)| ≤ n mi Proof. Let j ≤ i, and let x ∈ [x j ] Ej , following Definition III.1, we have φ s j (x, Y, Z) ≤ n mj .
Then by construction of φ si and Property II.5 we have |φ (x, Y, Z)| ≤ n mj which, as (n mi ) i is increasing, proves the lemma.

Theorem III.2 (Correctness with an exact #SAT oracle). Algorithm 1 is correct, i.e., the returned tuple (x m , n m ) satisfies the following relation:

n m = |φ (x m , Y, Z)| = max x∈MX (φ) |φ (x, Y, Z)|
Proof. Following Property II.1 and since n mk ≥ N k we have:

∀x ∈ M X (φ sk ) . |φ (x, Y, Z)| ≤ N k ≤ n mk
Then instantiating Lemma III.2 at iteration k we have:

∀x ∈ i≤k [x i ] Ei , |φ(x, Y, Z)| ≤ n mk Following Lemma III.1, at iteration k we have M X (φ) = M X (φ s k ) ∪ i≤k [x i ] Ei ,
and the result follows.

C. Correctness with a probabilistic #SAT oracle

Since the termination can be proven in the same way as in the exact case, we only prove the correctness.

Let us first recall the expected guarantees provided by an approximate model counter [START_REF] Chakraborty | A scalable approximate model counter[END_REF], where the ǫ parameter characterizes the precision of the result and the δ parameter determines its associated confidence.

Property III.1 (Correctness of the Model Counting). The count MC ǫ,δ (φ (x, Y, Z)) returned by an approximate model counter satisfies the following:

P 1 1 + ǫ ≤ MC ǫ,δ (φ (x, Y, Z)) |φ(x, Y, Z)| ≤ 1 + ǫ ≥ 1 -δ
These guarantees extend to partial witnesses naturally, i.e., queries of the form MC ǫ,δ (φ (x| E , Y, Z)).

The next theorem proves the correctness of Algorithm 1 in the approximate case and gives the associated tight bounds.

Theorem III.3. Let (x m , n m ) be the result returned by the call BAXMC ǫ0,ǫ1,δ0,δ1,δ2,κ (φ(X , Y, Z)), and let

M = max x∈MX (φ) |φ (x, Y, Z)| If δ 1 ≤ δ2
|X |+1 then:

P 1 1 + ǫ 1 ≤ n m |φ (x m , Y, Z)| ≤ 1 + ǫ 1 ≥ 1 -δ 1 and P |φ (x m , Y, Z)| ≥ M (1 + ǫ 0 ) * (1 + ǫ 1 ) * (1 + κ) ≥ (1 -δ 1 ) * min(1 -δ 2 , 1 -δ 0 )
Proof. Let φ S be the final value of the variable φ s after the last iteration of the while loop. We have the following guarantees from the approximate model counter (Property III.1):

P 1 1 + ǫ 1 ≤ n m |φ (x m , Y, Z)| ≤ 1 + ǫ 1 ≥ 1 -δ 1 (1)
P 1 1 + ǫ 0 ≤ N |M Y (φ S )| ≤ 1 + ǫ 0 ≥ 1 -δ 0 (2)
From Theorem IV.2 regarding the GENERALIZE function (which will be proved in the next section), we also have that for any x ∈ M X (φ ∧ ¬φ S ) it holds (assuming that

δ 1 ≤ δ2 |X |+1 ): P [|φ (x, Y, Z)| ≤ n m ] ≥ 1 -δ 2 . (3)
After the last iteration of the while loop we have that n m * (1 + κ) ≥ N . Using this and Equation ( 2) and Property II.5 we get that for any x ∈ M X (φ S ) it holds

P [|φ (x, Y, Z)| ≤ n m * (1 + κ) * (1 + ǫ 0 )] ≥ P [|φ (x, Y, Z)| ≤ N * (1 + ǫ 0 )] = P [|φ S (x, Y, Z)| ≤ N * (1 + ǫ 0 )] ≥ P [|M Y (φ S )| ≤ N * (1 + ǫ 0 )] ≥ 1 -δ 0 .
From Equation (3), for any x ∈ M X (φ ∧ ¬φ S ) it holds

P [|φ (x, Y, Z)| ≤ n m * (1 + κ) * (1 + ǫ 0 )] ≥ P [|φ (x, Y, Z)| ≤ n m ] ≥ 1 -δ 2 .
Hence, for any x ∈ M X (φ) it holds

P [|φ (x, Y, Z)| ≤ n m * (1 + κ) * (1 + ǫ 0 )] ≥ min(1 -δ 2 , 1 -δ 0 )
and hence

P n m 1 + ǫ 1 ≥ M (1 + κ) * (1 + ǫ 0 ) * (1 + ǫ 1 ) ≥ min(1 -δ 2 , 1 -δ 0 ). ( 4
)
Combining this with the Equation (1), we obtain

P |φ (x m , Y, Z)| ≥ M (1 + κ) * (1 + ǫ 0 ) * (1 + ǫ 1 ) ≥ (1 -δ 1 ) * min(1 -δ 2 , 1 -δ 0 ).
The following corollary instantiates Theorem III.3 in order to get the standard form (as in Property III.1).

Corollary III.1. For any 0 < ǫ, δ < 1, if in the call of the BAXMC function, we take as parameters

ǫ 0 = ǫ 1 = κ = 3 √ 1 + ǫ -1, δ 0 = δ 2 = δ 2 and δ 1 = δ 2 * (|X |+1)
, then the result (x m , n m ) satisfies the following inequalities:

P 1 1 + ǫ ≤ n m |φ (x m , Y, Z)| ≤ 1 + ǫ ≥ 1 -δ P |φ (x m , Y, Z)| ≥ M 1 + ǫ ≥ 1 -δ where M = max x∈MX (φ) |φ (x, Y, Z)| Proof. It is easy to check that ǫ 1 = 3 √ 1 + ǫ -1 ≤ ǫ, δ 1 = δ 2 * (|X |+1) < δ 2 = δ 2 < δ, (1 + ǫ 0 ) 3 = 1 + ǫ and (1 -δ 1 ) * (1 -δ 0 ) = 1 -δ 0 -δ 1 + δ 0 * δ 1 > 1 -2 * δ 0 = 1 -δ.
IV. GENERALIZATION ALGORITHM Algorithm 2 generalizes a single model x with insufficiently high count to a set of models with insufficiently high count. This is much the same that a CDCL loop blocks not only one assignment, but a whole set of assignments.

As shown in Property II.2, generalizing a witness is an instance of the MSMP problem (Minimal Set subject to a Monotone Predicate), which can be solved using generic algorithms such as QUICKXPLAIN [START_REF] Junker | QuickXplain: Conflict detection for arbitrary constraint propagation algorithms[END_REF]. Although in theory this should lead to a better algorithm, in practice we observed larger numbers of calls to the #SAT oracle, an issue already identified in other contexts [START_REF] Monniaux | Quantifier elimination by lazy model enumeration[END_REF].

Algorithm 2 is thus a specific solver of the MSMP problem in our setting, relying on a linear sweep over the variables that are part of the valuation.

For efficiency reasons, the steps mentioned in Algorithm 2 are in a precise order. The reason behind this is:

1) The first step relies on a consequence of Property II.3, allowing to relax variables with simple calls to a sat solver.

2) The log-based generalization is a heuristic allowing to do big steps in the generalization process by relaxing multiple variables at each loop turn.

3) The linear sweep pass generalizes x in such a way that the returned set is minimal, i.e. that none of the further generalizations of the returned value satisfies Definition III.1. The returned E is guaranteed only to be a local minimum and it may not be the smallest set such that Definition III.1 holds because of the order in which we consider variables of X in Algorithm 2.

A. Correctness and complexity with an exact #SAT oracle

Property IV.1. If φ(x| E [X i → ¬x(X i )], Y, Z) is UNSAT then: |φ (x| E , Y, Z)| = φ x| E-{Xi} , Y, Z
Proof. This follows directly from Property II.3.

Let us prove the correctness of Algorithm 2 in the context of an exact #SAT oracle. This will finish the correctness proof started in Section III-B.

Algorithm 2 Pseudocode for the generalization algorithm

1: function GENERALIZE δ (x, φ(X , Y, Z), n m ) 2: E ← X 3: for all X i ∈ X do ⊲ Redundancy elimination 4: if φ (x[X i → ¬x(X i )], Y, Z) UNSAT then 5: E ← E -{X i } 6: end if 7:
end for

8: k ← log n m -log MC ǫ,δ1 (φ (x| E , Y, Z)) 9:
while k > 0 ∧ |E| > 0 do ⊲ Log-elimination 10:

A k $ ← -{V ⊆ E | |V| = k} 11: c ← MC ǫ,δ1 (φ (x| E-A k , Y, Z)) 12:
if c ≤ nm 1+ǫ then

13:

E ← E -A k 14:
k ← log n mlog c 15:

else 16: k ← k -1 17:
end if Proof. In the while loop at Line 9 we can see that, at each iteration, either |E| or k decreases, thus ensuring the termination of the algorithm.

During any update of the temporary value E (Lines 5, 13 and 21), we ensure that the new value of E satisfies Definition III.1: 1) At Line 5, Property IV.1 keeps the model counting stable. 2) At Lines 13 and 21, the update is guarded by the explicit check of the property (in the if statement Lines 12 and 20).

Hence the correctness follows.

B. Bounds with an approximate #SAT oracle

Theorem IV.2. Let E ⊆ X be the set returned by the call GENERALIZE δ (x, φ(X , Y, Z), n), and assume that We denote by C x|V the value returned by the call MC ǫ,δ1 (φ (x| V , Y, Z)). Since each time we update E to a set V we ensure C x|V ≤ n 1+ǫ , we have the following probability:

P [|φ (x, Y, Z)| ≤ n] ≥ 1 - δ |X | + 1 Then: P [|φ (x| E , Y, Z)| ≤ n] ≥ 1 -δ Proof.
P [|φ (x| E , Y, Z)| ≤ n] ≥ 1 -δ 1
Let E l denote the value obtained after l updates of variable E during LOG-ELIMINATION and REFINEMENT steps within Algorithm 2 and let us denote by P l the probability that the set E l is approximately n-bounding.

Using that we update E to the value E l only if C x|E l * (1 + ǫ) ≤ n, we have the following recursive relation:

P l = P [|φ (x| E l , Y, Z)| ≤ n] * P l-1 ≥ (1 -δ 1 ) * P l-1 ≥ (1 -δ 1 ) l * P 0 ≥ (1 -δ 1 ) l * 1 - δ |X | + 1 Thus, as l ≤ |X |, if we take δ 1 = δ |X |+1
and we call the #SAT oracle with parameters (ǫ, δ |X |+1 ) we get:

P [|φ (x| E , Y, Z)| ≤ n] ≥ (1 -δ 1 ) l+1 ≥ 1-(l+1) * δ 1 ≥ 1-δ
Remark IV.1. The bound with respect to the number of updates is tight. The worst case is reached when the only valid subset of X is X itself, that is when the model cannot be generalized.

V. BREAKING SYMMETRIES IN MAX#SAT

Symmetries are a special kind of permutations of the input variables of a formula leaving it intact. Exploiting or breaking symmetries in SAT formulas has long been a topic of interest.

For instance, if a formula is left intact by such a permutation then for each blocking clause C, the solver may need to generate the full orbit of C by the group of permutations, leading to combinatorial explosion. Breaking the symmetry means selecting one solution per orbit by adding a predicate called symmetry breaking predicate to the formula, purposefully generated to break the symmetries. The resulting formula is equisatisfiable, but often simpler to solve.

A. Correctness in the presence of symmetries

In our context, handling symmetries within the witness set reduces the size of the search space, and leads to better complexity. We give in this section arguments about why this is true. Definition V.1. Given a Boolean formula φ(X , Y, Z), a symmetry of φ is a bijective function σ : X → X that preserves negation, that is σ(¬X) = ¬σ(X), and such that, when σ is lifted to formulas, σ(φ) = φ syntactically [START_REF] Zhang | Combinatorial designs by sat solvers 1[END_REF].

S φ denotes the set of all symmetries of φ. We lift S φ to models by defining the set of symmetries of a model x,

S φ (x) = {x • σ | σ ∈ S φ }.
Theorem V.1. In Algorithm 1, picking only one x per symmetry class of φ preserves the correctness of the algorithm both in the exact and approximate case.

Proof. Whatever the method used to select only one member of each symmetry class, this corresponds to creating a symmetry breaking predicate ψ(X ) and solving the problem over φ ∧ ψ, and thus the Property II.5 applies.

B. Implementing Max#SAT symmetry breaking

We detect symmetries in φ using the automorphisms of a colored graph representing the formula, defined as follows:

• For each variable, create two nodes: one for the positive literal, and one for the negative literal. Use color 0 if the variable is in X, otherwise use color 1. Add an edge (Boolean consistency edge) between the two nodes. • For each clause, create a node, and assign to it the color 2.

Add an edge between this clause node and every node corresponding to a literal present in the clause. Many tools can be used in order to list the automorphisms of a graph. In our case, we used BLISS [START_REF] Junttila | Engineering an efficient canonical labeling tool for large and sparse graphs[END_REF] because of its C++ interface, and its performance.

After detecting the symmetries, one can use any symmetry breaking technique available, either static [START_REF] Devriendt | Improved static symmetry breaking for sat[END_REF] or dynamic [START_REF] Metin | Cdclsym: Introducing effective symmetry breaking in sat solving[END_REF]. In our implementation, we chose to use CDCLSYM [START_REF] Metin | Cdclsym: Introducing effective symmetry breaking in sat solving[END_REF] because of its ease of use, and because it avoids generating complex symmetry breaking predicates ahead of time.

VI. HEURISTICS AND OPTIMIZATIONS

We present in this section heuristics used in both Algorithms 1 and 2 in practice, and discuss their effectiveness.

A. Progressive construction of the candidate

A simple yet effective optimization is to gradually add literals to the candidate x in Algorithm 1 at Line 7. By stopping earlier, this allows to call GENERALIZE on a partial assignment instead of a complete one, and will decrease the number of calls to the #SAT oracle as it anticipates work that is done in Algorithm 2.

B. Leads

When performing the generalization in Algorithm 2, one can see that we can extract hints about promising parts of the search space when relaxing variables. Indeed, when relaxing parts of the solution (Lines 16 and 22), if the model count of the relaxation goes above n m , then this part of the search space may contain an improvement over the current solution.

Following this intuition, one can hold a sorted list1 of relaxations whose count is above the current best known maximum, and use it to favor parts of the search space that look promising. We call these promising relaxations leads. More formally, given x| E a lead, when searching for a new solution in Algorithm 1 at Line 7, instead of searching in

M X (φ s ), one would search in M X (φ s ) ∩ [x] E .
Let L n (φ) denote the set of leads currently known to the solver with count lower than n. When the currently known maximum is improved in Algorithm 1 at Line 10, we can block all leads whose count is below the new maximum:

φ si+1 = φ si ∧ [x] E ∈Ln m (φ) ¬ (x| E )

C. Decision heuristic

As discussed in Section IV-A, the performances of the algorithm depend on the order with which variables are considered in various parts of the solving process (in the generalization and during the optimization presented in Section VI-A). One can see that this kind of problem, that we call variable scheduling, is actually predominant when solving SAT problems, and even #SAT problems.

One first heuristic arises from the leads described in Section VI-B. One can use the leads list as indications for literals leading to promising parts of the search space, by finding the literal which appears the most in the leads. We call this heuristic leads.

Another decision heuristic can be devised using VSIDS [START_REF] Moskewicz | Chaff: Engineering an efficient sat solver[END_REF]. The idea is to assign a weight to each literal based on its last appearance in a blocking clause. The weight of each literal is increased by a constant amount every time the literal appears in a blocking clause, and is multiplicatively decreased at each blocking clause. This heuristic showed promising results in both SAT and #SAT [START_REF] Sang | Heuristics for fast exact model counting[END_REF]. We call this heuristic vsids.

One could also choose the next decision variable at random, which we call rnd. And finally, one could just pick the decision variables in the order they are provided to the tool, which we call none.

An experimental evaluation is done in Section VII-B.

D. Handling equivalent literals

Equivalent literals are a notorious property of Boolean formulas which, when exploited, results generally in better runtime performances [START_REF] Lai | The power of literal equivalence in model counting[END_REF].

Definition VI.1. Given a Boolean formula φ, we say that two literals

L i ∈ V and L j ∈ V are equivalent if φ |= L i ⇔ L j .
Equivalent literals allow to simplify formulas based on the following theorem.

Theorem VI.1. Let φ be a Boolean formula and two equivalent literals L i and L j . Then solving the Max#SAT problem for φ is reduced to solving the Max#SAT problem for the simpler formula φ ′ obtained by replacing all occurrences of L j (resp. ¬L j ) by L i (resp. ¬L i ) when:

1) either L i and L j are in the same literal class (either X ,

Y or Z) 2) or L i ∈ X and L j ∈ Y ∪ Z 3) or L i ∈ Y and L j ∈ Z.
Theorem VI.1 can be applied multiple times in order to further simplify the formula. Literal equivalence can be detected using binary implication graphs [START_REF] Heule | Efficient cnf simplification based on binary implication graphs[END_REF].

VII. EXPERIMENTAL EVALUATION

Algorithm 1 has been implemented in an open-source tool written in C++ called BAXMC [START_REF]Baxmc website[END_REF], including dynamic symmetry breaking techniques (Section V) and all the heuristics discussed in Section VI. In this implementation, we only incorporated the approximate version of the algorithm using APPROXMC5 [START_REF] Meel | Sparse hashing for scalable approximate model counting: theory and practice[END_REF] as an approximated model counting oracle and CRYPTOMINISAT [START_REF] Soos | Extending SAT solvers to cryptographic problems[END_REF] as a SAT solver oracle. An exact solver is not implemented because we do not, at the time of writing, have another exact Max#SAT solver available as a comparison.

We use three sets of benchmarks, coming either from [START_REF]Maxcount 1.0.0[END_REF], or from MaxSat 2021 competition [START_REF]Maxsat evaluation[END_REF]. Benchmarks from this later class are transformed using the method from [START_REF] Fremont | Maximum model counting[END_REF]. Table I shows more details about the benchmark set considered. Benchmarks annoted with a star indicate that a symmetry was found.

All experiments are run on a Dell R640 with 40 cores and 192 GB of RAM running Debian 11, with a 2-hour timeout, a 10 GB memory limit and with parameters δ = 0.2, ǫ = 0.8.

A. Comparison to MAXCOUNT

MAXCOUNT [START_REF] Fremont | Maximum model counting[END_REF] is used as an off-the-shelf solver of the problem, with parameters corresponding to δ = 0.2, ǫ = 0.8. Note that these are not the parameters used in the experiments in [START_REF] Fremont | Maximum model counting[END_REF] and that we reimplemented MAXCOUNT using newer oracles. We did this in order to see how MAXCOUNT and BAXMC behave when both are providing the same correctness guarantees and using the same oracles for fairness. All figures from Table II are obtained when BAXMC is used with the (leads,rnd) heuristic combination.

Table II shows the results obtained when running both tools on our three benchmarks. Bolded values are the best values on this line (i.e., smaller time or biggest answer). The time columns are the running times of the tools. The model count columns are the values returned by the candidate tools.

One can see that BAXMC outperforms MAXCOUNT in all benchmark timings. In cases where BAXMC did not find the best value, it terminates when the bounds on the possible maximum are tight enough. This yields a small error margin on the returned value of BAXMC, but is configurable through its κ argument.

B. Decision heuristic comparison

Table III shows a comparison between the heuristics that are currently available in BAXMC. Lines enumerate the decision heuristics from Section VI-C. Columns specify heuristics used by the underlying SAT oracle about literals polarities.

Each cell of this table contains, in sequence: the total running time, the number of time this combination ran the fastest compared to all others, and the number of times this combination timed out. For example combination (leads,cache) ran for a total time of 62968.38 seconds with 7 timeouts, and ran the fastest on 3 benchmarks over a total number of 26. In this setup, any time-out from BAXMC increases the total running time by 7200s.

The table shows that none of the heuristics stands out. We can only eliminate random decision as a bad heuristic. Nevertheless, the combination of heuristics allows to strongly reduce the overall number of timeouts.

VIII. RELATED WORKS

Previous works on Max#SAT solving may be classified into three categories, based respectively on probabilistic solving as in MAXCOUNT [START_REF] Fremont | Maximum model counting[END_REF], exhaustive search [START_REF] Audemard | Identifying soft cores in propositional formulae[END_REF] and knowledge compilation [START_REF] Oztok | Solving pp pp-complete problems using knowledge compilation[END_REF].

Probabilistic solving relies on "amplification" to build a new formula φ(X , Y, Z) = k i=1 φ(X , Y i , Z i ), where the Y i and Z i are fresh copies of the initial Y and Z variables, and uniformly sampling among M X φ . The higher the k, the more the sampling is attracted towards the X with large projected model counting over (Y i ) i≤k . Given parameters ǫ and δ, the guarantees provided about the returned tuple (ñ, x) are the same as in Corollary III.1 [START_REF] Fremont | Maximum model counting[END_REF]. Unfortunately, when the size of the formula increases, uniform sampling may become quite expensive as shown in our benchmarks. Furthermore, this approach is not incremental: looking for a better solution involves re-running the search from scratch.

On the other side of the spectrum lie exhaustive searches. The idea here is to make incremental decisions among the variables in X , propagating the decision in φ, and simplifying the formula in order to cache some results [START_REF] Audemard | Identifying soft cores in propositional formulae[END_REF]. Such approaches are exact, but their exhaustive nature limits their scalability. Component caching [START_REF] Bacchus | Dpll with caching: A new algorithm for #sat and bayesian inference[END_REF] is a practical way to improve scalability [START_REF] Audemard | Identifying soft cores in propositional formulae[END_REF] and it could be beneficial into our algorithm too.

Knowledge compilation consists in compiling the formula into a representation over which solving the problem (here, the optimal model counting) is expected to be much easier. Compilation times tend to dominate and the memory usage of the compiled form may be huge.

A possible approach could use a generalization of X -constrained SDDs [START_REF] Oztok | Solving pp pp-complete problems using knowledge compilation[END_REF]. The idea here would be to build (X , Y)-constrained SDDs, that is SDDs that are Xconstrained, and for which each subtree that are not over X are Y-constrained. In this case, one can easily compute the count of every possible pair x ∈ M X (φ) and then propagate the maximum to the root of the tree. To the best of our knowledge, this direction has not been explored yet.

IX. CONCLUSION AND FUTURE WORK

We proposed a CEGAR based algorithm allowing to solve medium-sized instances of the Max#SAT within reasonable time limits, as illustrated in our experiments. This algorithm allows either to compute exact solutions (when possible), or can be smoothly relaxed to produce approximated results, under well-defined probabilistic guarantees. Comparisons with an existing probabilistic tool showed the gains provided by our algorithm on concrete examples. Our implementation and all the related benchmarks are available on [START_REF]Baxmc website[END_REF].

From an algorithmic point of view this work could be extended in several directions. First, we exploited some classes of symmetries when solving Max#SAT (Section V). This could be improved by detecting new kinds of symmetries [START_REF] Devriendt | Improved static symmetry breaking for sat[END_REF], or exploiting them further using techniques such as symmetry propagation [START_REF] Metin | Composing symmetry propagation and effective symmetry breaking for sat solving[END_REF].

As discussed in Section IV, our relaxation algorithm (Algorithm 2) uses a linear sweep over the literals composing a witness. Instead of returning one possible minimal relaxation, MERGEXPLAIN [START_REF] Shchekotykhin | Mergexplain: Fast computation of multiple conflicts for diagnosis[END_REF] returns multiple ones, which may be helpful in our case by allowing the creation of multiple blocking clauses.

As expected, in some instances, our algorithm may degenerate into exhaustive search. While we do not know yet any characterization of all such instances, we believe that preprocessing and in-processing [START_REF] Järvisalo | Inprocessing rules[END_REF] techniques such as UNHID-ING [START_REF] Heule | Efficient cnf simplification based on binary implication graphs[END_REF] should improve performances and limit the set of inefficient instances.

Finally, Algorithm 1 may be parallelized by correctly scheduling search spaces among threads, possibly using the leads described in Section VI-B. If we enforce the fact that all leads currently present in the lead list are disjoint, that is the [x] E are pairwise disjoint (hence splitting the search space into parts), we expect a favorable parallelization setting.

  Using Property IV.1, the variable E after the first loop within Algorithm 2 satisfies |φ (x, Y, Z)| = |φ (x| E , Y, Z)|.

  Algorithm 2 terminates and is correct: the returned set E satisfies Definition III.1, i.e., |φ (x| E , Y, Z)| ≤ n.

	18:	end while
	19: 20: 21: 22:	⊲ Refinement if MC ǫ,δ1 φ x| E-{Xi} , Y, Z ≤ nm for all X i ∈ X -E do 1+ǫ then E ← E -{X i } end if
	23:	end for
	24: end function
	Theorem IV.1.

The order to use here is: first the count of the relaxation, then the size of the relaxation.