125,99 €
Mehr erfahren.
- Herausgeber: John Wiley & Sons
- Kategorie: Wissenschaft und neue Technologien
- Sprache: Englisch
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.
Sie lesen das E-Book in den Legimi-Apps auf:
Seitenzahl: 390
Veröffentlichungsjahr: 2024
Ähnliche
Table of Contents
Cover
Table of Contents
Title Page
Copyright
Preface
1 Satisfiability Theories
1.1 Boolean Satisfiability (SAT)
1.2 Maximum Satisfiability (MaxSAT)
1.3 Satisfiability Algorithms
1.4 Chapter Summary
References
Notes
2 Encoding in General
2.1 CNF Encodings
2.2 Satisfiability Problem-Solving Environments
2.3 Case Study
2.4 Chapter Summary
References
Notes
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
Note
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.4 Chapter Summary
References
Note
5 Job-Shop Scheduling
5.1 Job-shop Scheduling Model
5.2 SAT Approach
5.3 Performance Evaluation
5.4 Chapter Summary
References
Note
6 Overloaded Scheduling
6.1 Overloaded Scheduling Model
6.2 Weighted Partial MaxSAT Approach
6.3 Theoretical Discussion
6.4 Performance Evaluation
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.6 Evaluating Heuristics
7.7 Chapter Summary
References
Notes
8 Rule Relation-Based Weighted Partial MaxSAT (RWPM) Encoding
8.1 Problem Statement
8.2 Representative Algorithms
8.3 Encoding Rule Relations into WPM
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.2 Encoding Agent Relations into WPM
9.3 Performance Evaluation
9.4 Chapter Summary
References
Note
10 Comparative Analysis and Improvement of RWPM
10.1 Motivation
10.2 Comparative Study on RWPM and AWPM
10.3 An Interesting Phenomenon: Analysis on a Special Case
10.4 RWPM with Refined Transitive Laws (RWPM-RT)
10.5 Performance Evaluation
10.6 Chapter Summary
References
Notes
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.4 Performance Evaluation
11.5 Chapter Summary
References
Notes
Appendix A: Complete File for Solving 4-Queens in DIMACS Format
Appendix B: A Sample of Sbox Expressed in ANF
Appendix C: Complete File Generated by MaxSAT for Solving Overloaded Scheduling in WPM Input Format
Appendix D: Complete File Generated by RWPM for Example 8.9 in WPM Input Format
Appendix E: Complete File Generated by RWPM for Example 8.11 in WPM Input Format
Appendix F: Complete File Generated by RWPM for Example 8.12 in WPM Input Format
Appendix G: Complete File Generated by RWPM for Example 8.13 in WPM Input Format
Appendix H: Complete File Generated by AWPM for Example 9.2 in WPM Input Format
Appendix I: Complete File Generated by AWPM for Example 9.3 in WPM Input Format
Appendix J: Complete File Generated by AWPM for Example 9.4 in WPM Input Format
Appendix K: 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 in Chapter 10
Note
Appendix N: Complete File Generated by RWPM-RT for Example 10.3 in WPM Input Format
Appendix O: Complete File Generated by RWPM-RT for Example 10.4 in WPM Input Format
Appendix P: Comparative Analysis of RWPM and I-RWPM
Reference
Note
Appendix Q: Complete File Generated by I-RWPM for Example 11.3 in WPM Input Format
Appendix R: Complete Files Generated by I-RWPM and RWPM-RT for Example 11.4 in WPM Input Format
Appendix S: Theoretical Analysis on
Note
Index
End User License Agreement
List of Tables
Chapter 2
Table 2.1 Monotone laws of Boolean algebra.
Table 2.2 Nonmonotone laws of Boolean algebra.
Table 2.3 Constraints of the 4-queens problem.
Table 2.4 Assignment of all Boolean variables in the -queens problem.
Chapter 4
Table 4.1 Average runtime (seconds) of SAT approach and original partial Max...
Table 4.2 Average runtime (seconds) of SAT approach and original partial Max...
Table 4.3 Average runtime (seconds) of original partial MaxSAT approach (OMA...
Chapter 5
Table 5.1 Processing information for each operation.
Table 5.2 Original LB and UB.
Table 5.3 Results of .
Table 5.4 Results of .
Table 5.5 Improvement of LB and UB.
Table 5.6 New LB and UB.
Chapter 6
Table 6.1 Notations and descriptions in scheduling model.
Table 6.2 Critical time points of each fragment in three tasks.
Table 6.3 Encodings related to variables in PM and WPM formulations.
Table 6.4 Experimental design.
Chapter 7
Table 7.1 Research status of problem.
Table 7.2 Critical information of two-restricted preemptive scheduling in Fi...
Table 7.3 The variation trend of factors influencing SAT performance as in...
Table 7.4 The variation trend of factors influencing PMS performance as in...
Table 7.5 The variation trend of factors influencing SAT performance as in...
Table 7.6 The variation trend of factors influencing PMS performance as in...
Chapter 10
Table 10.1 Notations and descriptions used in theoretical comparisons betwee...
Table 10.2 Number of variables and clauses in RWPM and AWPM.
Table 10.3 Average numbers of variables and clauses in AWPM and RWPM given
Chapter 11
Table 11.1 Notations and descriptions used throughout Chapter 11.
Table 11.2 Average runtime (seconds) for solving problems with negligible pe...
16
Table P.1 Notations and descriptions used in theoretical comparison
List of Illustrations
Chapter 2
Figure 2.1 Solutions of the 4-queens problem. (a) Solution 1 and (b) Solutio...
Figure 2.2 Variable representation of the 4-queens problem. (a) Variable not...
Chapter 3
Figure 3.1 Diagram of AES-128 key expansion in adjacent two rounds
Figure 3.2 Decayed AES key schedules under different decay assumptions
Figure 3.3 Average runtime (seconds) of SAT approach with and various numb...
Chapter 4
Figure 4.1 An example of applying the cut-up conversion
Figure 4.2 Bit relations related to , , , and . is the input byte star...
Figure 4.3 An example in which , , , and are all leaf variables
Figure 4.4 Average number of variables and clauses generated by two partial ...
Chapter 5
Figure 5.1 Two feasible schedules in Example 5.1. (a) Feasible schedule 1 an...
Chapter 6
Figure 6.1 Overview of the WPM-based scheduling method
Figure 6.2 A simple scheduling example. (a) Original problem and (b) problem...
Figure 6.3 WPM formulation for exemplified problem
Figure 6.4 Assignment of all Boolean variables in the exemplified problem...
Figure 6.5 Performance comparison of WPM and SMT for weighted cases in scena...
Figure 6.6 Completion percentage of formulations for unweighted cases in sce...
Figure 6.7 Comparison statistics of PM and WPM for unweighted cases in scena...
Figure 6.8 Comparison statistics of PM and WPM for unweighted cases in scena...
Figure 6.9 Comparison statistics of PM and WPM for unweighted cases in scena...
Figure 6.10 Comparison statistics of PM and WPM for unweighted cases in scen...
Figure 6.11 Comparison statistics of PM and WPM for unweighted cases in scen...
Chapter 7
Figure 7.1 Example schedule of no preemption, fully arbitrary preemption and...
Figure 7.2 Mathematical programming of .
Figure 7.3 Optimal makespan under the setting of and
Figure 7.4 Statistics with various preemption granularities . (a) Success r...
Figure 7.5 Statistics with various numbers of machines . (a) Success rate w...
Figure 7.6 Performance evaluation on scalability. (a) Average runtime with v...
Figure 7.7 Performance comparison with MP and SAT with larger processing tim...
Figure 7.8 Numbers of variables and clauses generated by SAT in all experime...
Figure 7.9 Numbers of variables and clauses generated by PMS in all experime...
Figure 7.10 Evaluation of 2RS. (a) Average values of makespan for various va...
Chapter 8
Figure 8.1 Enumeration of agents within all possible coalition structures in...
Figure 8.2 Enumeration of agents within all possible coalition structures in...
Figure 8.3 Graphical representation of Example 8.7 [11].
Figure 8.4 Assignment of all Boolean variables in Example 8.9
Figure 8.5 Assignment of all Boolean variables in Example 8.11
Figure 8.6 Assignment of all Boolean variables in Example 8.12
Figure 8.7 Assignment of all Boolean variables in Example 8.13
Figure 8.8 Average computation time of RWPM and direct encoding [11, 12]. (a...
Chapter 9
Figure 9.1 Assignment of all Boolean variables in Example 9.2 (Source: Xiaoj...
Figure 9.2 Assignment of all Boolean variables in Example 9.3 (Source: Xiaoj...
Figure 9.3 Assignment of all Boolean variables in Example 9.2 (Source: Xiaoj...
Figure 9.4 Assignment of all Boolean variables in Example 9.5 (Source: Xiaoj...
Figure 9.5 Average computation time of RWPM and AWPM (a) Computation time fo...
Figure 9.6 Number of Boolean variables in RWPM and AWPM (a) No. of Boolean v...
Figure 9.7 Number of clauses in RWPM and AWPM (a) No. of clauses for MC-nets...
Chapter 10
Figure 10.1 Average computation times of AWPM and RWPM given , ,
Figure 10.2 Assignment of all Boolean variables in Example 10.3
Figure 10.3 Assignment of all Boolean variables in Example 10.4
Figure 10.4 Average computation times of AWPM, RWPM and RWPM-RT given , ,
Figure 10.5 Number of variables and clauses in AWPM, RWPM and RWPM-RT given
Figure 10.6 Average computation times of AWPM and RWPM-RT given , ,
Figure 10.7 Number of variables and clauses in AWPM and RWPM-RT given , , ...
Chapter 11
Figure 11.1 Graphical representation of examples (a) Example 11.1 and (b) Ex...
Figure 11.2 Graphical representation of Example 11.4 (Source: Xiaojuan Liao ...
Figure 11.3 Average computation time for AWPM, RWPM, RWPM-RT, and I-RWPM (So...
Figure 11.4 Number of variables and clauses in AWPM, RWPM, RWPM-RT, and I-RW...
Figure 11.5 Average computation time with specific number of freelance rules...
Figure 11.6 Average computation time given with varied percentage of freel...
16
Figure P.1 Values of parameters that affect (a) Average values of , , ,...
Figure P.2 Trend of with growing
Guide
Cover
Table of Contents
Title Page
Copyright
Preface
Begin Reading
Appendix A Complete File for Solving 4-Queens in DIMACS Format
Appendix B A Sample of Sbox Expressed in ANF
Appendix C Complete File Generated by MaxSAT for Solving Overloaded Scheduling in WPM Input Format
Appendix D Complete File Generated by RWPM for Example 8.9 in WPM Input Format
Appendix E Complete File Generated by RWPM for Example 8.11 in WPM Input Format
Appendix F Complete File Generated by RWPM for Example 8.12 in WPM Input Format
Appendix G Complete File Generated by RWPM for Example 8.13 in WPM Input Format
Appendix H Complete File Generated by AWPM for Example 9.2 in WPM Input Format
Appendix I Complete File Generated by AWPM for Example 9.3 in WPM Input Format
Appendix J Complete File Generated by AWPM for Example 9.4 in WPM Input Format
Appendix K 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 in Chapter 10
Appendix N Complete File Generated by RWPM-RT for Example 10.3 in WPM Input Format
Appendix O 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 Complete File Generated by I-RWPM for Example 11.3 in WPM Input Format
Appendix R Complete Files Generated by I-RWPM and RWPM-RT for Example 11.4 in WPM Input Format
Appendix S Theoretical Analysis on
Index
END USER LICENSE AGREEMENT
Pages
iii
iv
ix
x
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
209
210
211
212
213
215
216
217
218
219
220
221
222
223
224
225
226
227
229
230
231
232
233
234
235
236
237
238
239
241
243
244
245
246
247
248
249
251
253
254
255
256
257
258
259
260
261
262
263
Applied Satisfiability
Cryptography, Scheduling, and Coalitional Games
Xiaojuan Liao
Chengdu University of Technology, Chengdu
China
Miyuki Koshimura
Kyushu University, Fukuoka
Japan
Copyright © 2025 by John Wiley & Sons, Inc. All rights reserved, including rights for text and data mining and training of artificial technologies or similar technologies.
Published by John Wiley & Sons, Inc., Hoboken, New Jersey.Published simultaneously in Canada.
No part of this publication may be reproduced, stored in a retrieval system, or transmitted in any form or by any means, electronic, mechanical, photocopying, recording, scanning, or otherwise, except as permitted under Section 107 or 108 of the 1976 United States Copyright Act, without either the prior written permission of the Publisher, or authorization through payment of the appropriate per-copy fee to the Copyright Clearance Center, Inc., 222 Rosewood Drive, Danvers, MA 01923, (978) 750-8400, fax (978) 750-4470, or on the web at www.copyright.com. Requests to the Publisher for permission should be addressed to the Permissions Department, John Wiley & Sons, Inc., 111 River Street, Hoboken, NJ 07030, (201) 748-6011, fax (201) 748-6008, or online at http://www.wiley.com/go/permission.
Trademarks: Wiley and the Wiley logo are trademarks or registered trademarks of John Wiley & Sons, Inc. and/or its affiliates in the United States and other countries and may not be used without written permission. All other trademarks are the property of their respective owners. John Wiley & Sons, Inc. is not associated with any product or vendor mentioned in this book.
Limit of Liability/Disclaimer of Warranty: While the publisher and author have used their best efforts in preparing this book, they make no representations or warranties with respect to the accuracy or completeness of the contents of this book and specifically disclaim any implied warranties of merchantability or fitness for a particular purpose. No warranty may be created or extended by sales representatives or written sales materials. The advice and strategies contained herein may not be suitable for your situation. You should consult with a professional where appropriate. Further, readers should be aware that websites listed in this work may have changed or disappeared between when this work was written and when it is read. Neither the publisher nor authors shall be liable for any loss of profit or any other commercial damages, including but not limited to special, incidental, consequential, or other damages.
For general information on our other products and services or for technical support, please contact our Customer Care Department within the United States at (800) 762-2974, outside the United States at (317) 572-3993 or fax (317) 572-4002.
Wiley also publishes its books in a variety of electronic formats. Some content that appears in print may not be available in electronic formats. For more information about Wiley products, visit our web site at www.wiley.com.
Library of Congress Cataloging-in-Publication Data applied for:
Hardback ISBN: 9781394249787
Cover Design: WileyCover Image: © Luvricon/Shutterstock
Preface
Many real-world problems are difficult to solve partially because they present computational challenges. Moreover, it is often important to find not just any solution to the problem, but the optimal one from all feasible solutions according to some objective. In such cases, the problem falls into the class of optimization problems. If an optimization problem is represented as discrete variables, it is known as a combinatorial optimization problem. Boolean satisfiability (SAT) and maximum satisfiability (MaxSAT), as advanced tools for solving combinatorial optimization problems, have been applied to a wide range of practical combinatorial optimization problems.
Historically, there have been a variety of SAT and MaxSAT applications, including bounded model checking, planning, software verification, combinatorial designs, and more. This book extends the application scope of satisfiability theories, demonstrating that high-performance satisfiability-based solvers have great advantages in handling a wider range of problems, provided that these problems are appropriately encoded as propositional formulae. Fundamental questions such as “What new fields can satisfiability theories be applied to?” and “How can advanced satisfiability techniques be effectively utilized to solve practical problems?” are explored.
The application fields introduced in this book primarily encompass encryption key recovery in side-channel attacks, scheduling in single- and parallel-machine environments, and coalition structure generation in coalitional games. These complex problems, challenging to tackle with conventional methods, demonstrate increased efficiency when encoded into Boolean propositional formulae in a proper way. Further details on these applications are presented below.
Satisfiability applied to cryptography: The advanced encryption standard (AES) is a specification for the encryption of electronic data established by the U.S. National Institute of Standards and Technology (NIST) in 2001, and it currently serves as a globally prevalent symmetric cryptographic algorithm. As a kind of block ciphers, AES is vulnerable to a side-channel attack known as a cold boot attack, where the attacker can extract the encryption key from memory. This book exploits the capabilities of SAT and MaxSAT solvers to reconstruct corrupted AES keys extracted from a cold boot attack. This approach is well suited for real attack scenarios where decaying and reverse flipping errors coexist.
Satisfiability applied to scheduling: Scheduling, a recurring decision-making process in various manufacturing and service industries, involves the allocation of resources to tasks over specified time periods. Its primary objective is to optimize one or more goals, such as makespan and total tardiness. This book demonstrates that by formalizing a scheduling problem as a set of Boolean formulae, the problem can be efficiently tackled using the available SAT or MaxSAT solvers in an out-of-the-box manner without further knowledge in scheduling or coding experience from the user. The addressed scheduling problems include job-shop scheduling, overloaded scheduling, and restricted preemptive scheduling. By leveraging satisfiability solving techniques, promising results can be achieved.
Satisfiability applied to coalitional games: Coalition structure generation (CSG) stands as a central research challenge in the coalition formation of multi-agent systems. It involves partitioning a set of agents into exhaustive and disjoint coalitions, where each coalition is assigned a positive or negative payoff. This partition is termed a coalition structure. The objective in solving the CSG problem is to find a coalition structure such that the total value of all the coalitions is maximized. This book shows that by encoding constraints of the CSG problem into Boolean propositional logic and employing an off-the-shelf MaxSAT solver to identify the optimal solution, the solvable problem can be significantly scaled up. In addition to various encoding strategies applied to the CSG problem, this book provides both theoretical and experimental comparisons to explore the underlying reason for performance variation. Building on these insights, a more compact encoding is constructed to further enhance the solving efficiency.
We anticipate that the solving efficiency of the provided encoding methods will see further improvement in the coming years, given the rapid development of novel technologies emerging in SAT and MaxSAT communities. Additionally, this book aims to enlighten researchers and practitioners seeking effective ways to address practical optimization problems. It offers a broader perspective, showing that satisfiability theories can be a competitive alternative for tackling optimization problems. Furthermore, researchers dedicated to the application areas covered in this book may find occasional utility in its insights.
December, 2024
Xiaojuan Liao
Chengdu, China
Miyuki Koshimura
Fukuoka, Japan
1Satisfiability Theories
After reading this chapter, you should be able to:
Comprehend fundamental concepts of Boolean satisfiability (SAT), maximum satisfiability (MaxSAT), and MaxSAT extensions.
Understand mainstream algorithms for solving SAT and MaxSAT problems.
1.1 Boolean Satisfiability (SAT)
A Boolean formula is a string that represents a Boolean function. A Boolean function is a function of the form: , where is a Boolean domain and is the arity of the function. Usually, and are represented by 1 and 0, respectively. A propositional Boolean formula is a Boolean formula that only contains logic operations and, or and not (sometimes called negation or complement), symbolized as , , and , respectively. Some examples of propositional Boolean formulas are listed as follows:
A propositional Boolean formula can be expressed in conjunctive normal form (CNF), also known as product of sum (POS) form. A formula in CNF consists of a conjunction (logic and) of one or more clauses. A clause is a disjunction (logic or) of one or more literals, and a literal is an occurrence of a Boolean variable or its negation. An example of a propositional Boolean formula in CNF is , which can also be represented by a set of clauses as , or an assemble of literal sets like . Usually, a CNF formula is denoted by a set of clauses, i.e., conjunction is omitted.
The problem of determining whether there exists a variable assignment that makes a propositional Boolean formula evaluate to true is called a Boolean satisfiability (SAT) problem. In other words, the SAT problem tries to find a variable assignment to a CNF formula that satisfies all the clauses in a Boolean propositional formula. If such an assignment exists, the formula is satisfiable; otherwise, the formula is unsatisfiable.
Example 1.1 is a Boolean propositional formula in CNF. This formula contains five clauses: , , , , and . The first clause contains four literals, i.e., , , , and . This formula is unsatisfiable because the last two clauses are conflicting, which means they cannot be satisfied at the same time.
SAT problem is the first known nondeterministic polynomial time (NP)-complete problem proven by Cook [1]. The proof shows how every decision problem in the complexity class NP can be reduced to the SAT problem for CNF formulas. That the SAT problem is NP-complete problem briefly means that there is no known algorithm that efficiently solves all instances of SAT, and it is generally believed that no such algorithm can exist. A class of algorithms to efficiently solve a large enough subset of SAT instances is called SAT solver. Extending the capabilities of SAT solving algorithms is an ongoing area of progress. However, no current such methods can efficiently solve all SAT instances.
In the last century, showing that a certain problem is as hard as SAT was the end of the story and trying to solve it directly seemed to be hopeless. With the significant progress made in SAT solving, it is now widely accepted that being able to encode a problem into SAT is highly likely to lead to a practical solution. This “SAT Revolution” started at the end of the last century and continues to produce amazing new practical and theoretical results [2].
Examples of SAT applications include software verification [3, 4], bounded model checking [5, 6], artificial intelligence (AI) planning [7, 8], cryptographic attacks [9–13], scheduling [14–17], etc. These applications rely on the ability of SAT solvers to determine whether there exists an assignment that makes a given Boolean formula evaluate to true and return one satisfying assignment if the formula is satisfiable. It is noticeable that there are applications that require enumerating all the satisfying assignments. For example, in frequent itemset mining, it is necessary to generate all sets of items with high support from a given transaction database [18]. This opens up a new variant of SAT, called all solutions SAT (AllSAT). Solving an AllSAT problem aims to enumerate all satisfying assignments if a given CNF formula is satisfiable. Readers may refer to [19] for major techniques of ALLSAT solvers.
1.2 Maximum Satisfiability (MaxSAT)
Given a Boolean propositional formula, if it is unsatisfiable, SAT solvers only report that no solution exists, without any information on unsatisfiable instances. However, assignments violating a minimum number of constraints, or satisfying all the compulsory (hard) constraints and as many optional (soft) constraints as possible, can be considered as acceptable solutions in real-life scenarios. To cope with this limitation of SAT, maximum satisfiability (MaxSAT) and its extensions, such as partial MaxSAT and weighted MaxSAT, are becoming an alternative for representing and efficiently solving over-constrained problems [2].
The MaxSAT problem for a CNF formula is the problem of finding a variable assignment that maximizes the number of satisfied clauses. MaxSAT is often used to mean MinUNSAT because finding an assignment that maximizes the number of satisfied clauses is equivalent to finding an assignment that minimizes the number of unsatisfied clauses. MaxSAT is useful to measure the extent of unsatisfiability of a CNF formula.
Three extensions of MaxSAT are more well suited for representing and solving over-constrained problems: partial MaxSAT, weighted MaxSAT, and weighted partial MaxSAT (WPM).
In a partial MaxSAT instance, each clause is labeled either hard or soft. The hard clauses must be obligatorily satisfied, while the soft clauses can be unsatisfied. The goal of solving the partial MaxSAT instance is to satisfy all hard clauses and the maximal number of soft clause. The partial MaxSAT problem is easily extended to a SAT problem if all the clauses are hard, and a MaxSAT problem if all the clauses are soft.
Example 1.2 Given a partial MaxSAT instance , the first and second clause, enclosed by “,” are hard clauses, and the third clause, enclosed by “,” is a soft clause. To satisfy the hard clauses, and are forced to be 1 and 0, respectively. Based on the assignment of and , the true assignment of has to be 1 so that the soft clause can be satisfied.
A weighted MaxSAT instance is expressed in weighted CNF, where each clause is assigned a positive integer. The problem is to find a truth assignment that maximizes the sum of weights of satisfied clauses. In a special case, if the weights of all the clauses in weighted MaxSAT are equal to one, the problem is regarded as a MaxSAT problem.
Example 1.3 A weighted MaxSAT instance has three weighed clauses holding weights 2, 3, 4, respectively. All of the three clauses can be satisfied by assigning 1, 0, 1 to , , , respectively, which leads to the maximal sum of weights of satisfied clauses.
The WPM is the combination of partial MaxSAT and WPM. A WPM instance distinguishes hard and soft clauses, where each soft clause is assigned a positive integer. Solving the WPM instance is to satisfy all hard clauses and maximize the sum of weights of satisfied soft clauses. The definition of WPM can be easily extended to partial MaxSAT, where all soft clauses have weight 1, and weighted MaxSAT, where no clauses are hard.
Example 1.4 Given a WPM instance , the first and second clause, enclosed by “,” are hard clauses, while the third and fourth clauses, enclosed by “,” are soft clauses. To satisfy the hard clauses, and are forced to be 1 and 0, respectively. Based on the assignment of and , the true assignment of is preferred to be 0 so that the weight 7 can be earned, which is larger than the other case that the gain is merely 2.
Many important problems can be naturally expressed as MaxSAT, including academic problems such as Max-Cut or Max-Clique, as well as problems from many industrial domains. Concrete examples include the following domains: routing problems [20], hardware debugging [21–23], software debugging [24, 25], scheduling [17,26–28], planning [29–32], coalitional games [33–37], etc. Additionally, many problems originally formulated in other optimization frameworks can be easily reformulated as MaxSAT, such as the Pseudo-Boolean Optimization framework [38], the Weighted Constraint Satisfaction Problem (WCSP) framework [39], and the MaxSMT framework [40]. Readers may refer [41] for more traditional applications of MaxSAT.
1.3 Satisfiability Algorithms
The last two decades have witnessed significant progress in the development of theoretical, logical and algorithmic aspects of SAT and MaxSAT solving techniques. Moreover, the SAT competition1 (starting from 2002), MaxSAT evaluation2 (starting from 2006), and the international conference on theory and applications of satisfiability testing3 (first held in 1996) jointly play as a driving force for motivating the development of novel SAT and MaxSAT technologies.
1.3.1 SAT Algorithms
Algorithms for solving the SAT problem are mainly based on incomplete algorithms and complete algorithms. Incomplete algorithms (e.g., GSAT [42], WalkSAT [43]) can get a satisfying assignment quickly, but do not prove unsatisfiability if the formula is unsatisfiable. By contrast, complete algorithms (e.g., DPLL algorithm and its variants Chaff [44] and Generic seaRch Algorithm for the Satisfiability Problem, GRASP [45]) guarantee to find satisfying assignment or prove unsatisfiability.
Incomplete algorithms are usually based on stochastic local search, which iteratively improve an assignment of the variables until all constraints are satisfied. Stochastic local search algorithms run efficiently especially on large-scale instances. The primary challenge is the cycling problem where a candidate solution may be revisited [46]. Random walk, restarting strategies, and the configuration check [46] are usually used to tackle this problem. For an in-depth understanding of most recent incomplete algorithms, we recommend readers to consult a comprehensive survey on intelligent optimization algorithms [47].
Complete algorithms are based on the modern improvements or variants of the DPLL approach. DPLL [48, 49], named after the four collective authors, i.e., Davis, Putnam, Logemann, and Loveland, is a complete, backtracking-based algorithmic framework that is the basis of many of the most successful modern complete SAT solvers.
The backtracking algorithm takes a CNF formula as input. Its objective is to determine whether is satisfiable, and if so to find a satisfying assignment. The algorithm maintains a truth assignment and runs recursively. Initially, the assignment is empty with all variables unassigned. At each recursive step, the algorithm selects a literal and explores two potential assignments: true and false. This is done by making recursive calls to investigate both assignments to . The algorithm continues this process until it either finds a satisfying assignment or it exhaustively search through the entire space and concludes that is unsatisfiable [50].
In the worst case, the backtracking algorithm has to explore the entire search space by setting each literal first true and then false. To enhance the search efficiency, based on the backtracking algorithm, DPLL is enhanced by unit propagation and pure-literal elimination rules.
If a clause contains only a single unassigned literal, it is called a unit clause. Given a CNF formula, the unit-clause rule checks if the formula contains a unit clause. If so, it removes all clauses that contain the literal from the formula and removes the negation of the literal from the other clauses. Unit propagation is the iterated application of the unit-clause rule, which repeatedly applies the unit-clause rule until either it derives an empty clause or there are no more unit clauses left.
Example 1.5 Consider the following propositional formula in CNF:
In this formula, is a unit clause and must be assigned true, then it can be removed from the formula. The first clause contains , thus this clause is always satisfied and can be removed from the formula safely.
Consider the second clause , which contains . Now that we have known that is false, we can remove from the clause since it has nothing to do with the truth value of the clause.
After unit propagation, the formula can be simplified as
Here, we find the simplified formula contains a new unit clause . Continue with the unit propagation. We can remove from the formula and remove from the clause . Thereby, the formula is simplified as
Apparently, is a unit clause and can be removed from the formula. Eventually, the formula becomes empty, and the original formula is satisfiable.
If a literal appears in some clause but its negation does not appear in the formula, it is called a pure literal. Pure-literal elimination removes all clauses containing a pure literal because these clauses can be always satisfied by making the pure literal true without falsifying any other clauses.
Example 1.6 Consider the following propositional formula in CNF:
In the formula, and are pure literals. We can always satisfy the clauses , , and by assigning to true and to false. After the pure-literal elimination, the formula can be simplified as
This simplified formula contains pure literals and . Therefore, we can remove this clause from the formula. Eventually, the formula is empty, and the original formula is satisfiable.
The DPLL procedure is described in Algorithm 1.1. Functions and take a CNF formula as input and return the simplified formula of applying unit propagation and pure-literal elimination, respectively. By picking an unassigned variable from , which is accomplished by , and assigning truth values to it, the resulting formula is simplified iteratively. This process continues until is empty or contains an empty clause, indicating that is satisfiable or unsatisfiable, respectively.
The DPLL algorithm has two primary limitations. First, upon encountering a conflict, where a variable assignment renders a clause unsatisfiable, the algorithm identifies only the present variable assignment as the source of the conflict, lacking the ability to deduce specific combinations of variable assignments that may also trigger the conflict. Second, when a conflict occurs, the algorithm employs the chronological backtracking approach, jumping back to the most recent variable assignment that led to the conflict and assigning the opposite truth value to that variable. This strategy may result in a considerable amount of time, as it wastes time exploring variable assignments in a search space that is guaranteed to lead to conflicts.
Conflict-driven clause learning (CDCL) [44, 45], improved from the DPLL algorithm, incorporates conflict analysis and clause learning techniques to avoid repeatedly exploring the same impossible assignments to literals, thus pruning the search space effectively and expediting the solving process. Main improvements of the CDCL are clause learning from conflicts and nonchronological backtracking, which are summarized as follows:
Clause learning from conflicts: When detecting a conflict, i.e., a clause becomes unsatisfiable, CDCL analyzes the conflict to identify the cause and adds a learnt clause (the negation of the assignments that led to the conflict) to the original formula. This learnt clause is essential for avoiding the same conflict in the future, as it blocks the problematic assignment.
Nonchronological backtracking: If a conflict arises, CDCL jumps back to the appropriate decision level where the first-assigned variable involved in the conflict and assigns the opposite truth value to it. The backtracking level may not necessarily be the level where the most recently assigned variable locates. This allows the algorithm to flexibly select the decision level for backtracking and intelligently avoid conflict repetition by skipping over potentially unnecessary variable assignments.
Given the ability to discover early that branches of the search space does not have to be explored, the CDCL algorithm is extremely efficient for solving large-scale SAT problems. Currently, the CDCL algorithm stands out as one of the most efficient methods for solving SAT problems, laying the foundation of many modern SAT solvers (e.g., MiniSAT [51], Glucose [52], MergeSat [53], and IsaSAT [54]). For more details on the CDCL procedure, we recommend readers to refer to [50]. For a comprehensive study and analysis of the latest developments and new approaches of SAT solvers, we suggest referring to [55].
1.3.2 MaxSAT Algorithms
Generally speaking, there are two approaches for MaxSAT solving techniques: heuristic and approximation algorithms that find near-optimal solutions and exact algorithms that compute optimal solutions.
Heuristic local search algorithms are the foundation of early practical works to find near-optimal solutions. Whereas many exact MaxSAT solvers use local search algorithms to rapidly compute an initial assignment of variables, these algorithms do not guarantee the quality of their output solutions. By contrast, approximation algorithms output solutions not as fast as heuristic algorithms, but they provide a guarantee about the quality of their solutions. The approximation of a MaxSAT solution is usually measured by a factor that is bounded by a constant or a slowly growing function of the input size. Given a constant , an algorithm is -approximation for a maximization problem if it provides a feasible solution in polynomial time, which is at least times the optimum, considering all the possible instances of the problem [56]. A number of improvements have been achieved on the performance guarantee, from 1/2, proposed in 1974 [57], to 0.7584, proposed in 1995 [58]. Later on, a limit on approximability was proved by Håstad [59] that unless NP=P, no approximation algorithm for MaxSAT can achieve a performance guarantee better than 7/8. This theory was proved again in [60], showing that the constant 7/8 is tight. From a theoretical and practical point of view, semidefinite programming has been shown quite promising for approximating MaxSAT solutions. Readers may refer to [61] to learn more about how to approximate MaxSAT with semidefinite programming.
Exact algorithms can be classified into two approaches. The one follows a branch and bound (BB) algorithm and applies several techniques tailored to MaxSAT. Another one makes use of a state-of-the-art SAT solver as an inference engine, referred to as a SAT-based approach.
Many contemporary exact MaxSAT solvers follow a BB algorithm [62–69], which ensures the minimal number of unsatisfied clauses in a MaxSAT problem. Given a MaxSAT instance , BB explores a search tree that represents the space of all possible assignments for in a depth-first manner. At every node, BB compares the upper bound () with the lower bound (). is the best solution (i.e., the minimum number of falsified clauses) found so far for a complete assignment, and is the sum of the number of clauses which are falsified by the current partial assignment plus an underestimation of the number of clauses that will become unsatisfied if the current partial assignment is completed. If , the algorithm prunes the subtree below the current node and backtracks chronologically to a higher level in the search tree. If , the algorithm tries to find a better solution by extending the current partial assignment by assigning one more variable. The value of after the search of entire tree is the optimal number of unsatisfied clauses in .
BB algorithms usually perform effective in solving small-scale MaxSAT problem instances with a few hundred variables. However, they are ineffective on instances with more than a thousand variables [70]. Currently, the most important algorithms for solving MaxSAT problems are based on iterative calls to a SAT solver, commonly known as the SAT-based approaches. These approaches can be further classified into three types: the model-improving, the core-guided, and the implicit hitting set approaches.
Model-improving approaches (e.g., SAT4j [71], QMaxSAT [72], Pacose [73], and MergeSat [74]) are based on querying a SAT solver for solutions of increasing quality. Given a MaxSAT instance with a collection of soft clauses , a new variable is added to each soft clause , where is called a blocking variable. Solving the MaxSAT problem for is to minimize the number of blocking variables that evaluate to true, called true blocking variables, in with soft clauses . The minimal satisfied assignment is searched by iterative calls to a SAT solver, which are summarized as follows [72]. First run the SAT solver on without any constraints to get an initial model and count the number of true blocking variables in the model, then add a constraint to limit the number of true blocking variables to a smaller (called a cardinality constraint), and run the solver again. If the problem is unsatisfied, is the optimal solution. Otherwise, the process is repeated with the constraint that limits the number of true blocking variables to a smaller integer. This process terminates when the problem becomes unsatisfied.
Model-improving solvers start by adding a blocking variables to each soft clause and then iteratively call a SAT solver by decreasing the number of true blocking variables until the formula becomes unsatisfiable. When a MaxSAT problem has a significantly large number of soft clauses, solving this problem becomes infeasible due to the resulting extensive encodings.
In contrast to model improving approaches, core-guided approaches (e.g., Fu–Malik algorithm [75], WPM1 [76], WMSU1 [77], OLL [78], and Maxino [79]) are unsatisfiability based, working from unsatisfiable (UNSAT) to SAT. Given a MaxSAT instance , the following process is iterated until is satisfiable: First run a SAT solver on . If is unsatisfiable, extract an unsatisfiable subset from and introduce new blocking variables . The unsatisfiable subset of clauses is called a core. Then, replace with and add a constraint to build a new formula . The process is called relaxation. If becomes satisfiable, the iteration terminates. The number of iterations indicates the number of falsified clauses in the original .
Core-based algorithms have proved to be effective on industrial problems, typically suitable for solving instances that have optimal solutions falsifying very few soft clauses (relative to the total number of soft clauses). A drawback of core-based algorithms is that the relaxation requires adding new cardinality constraints to the formula at each step, which makes the problem harder to solve at each iteration. Narodytska and Bacchus [80] proposed an alternative approach for solving WPM problems, which also builds a sequence of new SAT formulas, but avoids using cardinality constraints. The new core-guided solver outperforms the contemporary solvers by a large margin in the total number of industrial problem instances.
Similar to the purely SAT-based core-guided approaches, implicit hitting set solvers (e.g., [81–84]) extract cores in an iterative fashion. Given a set of cores, a hitting set is a set of soft clauses that includes at least one soft clause from each core. A hitting set is optimal (of minimum cost) if and only if the sum of the weights of the soft clauses in it is smallest among all hitting sets of the set of cores. In contrast to core-based algorithms that transform the input instance using core compilation steps, the input MaxSAT instance of implicit hitting set solvers is not altered during search. Each SAT solver call is made on the original hard clauses together with a subset of the original soft clauses. Thus, the MaxSAT instance does not get larger in size as the search progresses. As a result, the cores found during search remain relatively small compared to the core-guided approaches [70].
Although SAT and MaxSAT problems have a long history, the solving techniques have evolved and improved over the years. Many advanced techniques have been introduced to aid in problem solving, such as parallel computing [74,85–88], reinforcement learning [88, 89], machine learning [90–92], and quantum computing [93–95]. These new techniques, in turn, encourage SAT and MaxSAT applications in more real-world scenarios.
1.4 Chapter Summary
This section introduced the fundamental formal concepts of SAT, MaxSAT, partial MaxSAT, weighted MaxSAT, and WPM. Mainstream algorithms for solving SAT and MaxSAT were summarized.
From a practical view, many existing applications treat SAT and MaxSAT solvers as black boxes. In other words, once a real-world problem is translated into a CNF formula, the problem can be solved by utilizing an off-the-shelf solver without any interactions between the solver and the application. However, understanding the satisfiability algorithms is beneficial for selecting appropriate solvers, analyzing performance, and further optimizing the efficiency of solving specific problems.
References
1
S. A. Cook. The complexity of theorem-proving procedures. In
Proceedings of the Annual ACM Symposium on Theory of Computing
, pages 151–158, 1971.
2
A. Biere, M. Heule, H. van Maaren, and T. Walsh.
Handbook of Satisfiability
- Second Edition, IOS Press, 2021.
3
E. M. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In
Proceedings of Tools and Algorithms for the Construction and Analysis of Systems
, pages 168–176, 2004.
4
D. Jackson, I. Schechter, and I. Shlyakhter. Alcoa: the alloy constraint analyzer. In
Proceedings of International Conference on Software Engineering
, pages 730–733, 2000.
5
A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In
Proceedings of Tools and Algorithms for the Construction and Analysis of Systems
, pages 193–207, 1999.
6
M. Sheeran, S. Singh, and G. Stalmarck. Checking safety properties using induction and a SAT solver. In
Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design
, pages 108–125, 2000.
7
J. Rintanen, K. Heljanko, and I. Niemelä. Planning as satisfiability: Parallel plans and algorithms for plan search.
Artificial Intelligence
, 170(12-13):1031–1080, 2006.
8
B. Selman and H. Kautz. Planning as satisfiability. In
Proceedings of European Conference on Artificial Intelligence
, pages 359–363, 1992.
9
A. A. Kamal. Applications of SAT solvers to AES key recovery from decayed key schedule images. In
