<jupyter_start><jupyter_text>Z3 Proofs of Preference LanguageThe notebook investigates proofs of standard properties for different preference logic semantics.<jupyter_code>from z3 import *
from itertools import product, repeat<jupyter_output><empty_output><jupyter_text>The following function generates the set of mutually exclusive and exhaustive classes induced by `num_outcome` outcomes.<jupyter_code>def gen_classes(num_outcomes):
    classes_ = product([0, 1], repeat=num_outcomes)
    classes_ = {f"C_{''.join([str(i) for i in cls])}" for cls in classes_}
    return classes_

# Uncomment to see output.
print(gen_classes(2))
print(gen_classes(3))<jupyter_output>{'C_11', 'C_00', 'C_01', 'C_10'}
{'C_010', 'C_000', 'C_011', 'C_111', 'C_101', 'C_001', 'C_100', 'C_110'}<jupyter_text>The following function generates a dictionary of propositions `{p_name: p}` indicating the given word belongs to which class. For example, given a word `u`, the proposition `u_001` means that `u` satisfies $\varphi_3$ but not $\varphi_1, \varphi_2$.<jupyter_code>def gen_propositions(word, num_outcomes):
    props_ = product([0, 1], repeat=num_outcomes)
    props_ = {f"{word}_{''.join([str(i) for i in prop])}" for prop in props_}
    return {p: Bool(p) for p in props_}

# Uncomment to see output.
print(gen_propositions("u", 2))<jupyter_output>{'u_10': u_10, 'u_00': u_00, 'u_01': u_01, 'u_11': u_11}<jupyter_text>Given a dictionary of propositions, the following function generates a set of constraints representing that each word is exclusively belongs to a unique class.<jupyter_code>def gen_exclusivity_constraint(props_):
    constraints_ = []
    for p_name in props_:
        p = props_[p_name]
        p_constraints = [p]
        
        for q_name in props_:
            if q_name == p_name:
                continue
            p_constraints.append(Not(props_[q_name]))
        
        constraints_.append(And(p_constraints))

    return Or(constraints_)

# Uncomment to see output.
u_props = gen_propositions("u", 2)
g = gen_exclusivity_constraint(u_props)
g<jupyter_output><empty_output><jupyter_text>The exclusivity constraint generated by Z3 operations lacks appropriate brackets in the output. Let us verify if the constraint is generated correctly by enforcing two propositions to be true at once.<jupyter_code># Create Z3 Solver.
s = Solver()

# One proposition holds at a time.
s.reset()
s.add(g)
s.add(u_props["u_00"])
print("u_00: True -> ", str(s.check()))

s.reset()
s.add(g)
s.add(u_props["u_01"])
print("u_01: True -> ", str(s.check()))

s.reset()
s.add(g)
s.add(u_props["u_10"])
print("u_10: True -> ", str(s.check()))

s.reset()
s.add(g)
s.add(u_props["u_11"])
print("u_11: True -> ", str(s.check()))

# Two propositions hold at a time.
s.add(g)
s.add(u_props["u_01"])
s.add(u_props["u_10"])
print("u_01 & u_10: True -> ", str(s.check()))<jupyter_output>u_00: True ->  sat
u_01: True ->  sat
u_10: True ->  sat
u_11: True ->  sat
u_01 & u_10: True ->  unsat<jupyter_text>Free semantics for preferencesSuppose a strict preference is interpreted in exclusionary sense. That is, $\varphi_1 \triangleright \varphi_2$ means that satisfying $\varphi_1$ (and not $\varphi_2$) is strictly preferred to satisfying $\varphi_2$ (and not $\varphi_1$). Also, let the set of outcomes be $\{\varphi_1, \varphi_2, \varphi_3\}$. In this case, free (= non-Ceteris Paribus) semantics of preferences interpretes $(u, v) \models \varphi_1 \triangleright \varphi_2$ holds if $u \models \varphi_1 \land \neg \varphi_2$ and $v \models \neg \varphi_1 \land \varphi_2$, regardless of whether $u, v$ satisfy $\varphi_3$. On the contrary, CP (Ceteris Paribus) semantics of preference interprets $(u, v) \models \varphi_1 \triangleright \varphi_2$ to hold when $u \models \varphi_1 \land \neg \varphi_2$ and $v \models \neg \varphi_1 \land \varphi_2$, if either $u, v$ both satisfy $\varphi_3$, or both do not satisfy $\varphi_3$. **IS THIS CORRECT?**We start by studying free semantics. **Nomenclature**Function named `fs_strict` means a strict preference under free semantics. Whereas, `cp_strict` means strict preference under CP-semantics. - `mpo`: (int) more preferred outcome index.- `lpo`: (int) less preferred outcome index.- `uprops`: (dict) dictionary of propositions corresponding to word `u`- `vprops`: (dict) dictionary of propositions corresponding to word `v`The functions will generate a z3 constraint for $(u, v) \models \psi$.<jupyter_code>def fs_strict(mpo, lpo, uprops, vprops):
    # Case 1: u \in C_10, v \in C_01 or C_00 (other specs may be 0 or 1).
    u_c10 = [uprops[p] for p in uprops if p[mpo+1] == "1" and p[lpo+1] == "0"]
    v_c01 = [vprops[p] for p in vprops if p[mpo+1] == "0" and p[lpo+1] == "1"]
    v_c00 = [vprops[p] for p in vprops if p[mpo+1] == "0" and p[lpo+1] == "0"]
    u = Or(u_c10)
    v = Or(v_c01 + v_c00)
    constraint_1 = And(u, v)
#     print(constraint_1)

    # Case 2: u \in C_01, v \in C_00 (other specs may be 0 or 1).
    u_c01 = [uprops[p] for p in uprops if p[mpo+1] == "0" and p[lpo+1] == "1"]
    v_c00 = [vprops[p] for p in vprops if p[mpo+1] == "0" and p[lpo+1] == "0"]
    u = Or(u_c01)
    v = Or(v_c00)
    constraint_2 = And(u, v)
#     print(constraint_2)
    
    return Or(constraint_1, constraint_2)


def fs_indiff(mpo, lpo, uprops, vprops):
    u_c10 = [uprops[p] for p in uprops if p[mpo+1] == "1" and p[lpo+1] == "0"]
    u_c01 = [uprops[p] for p in uprops if p[mpo+1] == "0" and p[lpo+1] == "1"]
    u_c11 = [uprops[p] for p in uprops if p[mpo+1] == "1" and p[lpo+1] == "1"]
    
    v_c10 = [vprops[p] for p in vprops if p[mpo+1] == "1" and p[lpo+1] == "0"]
    v_c01 = [vprops[p] for p in vprops if p[mpo+1] == "0" and p[lpo+1] == "1"]
    v_c11 = [vprops[p] for p in vprops if p[mpo+1] == "1" and p[lpo+1] == "1"]
    
    # Case 1: u \in C_01 U C_10 U C_11 and v \in C_01 U C_10 U C_11
    u = Or(u_c10 + u_c01 + u_c11)
    v = Or(v_c10 + v_c01 + v_c11)
    constraint_1 = And(u, v)
    
    # Case 2: u \in C_00 and v \in C_00
    u_c00 = [uprops[p] for p in uprops if p[mpo+1] == "0" and p[lpo+1] == "0"]
    v_c00 = [vprops[p] for p in vprops if p[mpo+1] == "0" and p[lpo+1] == "0"]
    constraint_2 = And(u_c00, v_c00)
    
    return Or(constraint_1, constraint_2)
    
    
def fs_incomp(mpo, lpo, uprops, vprops):
    u_c10 = [uprops[p] for p in uprops if p[mpo+1] == "1" and p[lpo+1] == "0"]
    u_c01 = [uprops[p] for p in uprops if p[mpo+1] == "0" and p[lpo+1] == "1"]
    u_c11 = [uprops[p] for p in uprops if p[mpo+1] == "1" and p[lpo+1] == "1"]
    u_c00 = [uprops[p] for p in uprops if p[mpo+1] == "0" and p[lpo+1] == "0"]
    
    v_c10 = [vprops[p] for p in vprops if p[mpo+1] == "1" and p[lpo+1] == "0"]
    v_c01 = [vprops[p] for p in vprops if p[mpo+1] == "0" and p[lpo+1] == "1"]
    v_c11 = [vprops[p] for p in vprops if p[mpo+1] == "1" and p[lpo+1] == "1"]
    v_c00 = [vprops[p] for p in vprops if p[mpo+1] == "0" and p[lpo+1] == "0"]
    
    # Case 1: u \in C_00 and v \notin C_00
    constraint_1 = And(u_c00, Or(v_c01, v_c10, v_c11))
    
    # Case 2: u \in C_01 and v \notin C_01
    constraint_2 = And(u_c01, Or(v_c00, v_c10, v_c11))
    
    # Case 3: u \in C_10 and v \notin C_10
    constraint_3 = And(u_c10, Or(v_c00, v_c01, v_c11))
    
    # Case 4: u \in C_11 and v \notin C_00
    constraint_4 = And(u_c11, Or(v_c00, v_c01, v_c10))
    
    return Or(constraint_1, constraint_2, constraint_3, constraint_4)


def fs_and(constraint_1, constraint_2):
    return And(constraint_1, constraint_2)


def fs_and(constraint_1, constraint_2):
    return Or(constraint_1, constraint_2)
# Uncomment to see output
uprops = gen_propositions("u", 3)
vprops = gen_propositions("v", 3)
fs_strict(1, 2, uprops, vprops)<jupyter_output><empty_output><jupyter_text>In the remainder, we will prove the following properties using validity testing. * PP-Transitivity, i.e. transitivity of strict preference* II-Transitivity, i.e. transitivity of indifference* PI-Transitivity* IP-Transitivity* Left Disjunctive Distribution* Right Disjunctive Distribution**Approach**:Consider PP-transitivity $$\varphi_1 \triangleright \varphi_2 \land \varphi_2 \triangleright \varphi_3 \implies \varphi_1 \triangleright \varphi_3$$We will formulate a SAT problem by deriving constraints $f$ from semantics `fs_strict`. Then, validity of PP-transitivity statement is checked by testing whether $\neg f$ is UNSAT.  **Test Example**A test example is given below.<jupyter_code>s = Solver()

p = Bool('p')
q = Bool('q')
f = Implies(p, q)                                            # f = p => q
s.add(Not(f))
s.check()

s.reset()
p = Bool('p')
f = Or(p, Not(p))                                            # f = p | !p
s.add(Not(f))
print(s)
s.check()<jupyter_output>[Not(Or(p, Not(p)))]<jupyter_text>**PP-transitivity**<jupyter_code>uprops = gen_propositions("u", 3)
vprops = gen_propositions("v", 3)

# Get constraints from semantics
constraint_12 = fs_strict(1, 2, uprops, vprops)
constraint_23 = fs_strict(2, 3, uprops, vprops)
constraint_13 = fs_strict(1, 3, uprops, vprops)

print(constraint_12)
print(constraint_23)
print(constraint_13)

# Assert exclusiveness
u_exclusive = gen_exclusivity_constraint(uprops)
v_exclusive = gen_exclusivity_constraint(vprops)
# print(simplify(u_exclusive))
# print(simplify(v_exclusive))

constraint_12 = And([u_exclusive, v_exclusive, constraint_12])
constraint_23 = And(u_exclusive, v_exclusive, constraint_23)
constraint_13 = And(u_exclusive, v_exclusive, constraint_13)
print(simplify(constraint_12))


f = Implies(And(constraint_12, constraint_23), constraint_13)
# print(f)

s = Solver()
s.add(Not(f))
print(s.check())
for p in s.model():
     print(p, s.model()[p])<jupyter_output>Or(And(Or(u_101, u_100), Or(v_010, v_011, v_000, v_001)),
   And(Or(u_011, u_010), Or(v_000, v_001)))
Or(And(Or(u_110, u_010), Or(v_101, v_001, v_000, v_100)),
   And(Or(u_001, u_101), Or(v_000, v_100)))
Or(And(Or(u_110, u_100), Or(v_011, v_001, v_000, v_010)),
   And(Or(u_001, u_011), Or(v_000, v_010)))
And(Or(And(u_110,
           Not(u_111),
           Not(u_001),
           Not(u_011),
           Not(u_101),
           Not(u_000),
           Not(u_100),
           Not(u_010)),
       And(u_111,
           Not(u_110),
           Not(u_001),
           Not(u_011),
           Not(u_101),
           Not(u_000),
           Not(u_100),
           Not(u_010)),
       And(u_001,
           Not(u_110),
           Not(u_111),
           Not(u_011),
           Not(u_101),
           Not(u_000),
           Not(u_100),
           Not(u_010)),
       And(u_011,
           Not(u_110),
           Not(u_111),
           Not(u_001),
           Not(u_101),
           Not(u_000),
           Not(u_100)[...]
{'fraction_non_alphanumeric': 0.14713030472985605, 'fraction_numerical': 0.05832865956253505, 'mean_word_length': 3.6017204301075267, 'pattern_counts': {'":': 0, '<': 28, '<?xml version=': 0, '>': 39, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '8', 'dir': 'jupyter-structured-clean-dedup', 'id': '55829', 'license': 'BSD-3-Clause', 'n_tokens_mistral': 4555, 'n_tokens_neox': 4157, 'n_words': 1154, 'path': 'jp-notebooks/pref-scltl-semantics-3.ipynb', 'repo_name': 'abhibp1993/preference-planning', 'size': '10698'}