On Consensus Extraction

1 Introduction

A ubiquitous concept in AI concerns forms of consensus among several agents (e.g., [Ephrati and Rosenschein, 1996; Ren et al., 2005]), belief sources (e.g., [Jøsang, 2002; Gauwin et al., 2007]), and more generally several information or knowledge 1 sources, hereafter all simply called sources. Consensuses can take different forms. In this paper, they are investigated in a logic-based context and defined as sets of formulas that do not contradict any of the sources to be reconciled, each of the sources being itself a set of formulas. In this respect, we adopt a liberal approach to the nature of a consensus in the sense that a consensus is not necessary only made of some of the information present in every source but can contain some information not opposed by any source, where opposition is translated by a logical conflict. However, this liberal attitude is limited in this study in the sense that a consensus can only be a subset of all the formulas in the sources.

For example, such a form of consensus can prove helpful in a negotiation context since it allows a group of agents to agree on a common position that is not conflicting with the position of any member of the group. For instance, a coalition of political groups that tries to define and agree on a shared political agenda can find such consensuses useful since they can be advocated and defended by each group. Indeed, each group can explain that the contents of the consensus does not conflict with its own specific positions. Obviously, some consensuses are more appealing than other ones and various families of preference criteria can be used to select consensuses.

1 In this paper, no difference is made between knowledge, belief and information.

Technically, we consider consensus operators in Boolean logic that thus deliver subsets Γ of the set-theoretical union of n information sources [Φ1↪ ▷ ▷ ▷ ↪Φn] such that Γ does not logically conflict with any Φi. We require each source to be a satisfiable set of formulas: an unsatisfiable source would lead to the absence of consensus since no set of formulas is satisfiable together with an unsatisfiable set of formulas. Of natural interest are consensuses that are maximal in some sense. The simplest maximal consensus operators deliver (cardinality or set-inclusion) maximal subsets of formulas that obey the required absence of conflict with each of the sources. Interestingly, they differ from the well-studied family of maximal consistent merging operators (e.g., [Baral et al., 1991; Konieczny, 2000]), which can contradict some of the sources by focusing on (preferred) maximal satisfiable subsets of Sni=1 Φi. Actually, we investigate a family of consensus operators that implement a stepwise prioritization of various forms of preference between the sources to be reconciled and/or their contents.

Noticeably, a generic method to compute one consensus according to these operators is presented and is shown experimentally efficient for many large difficult instances. The approach circumvents the difficulty of having to check the satisfiability of the candidate consensus with each source separately while providing at the same time the guarantee that the consensus satisfies all the maximality and preference requirements.

2 Logical Preliminaries and Conventions

Let L be the standard language of Boolean logic. Boolean variables are noted a↪ b↪ ▷ ▷ ▷ The conjunctive, disjunctive, negation, material implication and equivalence connectives are noted ^↪ _↪ ≻↪!↪⌘, respectively. A literal is a possibly negated variable and a clause is a formula that consists of a disjunction of literals. Formulas and sets of formulas are noted ↵↪ β↪ ▷ ▷ ▷ and Φ↪ Γ↪ ▷ ▷ ▷ , respectively. Profiles are noted S↪ V↪ ▷ ▷ ▷ The cardinality of a set Φ is noted #Φ. Logically equivalent formulas are considered indistinguishable. A set of formulas is satisfiable (also said consistent) iff there exists a truth value assignment of every variable such that all formulas in the set are true according to usual compositional rules. ` denotes the deduction relation and > a tautology. A pre-ordering, noted ⪯, is a binary relation that is both reflexive and transitive: we often use its induced ≺ strict relation. From now on, the profile S = [Φ1↪ ▷ ▷ ▷ ↪Φn] represents n sources Φi where each Φi ⇢ L is satisfiable.

3 Basic Forms of Consensus

Definition 1. A set Γ ⇢ L is a consensus for S iff Γ ✓ Sni=1 Φi and 8 Φi 2 S : Γ [ Φi is satisfiable.

A consensus for S is defined as a subset of Sni=1 Φi that does not logically contradict any Φi. Formally,

Note that by definition any consensus is satisfiable. Of wide-scope interest are consensuses that are maximal either with respect to cardinality or set inclusion.

Definition 2. A consensus Γ for S is max✓ iff 8 ⇥ s.t. Γ ⇢

Clearly, any max# consensus is a max✓ consensus whereas the converse does not hold. Depending on the context, max is used as a shortcut for either max# or max✓, or for any of them. When Sni=1 Φi is satisfiable, this latter set is the unique max consensus for S. For any S, there always exists at least one max consensus, which can be the empty set. Notice also that none of these forms of maximality (and none of the other ones that will be investigated later in the paper) necessarily delivers one unique consensus for S.

⇥ ✓ Sni=1 Φi, 9 Φi 2 S s.t. ⇥ [ Φi is unsatisfiable. A consensus Γ for S is max# iff 8 ⇥ s.t. ⇥ ✓ Sni=1 Φi and #⇥ > #Γ, 9 Φi 2 S s.t. ⇥ [ Φi is unsatisfiable.

Interestingly, max consensuses can differ from maximal satisfiable subsets of Sni=1 Φi noted maxcons, extracted by belief merging operators (see e.g. [Konieczny, 2000]). Indeed, maxcons are not required to be satisfiable with each individual Φi. Accordingly, maxcons are not necessarily max consensuses for S and conversely, although any consensus is included in a maxcons. Assume for example that t↪ w↪ u and p are Boolean variables standing respectively for increase taxation on pollution, increase wages, reduce unemployment and reduce pollution. Let S be the programs of three political groups that negotiate to form a coalition: S = ¶Φ1↪Φ2↪Φ3♦ with Φ1 = ¶t↪ ≻w♦, Φ2 = ¶w ^ (t ! ≻u)♦ and Φ3 = ¶u ^ (≻w ! ≻u)↪ t ! p♦. The unique max✓ consensus for S is Γ = ¶t↪ t ! p♦, namely, increase taxation on pollution and this will reduce pollution. If the group adopts this consensus then it agrees that t and p could hold. Notice that none of the members of the coalition can deduce p based on its own Φ: p is a kind of implicit group information produced by the consensus. Notice that one of the maxcons of S is ⇥ = ¶w ^ (t ! ≻u)↪ u ^ (≻w ! ≻u)↪ t ! p♦: ⇥ does not entail t and ⇥ is not satisfiable together with Φ1.

4 Maximal Number of Agreed Concepts

The knowledge represented in S can be such that each Boolean variable translates one concept. We might prefer a consensus that expresses an agreement on a maximum number of concepts mentioned in S and thus on a maximum number of variables. For example, in a political negotiation, we might prefer a consensus that translates an agreement on decrease taxation, strengthen foreign policy and preserve social security than another consensus with an agreement on only two of these concepts.

Different notions of agreement on a Boolean variable v (say, decrease taxation) in S can be defined. For example, v (or, ≻v) might be required to be inferable from each source; a consensus that translates this agreement should then contain the formula v (resp., ≻v), or, at least, sufficient information to derive it.

In this paper, we adopt a wider-scope form of agreement on a variable v that does not require v (resp., ≻v) to be derivable in every source, or even simply in one of them. We require any consensus that translates an agreement on the variable v to gather what is directly expressed in each source about v, namely all the formulas from S that contain at least one occurrence of the variable v. Notice that, as a consequence, when at least one source contains that (resp., negated) variable as a formula, any consensus that translates an agreement on v must contain the formula v (resp., ≻v). The intuition for this approach to agreement on a variable is best understood in the clausal setting, which will be our practical computational framework. Indeed, a clause that contains a literal v as a disjunct can be rewritten in implicative format, or rule, with v as right-hand side and with the left-hand side stating conditions for v to hold. Accordingly, gathering inside a consensus all clauses that contain v gathers all conditions to derive v that are directly expressed. Obviously, each source might or might not contain its own ways to derive these conditions for v and the different sources might not agree on that.

A consensus Γ that agrees on a maximum number of variables, interpreted as concepts, will thus be a subset of Sni=1 Φi that is satisfiable with each Φi and that contains occurrences of a maximum number of variables that do not occur in S ∩ Sni=1 Φi. Formally, let ⇥ and be two sets of formulas, we note #var(⇥↪ ) the number of different variables occurring in ⇥ that are not occurring at all in .

Definition 3. A consensus Γ for S is max#ac ("ac"meaning agreed concepts) iff for any consensus Γ0 for S s.t. Γ 6= Γ0 , we have that #var (Γ0 ↪ Sni=1 Φi ∩Γ0 )  #var (Γ↪ Sni=1 Φi ∩Γ).

Notice that there may exist consensuses for S that contain occurrences of more variables than max#ac consensuses for S do.

5 More Maximality Preference Criteria

We now examine other maximality-based preference paradigms that can lead to the selection of different or even smaller subsets of consensuses for S. We will allow for their stepwise combinations: this will yield possible additional progressive pruning of the set of of preferred consensuses into a set of better preferred consensuses.

First, let us give an example of stepwise combination of criteria: the max#ac concept can be selected and adapted to follow or precede the max✓ (or the max#) paradigm. We can for instance first select the max#ac consensuses for S and adapt max# in such a way that it only refines this latter set of consensuses. Clearly this translates a sequencing and prioritization of preferences: 1. a preference for consensuses that agree on a maximal number of concepts, and then 2. a preference for the consensuses (among these latter ones) that contain a maximum number of formulas from the sources. For short, this ordered combination of operations is noted max#(max#ac(S)).

Definition 4. A consensus Γ for S totally satisfies a source Φi iff Φi ✓ Γ. Γ is max#100%Φi iff @Γ0 s.t. Γ0 is a consensus for S that totally satisfies a strictly greater number of sources of S than Γ does.

Let us now examine other possible forms of preferences among sources. For example, one might prefer a consensus Γ that totally satisfies a maximum number of sources when a source Φi is defined as totally satisfied by Γ iff Φi ✓ Γ.

The consensuses defined so far handle all sources (resp., all formulas in the sources) with no specific priority or preference among them. There has been a tremendous amount of work in AI about preferred maximal satisfiable subsets of formulas (see e.g., [Martinez et al., 2013; Benferhat et al., 1998b]) when such priorities or preferences are to be taken into account. Adapting this to consensuses requires the additional condition of consistency with each source to be handled. Let us just give two examples.

A simple criterion discriminates among formulas by means of a pre-ordering between all formulas of Sni=1 Φi.

A consensus Γ for S is a max≺ consensus for S iff no consensus for S contains a formula ↵ such that ↵ ≺ β 8β 2 Γ.

Definition 5. Assume that a preference pre-ordering ≺ applies to all formulas in Sni=1 Φi in such a way that ↵ ≺ β whenever ↵ is preferred over β.

A second form of preference adapts a well-known way to handle inconsistencies in stratified belief bases ([Benferhat et al., 1998a; 1998b]) to the consensuses extraction problem: it gives each source a specific weight and states an ordering between these weights. Formally, this yields:

Definition 6. Assume that all Φi in [Φ1↪ ▷ ▷ ▷ ↪ Φn] are under a total ordering < such that Φi is preferred over Φj whenever i < j. A consensus Γ for S is a max[Φ1<···<Φn] consensus for S iff for every consensus Γ0 for S, @j 2 [1 ▷ ▷ ▷ n] s.t. 8i < j we have that (Γ \ Sik=1 Φk) = (Γ0 \ Sik=1 Φk) and (Γ \ Φj) ⇢ (Γ0 \ Φj).

Importantly, various forms of integrity constraints can be easily mixed up with the consensus concept: for instance, they can be formulas that can be external or not to S and that must belong to any consensus, or simply be satisfiable with any consensus. They can also be variables that represent concepts for which an agreement must be reached in the sense, for example, that any formula in S containing any occurrence of these variables must belong to any consensus. In the same vein, a pre-ordering among variables could express a preference ranking among variables on which preferred consensus should agree on.

6 More on max Consensuses vs. maxcons

Let us come back to the difference between max✓ (and max#) consensuses and maxcons. As every consensus is included in a maxcons, one natural question is whether or not a same set of consequences can be drawn from the intersection of either all max✓ (resp., max#) consensuses or all maxcons. Interestingly, the additional constraint requiring consistency with all sources makes both inference relations differ. Indeed, skeptical inference from max consensuses and maxcons differs in the general case. Assume X is a profile. The set of skeptical consequences fromX, noted SKI(X), is defined as follows.

Assume c 2 ¶✓↪#♦ in the following. Let us note C cS (resp., McS ) the set of all maxc consensuses (resp., maxconsc) for S.

maxcons have been used to define merging operators [Baral et al., 1991; Konieczny, 2000], so we can check which merging properties [Konieczny, 2000] are satisfied by max consensuses. This requires to modify slightly consensuses for S to include an additional non-empty set of formulas θ to play the role of integrity constraints; let us note C✓ S↪θ the corresponding operator:

Definition 8. A set Γ ⇢ L is a consensus for S under the constraints θ iff θ ✓ Γ ✓ Sni=1 Φi [θ and 8 Φi 2 S : Γ[Φi is satisfiable.

As consensuses are syntax-based and as their aim is distinct from the goal of merging operators, it is not a surprise that few properties from those operators are satisfied by C✓ S↪θ .

Proposition 2. C✓ S↪θ satisties (IC0) and (IC2). It does not satisfy (IC1), (IC3), (IC4), (IC5), (IC6), (IC7), (IC8).

Finally, about the relationship between the different notions of consensus: it is easy to show that using preferences allows more inferences to be drawn.

7 Computing one Preferred Consensus

We now present a generic computational framework for the extraction of consensuses for S according to any of the above preference paradigms and their possible stepwise combinations. As we make use of a single-type optimization process that maximizes the size of consensuses, we do not mix the max✓ with other preference criteria. Note that max# consensus is a max✓ consensus; one max✓ consensus can thus be computed by our technique, too.

We assume that every formula in S is a clause and we opportunely take advantage of the best advances of SAT-related technologies. This restriction is not an invincible limitation on the scope of our approach since every formula can be translated into a set of clauses while preserving satisfiability: each such set of clauses (vs. each clause) should then be treated as an elementary entity with respect to the various preference criteria and the algorithms that compute one consensus must be adapted `a la group-CNF (see e.g., [Belov and Marques-Silva, 2012; Nadel, 2010] for group-CNF techniques).

Although consensuses and satisfiable subsets are not identical concepts, the extraction of max consensuses can benefit from techniques to compute maxcons, at least to some extent. But, first, let us stress that computing one maxcons of a set of clauses is intractable in the worst case and so is the extraction of one max consensus. The extraction of one maxcons✓

belongs to the FP NP [wit↪ log] class, i.e., the set of function problems that can be computed in polynomial time by executing a logarithmic number of calls to an NP oracle that returns a witness for the positive outcome [Marques-Silva and Janota, 2014]. The extraction of one maxcons# belongs to the Opt-P class of problems [Papadimitriou and Yannakakis, 1991], i.e., the class of functions computable by taking the maximum of the output values over all accepting paths of an NP machine. In the worst case, the number of maxcons and of max consensuses for a profile is exponential with respect to the number of clauses in the profile. In this last respect, we propose a technique that will deliver one preferred consensus, only. For applications involving a lot of variables and formulas, extracting one such consensus can be sufficient to agree on a common position. A tentative enumeration of all preferred consensuses would require a form of iteration of the process and by augmenting the problem with a constraint stating that previously extracted consensuses should not be exhibited again (see for example [Liffiton and Sakallah, 2008] for this kind of enumeration technique).

Interestingly, recent techniques to compute one maxcons✓ or one maxcons# prove actually efficient for many problem instances: see for example [Gr´egoire et al., 2014; Marques-Silva et al., 2013; Menc´ıa et al., 2015]. This opens the way for computing one consensus even for very large sources. Consensuses differ from maxcons by an additional constraint that requires satisfiability with each one of the n sources. Since the sources can be mutually conflicting, this consistency constraint cannot be replaced by one satisfiability check with the conjunction (i.e., set-theoretical union) of these sources. It is also crucial to note that starting with Sni=1 Φi and pruning this set in a progressive and minimal manner so that it becomes satisfiable with more and more sources until it becomes satisfiable with all sources, does not necessarily deliver one max# (or max✓) satisfiable subset. As emphasized in [Besnard et al., 2015], this process would need to be repeated for all possible orderings of the sources, and all possible orderings of the clauses within each source, in order to guarantee maximality: such an iterated process leads to a combinatorial blow up since these numbers of orderings are exponential. In [Besnard et al., 2015], the authors have introduced a so-called transformational approach to compute one maximal set of clauses that does not contradict several given external contexts. Despite the increase of the size of the problem representation, this approach is currently the most efficient and scalable one for difficult and large instances.

max# First, we thus adapt this transformational approach in order to compute one max# consensus. Interestingly, we also generalize it so that it can extract one consensus under any stepwise combination of the preference paradigms presented above. The approach relies on the transformation of the search for one consensus into one instance of the Weighted Partial MaxSAT problem. This optimization problem requires the set of clauses to be partitioned into two subsets: the set of hard clauses (which must be satisfied in any solution) and the set of soft clauses (which are not necessarily satisfied in solutions). It searches one truth value assignment that satisfies all hard clauses and a maximum number of soft clauses. Actually, the soft clauses are given weights. Any solution must be such that the sum of the weights of the falsified clauses is minimal. [Besnard et al., 2015] made use of Partial MaxSAT only, missing the possibility to handle preferences among variables, clauses or sources, and the stepwise combinations of those preferences. Actually, we use a version of Weighted Partial Max-SAT that does not only deliver the maximal number of soft clauses satisfiable together with the hard clauses, but also the set of these satisfied clauses itself.

The adaptation of [Besnard et al., 2015] to the extraction of one max# consensus for S is as follows. Algorithm Transform1 illustrates the construction of the soft and hard clauses of the instance of the Weighted Partial MaxSAT problem.

Transform1(S) for max# input : S = [Φ1↪ ▷ ▷ ▷ ↪Φn]: a profile of n satisfiable sets of Boolean clauses ; Assume that the clauses of Φi are noted δ1 i ↪ δ2 i ↪ ▷ ▷ ▷ ; output: ΓHard: a set of hard clauses, ΓSoft: a set of soft clauses ΓHard ;; ΓSoft ;; 1 ⌃ SΦi2S ¶≻✏ji _ δj i s.t. δj i 2 Φi and where ✏ji are new fresh variables♦; 2 ΓSoft ¶✏ji ♦i↪j; 3 foreach Φi 2 S do 4 Φi ⌃[Φi; 5 Rename all variables in Φi (except the ✏ji ) with fresh new ones; 6 ΓHard ΓHard [Φi; 7 return (ΓHard, ΓSoft); 8

We need to find some subset of Sni=1 Φi that is satisfiable with each Φj. Each restriction of this satisfiability constraint to one Φj is considered as a subproblem; the subproblems will be linked together to form one single optimization problem. Each clause δj i from any Φi is augmented with an additional disjunct ≻✏ji using a new fresh variable (line 2): this yields a set ⌃. These ✏ji variables will be used to link the various subproblems. Each subproblem is created by unioning ⌃ with one Φi and by renaming all variables except the ✏ji (l. 4-7). All together, the subproblems form the set of hard clauses; these ones are all simultaneously satisfiable (just assign all ✏ji to true). The set of soft clauses is made of all unit clauses ✏ji (l. 3). If a same weight is assigned to every soft clause, this instance of Weighted Partial Max-SAT is actually an instance of Partial Max-SAT, which searches one truth-value assignment such that all hard clauses and one maximal number of clauses ✏ji are satisfied. Accordingly, all clauses δj i corresponding to the satisfied ✏ji form one max# consensus for S.

Even more linking variables and the use of weights The challenge is to keep one single optimization process while coping with other preferences and their combinations. To this end, we take advantage of both the weights on soft clauses and more ✏ji -like variables to link sub-problems. The weight, noted weight(↵), given to a soft clause ↵ can be used to enforce a stepwise prioritization between clauses or sources in the optimization process. In the previous representation, the set of the soft clauses is ¶✏ji ♦i↪j and when one ✏ji is satisfied in the Weighted Partial MaxSAT solution, this means that the clause δj i belongs to the computed consensus. To enforce the higher priority of ✏ji over a set ⇥ of other ✏lk clauses in any solution, weight(✏ji ) needs to be strictly greater than the total sum of the weights given to the clauses of ⇥.

max#100%Φi We augment the sets of hard and soft clauses delivered by Transform1 as follows. A new fresh variable 'i is associated to each Φi. The set of soft clauses is augmented with each 'i unit clause, whose weight is such that weight('i) > Pnj=i+1 weight('j) and weight('i) > Pk↪l weight(✏lk). The set of hard clauses is augmented with ¶≻'i _ ✏ji ♦i↪j . Hence, 'i with the biggest weights will be tentatively satisfied first. When 'i is satisfied, ✏ji is also satisfied for all j and so are all clauses of Φi.

max#ac For each variable x occurring in S, a new soft clause x0 is created where x0 is a new fresh variable. Then, additional clauses are created and inserted within the set of hard clauses for each x0 : they are the clausal form of x0 ! (✏ml ^ · · · ^ ✏qp) where the ✏ji are the variables corresponding to all the clauses in S that contain an occurrence of a literal containing x. Accordingly, Weighted Partial Max-SAT will maximize the number of satisfied clauses x0 : corresponding to each satisfied x0 , all the occurrences of clauses containing x or ≻x will be satisfied in the solution since ✏ji is itself satisfied. Again, weights need to be assigned to rank-order the priorities between the soft clauses to ensure the intended order between the selected criteria.

max[Φ1<···<Φn] The sets of soft and hard clauses are given by the Transform procedures above, with the following constraints on ✏ji (which weight must be bigger than any other types of soft clauses): 8i8j weight(✏ji ) > P(weight(✏ml ) 8δm l 2 Φl s.t. l > i).

max≺ Weights are assigned to soft clauses in a similar way to reflect a pre-ordering among clauses.

max#(max[Φ1<···<Φn]) and max≺(max#) As other examples of implementing sequential combinations of preferences, the ≻✏ji _δj i hard clauses are replaced by ≻✏ji _≻cji _δj i where cji are fresh variables. The set of soft clauses is augmented with the set ¶cji ♦i↪j. Weights are assigned according to the order between the criteria. Transform2 describes this process (weights are not represented).

Transform2(S) for max#(max[Φ1<···<Φn]) and max≺(max#) ΓHard ;; ΓSoft ;; 1 ⌃ SΦi2S ¶≻✏ji _≻cji _ δj i s.t. δj i 2 Φi (✏ji and cji are new variables)♦; 2 ΓSoft ¶✏ji ♦i↪j [ ¶cji ♦i↪j; 3 foreach Φi 2 S do 4 Φi ⌃[Φi; 5 Rename all variables in Φi (except the ✏ji and the cji ) with fresh new ones; 6 ΓHard ΓHard [Φi; 7 return (ΓHard, ΓSoft); 8

Interestingly, all these transformations can be combined. We have implemented a platform, called Consensus, which allows the computation of sequential combinations of preferences and criteria from this study. One practical limit is the maximal possible value for weight. Indeed, when the soft clauses are for example ranked in l different levels with m clauses per level and when strictly positive integers are considered, the maximum weight assigned to a clause is O(ml-1 ), which must not exceed the 264 maximum weight permitted by current best performing Weighted Partial MaxSAT solvers.

8 Experimental Study

All experimentations have been conducted on Intel Xeon E52643 (3.30GHz) processors with 8Gb RAM on Linux CentOS. We made used of MaxHS, the Weighted Partial MaxSAT solver from www.maxhs.org. We have implemented all the other algorithms in C++ on top of Glucose (www.labri.fr/ perso/lsimon/glucose). Our software, as well as the data and results of these experimentations are available at www.cril.fr/ consensus. The profiles S were based on the 291 different unsatisfiable (mostly real-world) instances from the 2011 MUS competition www.satcompetition.org/2011, which focused on the extraction of (set-inclusion) minimal unsatisfiable subsets, in short MUSes. The search for MUSes and maxcons are naturally related. Indeed, MUSes can be computed frommaxcons and conversely (see e.g. [Liffiton and Sakallah, 2005]). Let us stress that these instances are really challenging: they are formed of up to more than 15983000 clauses and 4426000 variables (457459 clauses using 139139 different variables, on average): their maxcons# are often made of a few clauses, only. Consensuses are thus necessarily not bigger than that. Each instance was randomly split into n 2 [3↪ 5↪ 7↪ 10] samesize (modulo n) Φi to yield all the S. When preferences that rank-order clauses were considered, 5 levels of preference were used: clauses were assigned randomly inside these levels so that each level contains a same number of clauses. When n ≥ 5 sources had to be rank-ordered, each source was assigned to one of the 5 levels, randomly. For n < 5 sources, we used n levels of preference between sources.

Consensus was run to transform each instance and extract one preferred consensus following max#, max#ac, max#100%Φi , max≺, max[Φ1<···<Φn], max#(max#ac), max[Φ1<···<Φn](max#) and max#(max#ac(max#100%Φi )), as a significant panel of criteria and of their combinations. Time-out was set to 900 seconds per consensus extraction.

Table 1 summarizes the average results for the extraction of one preferred consensus per criterion and value of n. It summarizes the 500+ Gb of detailed data results. For each criterion or combination of criteria, it gives the number of successful extractions, the average time in seconds to extract one preferred consensus, the average numbers of clauses and variables in the transformed instance and the average number of clauses in the extracted consensuses. When max#100%Φi was involved, it then gives the number of totally satisfied sources in the consensus. max#100%Φi was successful almost all the times (e.g., for n = 3, a consensus was found for each of the 291 instances, except one; for n = 10, 266 instances were solved). The drop of performance when n increases is clearly due to the increasing number of satisfiability constraints with each source in the transformed problem. Actually, increasing n entails both an increase of size of the representation of the transformed instance and additional satisfiability tests: as our experimentations illustrate, this affects all the considered criteria. A similar drop of performance was noticed for the max# criterion, which solved between 207 and 235 instances, depending on n. Interestingly, the approach proved somewhat less efficient for this latter criterion. One explanation for this phenomenon is as follows: under max#100%Φi , when some of the clauses of Φi have been shown already unsatisfied by the current truth assignment, the other clauses of Φi need not be examined under this assignment. This does not apply under max#. Not surprisingly, max[Φ1<···<Φn] and max≺ gave quite similar results in terms of successful extractions: except for n = 3 where the difference is more significant. More precisely, max[Φ1<···<Φn] has extracted a consensus for 232 (n = 3) and 135 (n = 10) instances whereas max≺ solved 137 and 133 instances for these values for n. On the one hand, the better result obtained under max[Φ1<···<Φn] for n = 3 can be explained by the fact that the number of clauses in S is then divided inside 3 strata whereas max≺ always classifies clauses inside 5 strata. Accordingly, since the number of clauses per stratum is often huge, the maximum possible value 264 for the weights permitted by the Weighted Partial MaxSAT solver is more quickly reached under max≺, leading to a memory fault. On the one hand, the decrease of performance with respect to the previously examined criteria is also explained by the fact that additional constraints of preference must be represented and taken into account for each clause or source in S.

For max#ac, as the number of constraints is significantly increased in the transformed instance, it does not come as a surprise that, globally, the number of solved instances is lower than all the above criteria (it ranges from 117 to 102, depending on n). Interestingly, the combination of max#(max#ac) allowed to solve almost the same number of instances than max#ac alone (a difference of at most 4 instances, only). This does neither come as a surprise since the max# criterion does not require coping with additional clauses when it is considered together with max#ac. max#(max#ac(max#100%Φi )) allowed to solve between 60 and 35 instances, only. The combination max[Φ1<···<Φn](max#) allowed us to extract one consensus for a somewhat smaller number of instances, only (except for n = 3 for a reason already explained). These numbers might appear low, but remember that we are addressing here huge hard benchmarks allowing for very small -hard to findconsensuses, only. These results show the viability of the approach and its scalability, at least provided that the number of strata or preference levels that must be obeyed remains small.

9 Conclusion and Perspectives

The contribution of this paper is twofold. On the one hand, we have proposed a logic-based concept of consensus that does not merely amount to computing some shared information. On the other hand, we have shown how this consensus concept augmented with various preference paradigms can be computed in practice. Noticeably, the approach circumvents -at least to some extent- the computational blow-up due to the investigation of all orders between formulas that is necessary to guarantee maximality, and to the necessity to check satisfiability with each source separately. Mainly, the whole task is rewritten into one single optimization problem. Interestingly, we have shown how to allow various preference criteria to be combined and computed in this framework, too.

We envision various promising paths for further research. First, group-CNF algorithms could be explored to extend the computational approach from clauses to all formulas. The practical handling of preferences that define a large number of levels or strata for large sources remains an open problem. Adapting the approach into an efficient multi-steps optimization process to address this issue is a promising path worth exploring. From an application perspective, consensuses can play a role in various AI fields.

For instance, our approach could be exported to argumentation frameworks. Caminada and Pigozzi [2011] consider a notion of consensus between the positions of agents expressed by a labeling, given a common abstract argumentation. Since abstract argumentation can be encoded in propositional logic [Besnard and Doutre, 2004], it would be interesting to check whether our specific approach to consensus and its computational counterpart could open new perspectives for such investigations about abstract argumentation.