Preface -- 1 Satisfiability Theories -- 1.1 Boolean Satisfiability (SAT) -- 1.2 Maximum Satisfiability (MaxSAT) -- 1.3 Satisfiability Algorithms -- 1.3.1 SAT Algorithms -- 1.3.2 MaxSAT Algorithms -- 1.4 Chapter Summary -- References -- 2 Encoding in General -- 2.1 CNF Encodings -- 2.1.1 Transformation by Boolean Algebra -- 2.1.2 Transformation by Tseitin Encoding -- 2.2 Satisfiability Problem-Solving Environments -- 2.2.1 DIMACS Format -- 2.2.2 PySAT: Python Toolkit -- 2.3 Case Study -- 2.4 Chapter Summary -- References -- 3 SAT Encoding for AES Partial Key Recovery -- 3.1 Logical Cryptanalysis with SAT -- 3.2 Cold Boot Attack -- 3.3 Advanced Encryption Standard (AES) -- 3.4 Decay Pattern Assumptions and AES Key Recovery Solutions -- 3.5 SAT Approach for Recovering AES Key Schedules -- 3.6 Performance Evaluation -- 3.7 Chapter Summary -- References -- 4 MaxSAT Encoding for AES Partial Key Recovery -- 4.1 Original Partial MaxSAT Approach -- 4.2 Improved Partial MaxSAT Approach -- 4.3 Performance Evaluation -- 4.3.1 Results of SAT and Original Partial MaxSAT Approaches -- 4.3.2 Results of Two Partial MaxSAT Approaches -- 4.4 Chapter Summary -- References -- 5 Job-Shop Scheduling -- 5.1 Job-shop Scheduling Model -- 5.2 SAT Approach -- 5.3 Performance Evaluation -- 5.3.1 Solving ABZ9 and YN 1 -- 5.3.2 Improving LB and UB -- 5.4 Chapter Summary -- References -- 6 Overloaded Scheduling -- 6.1 Overloaded Scheduling Model -- 6.2 Weighted Partial MaxSAT Approach -- 6.2.1 Feature Preprocessing -- 6.2.2 WPM Formulation -- 6.2.3 A Pedagogical Example -- 6.3 Theoretical Discussion -- 6.3.1 Similarities of PM and WPM Formulations -- 6.3.2 WPM Improvement -- 6.4 Performance Evaluation -- 6.4.1 Experimental Design -- 6.4.2 Comparison on Weighted Cases -- 6.4.3 Comparison on Unweighted Cases -- 6.5 Adaption for Parallel-machine Scheduling Problem -- 6.6 Chapter Summary -- References -- 7 Restricted Preemptive Scheduling -- 7.1 Restricted Preemptive Scheduling Model -- 7.2 Mathematical Programming -- 7.3 SAT Approach -- 7.4 MaxSAT Approach -- 7.5 Performance Evaluation -- 7.5.1 Evaluation on the Optimal Makespan -- 7.5.2 Evaluation on Preemption Granularity k -- 7.5.2.1 Evaluation on Number of Machines m -- 7.5.3 Evaluation on Scalability -- 7.6 Evaluating Heuristics -- 7.7 Chapter Summary -- References -- 8 Rule Relation-Based Weighted Partial MaxSAT (RWPM) Encoding -- 8.1 Problem Statement -- 8.1.1 Characteristic Function Game -- 8.1.2 Partition Function Game -- 8.2 Representative Algorithms -- 8.2.1 An Overview -- 8.2.2 Revisiting Important Works -- 8.3 Encoding Rule Relations into WPM -- 8.3.1 Encoding Positive Value Rules -- 8.3.2 Encoding Positive Value Embedded Rules -- 8.3.3 Encoding Negative Value Rules -- 8.3.4 Encoding Negative Value Embedded Rules -- 8.4 Performance Evaluation -- 8.5 Chapter Summary -- References -- 9 Agent Relation-Based Weighted Partial MaxSAT (AWPM) Encoding -- 9.1 Extended Weighted Partial MaxSAT -- 9.1.1 EWPM-to-WPM Transformation -- 9.1.2 Redundancy in Transformation -- 9.1.3 MinSAT Extension -- 9.2 Encoding Agent Relations into WPM -- 9.2.1 Agent Relation -- 9.2.2 Encoding Positive Value Rules -- 9.2.3 Encoding Positive Value Embedded Rules -- 9.2.4 Encoding Negative Value Rules -- 9.2.5 Encoding Negative Value Embedded Rules -- 9.3 Performance Evaluation -- 9.4 Chapter Summary -- References -- 10 Comparative Analysis and Improvement of RWPM -- 10.1 Motivation -- 10.2 Comparative Study on RWPM and AWPM -- 10.2.1 Comparing the Number of Boolean Variables -- 10.2.2 Comparing the Number of Clauses -- 10.3 An Interesting Phenomenon: Analysis on a Special Case -- 10.4 RWPM with Refined Transitive Laws (RWPM-RT) -- 10.5 Performance Evaluation -- 10.5.1 Results in a Special Case -- 10.5.2 Results in a General Case -- 10.6 Chapter Summary -- References -- 11 Improved Rule Relation-Based WPM (I-RWPM) -- 11.1 Motivation -- 11.2 Identify Freelance Rules in an MC-Net -- 11.3 Improved Weighted Partial MaxSAT Encoding on Refined MC-Nets -- 11.3.1 I-RWPM Encoding Theory -- 11.3.2 Interpretation of I-RWPM -- 11.3.3 Pedagogical Examples -- 11.4 Performance Evaluation -- 11.4.1 Results in a General Case -- 11.4.2 Results with Varied Number of Freelance Rules -- 11.4.3 Results with Few Freelance Rules -- 11.5 Chapter Summary -- References -- Appendix A Complete File for Solving 4-Queens in DIMACS Format -- Appendix B A Sample of Sbox Expressed in ANF -- Appendix -- Appendix -- Appendix E -- Appendix F -- Appendix G -- Appendix H -- Appendix -- Appendix J Appendix K Complete File Generated by MaxSAT for Solving Overloaded Scheduling in WPM Input Format -- Complete File Generated by RWPM for Example 8.9 in WPM Input Format -- Complete File Generated by RWPM for Example 8.11 in WPM Input Format -- Complete File Generated by RWPM for Example 8.12 in WPM Input Format -- Complete File Generated by RWPM for Example 8.13 in WPM Input Format -- Complete File Generated by AWPM for Example 9.2 in WPM Input Format -- Complete File Generated by AWPM for Example 9.3 in WPM Input Format -- Complete File Generated by AWPM for Example 9.4 in WPM Input Format -- Complete File Generated by AWPM for Example 9.5 in WPM Input Format -- Appendix L Proof of Formula in Lemma 10.3 -- Appendix M Calculation of ̄m in Chapter 10 -- Appendix N Appendix O Complete File Generated by RWPM-RT for Example 10.3 in WPM Input Format -- Complete File Generated by RWPM-RT for Example 10.4 in WPM Input Format -- Appendix P Comparative Analysis of RWPM and I-RWPM -- Appendix Q Appendix R Complete File Generated by I-RWPM for Example 11.3 in WPM Input Format -- Complete Files Generated by I-RWPM and RWPM-RT for Example 11.4 in WPM Input Format -- Appendix S Theoretical Analysis on d -- Index.