Verification of some Boolean partial polymorphisms

This dataset contains the formal verification that a certain partial ternary Boolean conjunction f preserves two specific Boolean relations, but does not preserve two other ones. Our approach is by translating the question into Boolean satisfiability problems and to implement these such that they can be treated by a sat solver being capable of reading SMT-LIB2.0 specifications. Specifically, we have been using the Z3 solver developed by Microsoft Research (https://github.com/z3prover/z3) to attack the problem. The following is a list of the files contained in the dataset and their function:

Filename
Purpose

f-pPol-GammaL0chi2-GammaL2chi3.
z3
The SMT-LIB2.0 implementation of the problem, to be run, e.g. by Z3.

z3-output.txt
The output received by running Z3 on f-pPol-GammaL0chi2-GammaL2chi3.
z3

f-preserves-GammaL0chi2_proof.txt
A formal proof generated by Z3 that f preserves ΓL₀(χ₂).

f-preserves-GammaL2chi3_proof.txt
A formal proof generated by Z3 that f preserves ΓL₂(χ₃).

partial_polymorphisms.pdf
A detailed description of the problem and the dataset.

partial_polymorphisms.tex
The source file used to produce partial_polymorphisms.pdf