Applied Satisfiability - Miyuki Koshimura

. .

Résumé :

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...

Biographie:

Xiaojuan Liao, PhD, is an Associate Professor in the College of Computer and Cyber Security, Chengdu University of Technology, Chengdu, China.

Miyuki Koshimura, PhD, is an Assistant Professor in the Faculty of Information Science and Electrical Engineering, Kyushu University, Fukuoka, Japan....

Sommaire:

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....