Verification of some Boolean partial polymorphisms

<p>This dataset contains the formal verification that a certain partial ternary Boolean conjunction <em>f</em> 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:</p> <table> <tbody><tr> <th>Filename</th> <th>Purpose</th> </tr> </tbody><tbody> <tr> <td>f-pPol-GammaL0chi2-GammaL2chi3.<br> z3</td> <td>The SMT-LIB2.0 implementation of the problem, to be run, e.g. by Z3.</td> </tr> <tr> <td>z3-output.txt</td> <td>The output received by running Z3 on f-pPol-GammaL0chi2-GammaL2chi3.<br> z3</td> </tr> <tr> <td>f-preserves-GammaL0chi2_proof.txt</td> <td>A formal proof generated by Z3 that <em>f</em> preserves &Gamma;_L₀(&chi;₂).</td> </tr> <tr> <td>f-preserves-GammaL2chi3_proof.txt</td> <td>A formal proof generated by Z3 that <em>f</em> preserves &Gamma;_L₂(&chi;₃).</td> </tr> <tr> <td>partial_polymorphisms.pdf</td> <td>A detailed description of the problem and the dataset.</td> </tr> <tr> <td>partial_polymorphisms.tex</td> <td>The source file used to produce partial_polymorphisms.pdf</td> </tr> </tbody> </table> <p>&nbsp;</p>