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

Abstract

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.

School	Laney Graduate School
Department	Math and Computer Science
Degree	PhD
Submission	Dissertation
Language	English
Research Field	Computer Science Artificial Intelligence
Keyword	Symmetry Propositional Logic Local Symmetry Diversity
Committee Chair / Thesis Advisor	Lu, James, Emory University
Committee Members	Xiong, Li, Emory University Grigni, Michelangelo, Emory University

Last modified

Primary PDF

Thumbnail	Title	Date Uploaded	Actions
	New Insights Into the Similarity and Difference of Propositional Models Via Symmetry ()	2018-08-28 14:32:02 -0400	Press to Select an action Download

Supplemental Files

Thumbnail	Title	Date Uploaded	Actions