New Insights Into the Similarity and Difference of Propositional Models Via Symmetry Open Access

Przybylinski, Thomas John (2015)

Permanent URL:


Recently, there has been an increased interest in finding diverse solutions to propositional formula. Modern SAT solvers are capable of producing a large number of models very efficiently. However, this can result in an overwhelming number of nearly indistinguishable results. Hence, finding a general way to discount most of these variants and leaving a semantically diverse set of solutions is an important problem. Historically, diversity techniques concentrated on distance, while uniform sampling and global symmetries have been put forward as diversity concepts. No work in this area has closely examined diversity in general nor examined when their concepts return inferior results. In this dissertation we closely examine different notions of diversity, and show that existing criteria are lacking in different ways. We present a structure for unifying and combining previous notions of diversity, and study their relative power to discriminate solutions. We then consider two new notions of diversity: local symmetry and constructive symmetry, that we show to be more intuitively satisfying. We analyze theoretical and computational properties, and present different algorithms. A comprehensive set of experiments are presented to explore different strategies.

Table of Contents

1 Introduction. 1

2 Technical Background and Related Work. 3

2.1 Propositional Logic. 3

2.2 Isomorphims, Symmetry, and Automorphisms. 4

2.3 Background Work. 5

2.3.1 Diversity. 5

2.3.2 Local Symmetry. 6

2.4 Diverse Models and Data Mining. 7

3 Augmenting Symmetry. 9

3.1 Generalizing Diversity. 9

3.1.1 Diversity Graphs. 10

3.1.2 Symmetry-Aware Distance. 12

3.2 Calculating Symmetry. 14

3.2.1 JAUNTY. 14

3.2.2 Internal Representation. 16

3.2.3 Refinement. 18

3.2.4 Pruning. 19

4 Local Symmetry 20

4.1 Local Symmetry Diversity. 20

4.1.1 Introduction. 20

4.1.2 Computational Properties. 24

4.2 Algorithms. 30

4.2.1 Complete Offline Local Symmetries. 30

4.2.2 Other Algorithms. 39

4.3 Comparing Discrimination. 53

5 Constructive Symmetry. 64

5.1 Introduction. 64

5.2 Constructive Symmetry Properties. 66

5.3 A General Algorithm. 69

5.4 Improving Constructive Symmetry. 71

5.4.1 Restricting Choices. 71

5.4.2 Shallow Approximation. 73

5.5 Results. 74

6 Discussion. 80

6.1 Overview of Completed Work. 80

6.2 Future Work. 83

6.2.1 Link Analysis. 83

6.2.2 Complete Symmetry. 84

6.2.3 Over-estimating Symmetry. 85

6.3 Conclusion. 86

Bibliography. 87

About this Dissertation

Rights statement
  • Permission granted by the author to include this thesis or dissertation in this repository. All rights reserved by the author. Please contact the author for information regarding the reproduction and use of this thesis or dissertation.
  • English
Research Field
Committee Chair / Thesis Advisor
Committee Members
Last modified

Primary PDF

Supplemental Files