Applied Satisfiability: Cryptography, Scheduling, and Coalitional Games

Apply satisfiability to a range of difficult problems The Boolean Satisfiability Problem (SAT) is one of the most famous and widely-studied problems in Boolean logic. Optimization versions of this problem include the Maximum Satisfiability Problem (MaxSAT) and its extensions, such as partial MaxSAT and weighted MaxSAT, which assess whether, and to what extent, a solution satisfies a given set of problems. Numerous applications of SAT and MaxSAT have emerged in fields related to logic and computing technology. Applied Satisfiability: Cryptography, Scheduling, and Coalitional Games outlines some of these applications in three specific fields. It offers a huge range of SAT applications and their possible impacts, allowing readers to tackle previously challenging optimization problems with a new selection of tools. Professionals and researchers in this field will find the scope of their computational solutions to otherwise intractable problems vastly increased. Applied Satisfiability readers will also find: Coding and problem-solving skills applicable to a variety of fields Specific experiments and case studies that demonstrate the effectiveness of satisfiability-aided methods Chapters covering topics including cryptographic key recovery, various forms of scheduling, coalition structure generation, and many more Applied Satisfiability is ideal for researchers, graduate students, and practitioners in these fields looking to bring a new skillset to bear in their studies and careers.

Table of Contents:
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