Preface ix
1 Satisfiability Theories 1
1.1 Boolean Satisfiability (SAT) 1
1.2 Maximum Satisfiability (MaxSAT) 3
1.3 Satisfiability Algorithms 4
1.3.1 SAT Algorithms 5
1.3.2 MaxSAT Algorithms 8
1.4 Chapter Summary 11
References 11
2 Encoding in General 21
2.1 CNF Encodings 21
2.1.1 Transformation by Boolean Algebra 22
2.1.2 Transformation by Tseitin Encoding 24
2.2 Satisfiability Problem-Solving Environments 25
2.2.1 DIMACS Format 26
2.2.2 PySAT: Python Toolkit 28
2.3 Case Study 33
2.4 Chapter Summary 36
References 36
3 SAT Encoding for AES Partial Key Recovery 39
3.1 Logical Cryptanalysis with SAT 39
3.2 Cold Boot Attack 41
3.3 Advanced Encryption Standard (AES) 42
3.4 Decay Pattern Assumptions and AES Key Recovery Solutions 44
3.5 SAT Approach for Recovering AES Key Schedules 46
3.6 Performance Evaluation 48
3.7 Chapter Summary 50
References 50
4 MaxSAT Encoding for AES Partial Key Recovery 55
4.1 Original Partial MaxSAT Approach 55
4.2 Improved Partial MaxSAT Approach 58
4.3 Performance Evaluation 62
4.3.1 Results of SAT and Original Partial MaxSAT Approaches 62
4.3.2 Results of Two Partial MaxSAT Approaches 64
4.4 Chapter Summary 65
References 65
5 Job-Shop Scheduling 67
5.1 Job-shop Scheduling Model 67
5.2 SAT Approach 69
5.3 Performance Evaluation 70
5.3.1 Solving ABZ9 and YN 1 71
5.3.2 Improving LB and UB 73
5.4 Chapter Summary 73
References 74
6 Overloaded Scheduling 77
6.1 Overloaded Scheduling Model 77
6.2 Weighted Partial MaxSAT Approach 79
6.2.1 Feature Preprocessing 80
6.2.2 WPM Formulation 81
6.2.3 A Pedagogical Example 83
6.3 Theoretical Discussion 85
6.3.1 Similarities of PM and WPM Formulations 86
6.3.2 WPM Improvement 86
6.4 Performance Evaluation 89
6.4.1 Experimental Design 90
6.4.2 Comparison on Weighted Cases 91
6.4.3 Comparison on Unweighted Cases 91
6.5 Adaption for Parallel-machine Scheduling Problem 96
6.6 Chapter Summary 97
References 98
7 Restricted Preemptive Scheduling 101
7.1 Restricted Preemptive Scheduling Model 101
7.2 Mathematical Programming 104
7.3 SAT Approach 106
7.4 MaxSAT Approach 110
7.5 Performance Evaluation 111
7.5.1 Evaluation on the Optimal Makespan 112
7.5.2 Evaluation on Preemption Granularity k 114
7.5.2.1 Evaluation on Number of Machines m 115
7.5.3 Evaluation on Scalability 118
7.6 Evaluating Heuristics 120
7.7 Chapter Summary 121
References 122
8 Rule Relation-Based Weighted Partial MaxSAT (RWPM) Encoding 125
8.1 Problem Statement 125
8.1.1 Characteristic Function Game 127
8.1.2 Partition Function Game 129
8.2 Representative Algorithms 131
8.2.1 An Overview 131
8.2.2 Revisiting Important Works 132
8.3 Encoding Rule Relations into WPM 134
8.3.1 Encoding Positive Value Rules 135
8.3.2 Encoding Positive Value Embedded Rules 138
8.3.3 Encoding Negative Value Rules 140
8.3.4 Encoding Negative Value Embedded Rules 143
8.4 Performance Evaluation 145
8.5 Chapter Summary 146
References 147
9 Agent Relation-Based Weighted Partial MaxSAT (AWPM) Encoding 151
9.1 Extended Weighted Partial MaxSAT 151
9.1.1 EWPM-to-WPM Transformation 152
9.1.2 Redundancy in Transformation 155
9.1.3 MinSAT Extension 156
9.2 Encoding Agent Relations into WPM 156
9.2.1 Agent Relation 157
9.2.2 Encoding Positive Value Rules 159
9.2.3 Encoding Positive Value Embedded Rules 160
9.2.4 Encoding Negative Value Rules 162
9.2.5 Encoding Negative Value Embedded Rules 163
9.3 Performance Evaluation 165
9.4 Chapter Summary 166
References 167
10 Comparative Analysis and Improvement of RWPM 169
10.1 Motivation 169
10.2 Comparative Study on RWPM and AWPM 170
10.2.1 Comparing the Number of Boolean Variables 170
10.2.2 Comparing the Number of Clauses 172
10.3 An Interesting Phenomenon: Analysis on a Special Case 175
10.4 RWPM with Refined Transitive Laws (RWPM-RT) 177
10.5 Performance Evaluation 181
10.5.1 Results in a Special Case 181
10.5.2 Results in a General Case 182
10.6 Chapter Summary 184
References 184
11 Improved Rule Relation-Based WPM (I-RWPM) 187
11.1 Motivation 187
11.2 Identify Freelance Rules in an MC-Net 189
11.3 Improved Weighted Partial MaxSAT Encoding on Refined MC-Nets 192
11.3.1 I-RWPM Encoding Theory 193
11.3.2 Interpretation of I-RWPM 195
11.3.3 Pedagogical Examples 196
11.4 Performance Evaluation 199
11.4.1 Results in a General Case 199
11.4.2 Results with Varied Number of Freelance Rules 200
11.4.3 Results with Few Freelance Rules 201
11.5 Chapter Summary 203
References 203
Appendix A Complete File for Solving 4-Queens in DIMACS Format 205
Appendix B A Sample of Sbox Expressed in ANF 209
Appendix C
Appendix D
Appendix E
Appendix F
Appendix G
Appendix H
Appendix I
Appendix J Appendix K Complete File Generated by MaxSAT for Solving Overloaded Scheduling in WPM Input Format 215
Complete File Generated by RWPM for Example 8.9 in WPM Input Format 217
Complete File Generated by RWPM for Example 8.11 in WPM Input Format 219
Complete File Generated by RWPM for Example 8.12 in WPM Input Format 221
Complete File Generated by RWPM for Example 8.13 in WPM Input Format 223
Complete File Generated by AWPM for Example 9.2 in WPM Input Format 229
Complete File Generated by AWPM for Example 9.3 in WPM Input Format 231
Complete File Generated by AWPM for Example 9.4 in WPM Input Format 233
Complete File Generated by AWPM for Example 9.5 in WPM Input Format 235
Appendix L Proof of Formula in Lemma 10.3 237
Appendix M Calculation of ?m in Chapter 10 239
Appendix N Appendix O Complete File Generated by RWPM-RT for Example 10.3 in WPM Input Format 241
Complete File Generated by RWPM-RT for Example 10.4 in WPM Input Format 243
Appendix P Comparative Analysis of RWPM and I-RWPM 245
Appendix Q
Appendix R Complete File Generated by I-RWPM for Example 11.3 in WPM Input Format 251
Complete Files Generated by I-RWPM and RWPM-RT for Example 11.4 in WPM Input Format 253
Appendix S Theoretical Analysis on d 255
Index 257
