Introduction
The goal of AI is to perform intelligent tasks as humans do, which requires the derivation of new information from given information. Inference is essential to derive such information. There are two major areas in this function of inference.
One is inference that derives new information based on given premises and rules, which uses inference engines that use logic and knowledge, as described in “Rule-Based, Knowledge-Based, Expert Systems, and Relational Data“. The inference engine searches for and derives new information from the information it holds based on the given premises and rules. Such inference engines are used in expert systems, diagnostic systems, and other applications.
There are also various inference methods (procedures) for such inference. As described in “Scientific Thinking (2) Reasoning Patterns for Hypothesis Testing” there are various patterns such as deduction, induction, projection, analogy, and abduction.
Another type of inference is machine learning, as described in “Machine Learning Technology” which makes predictions on new data by learning patterns from a large amount of data.
In addition, as described in “Fusion of Logic, Rules, and Probability/Machine Learning” there are inference technologies that combine these two.
In this article, we will discuss some of these inference techniques related to SAT (Boolean SAtisfiability), which is used in logic-based inference to derive new information based on given premises and rules.
About SAT (Boolean SAtisfiability; Satisfiability Determination Problem)
A propositional logic satisfiability problem (SAT: Boolean Satisfiability) is a problem to determine whether or not there exists an assignment of variables such that a given propositional logic formula is true. For example, if there is a problem “whether there exists an assignment of A, B, C, D, E, or F such that A and (B or C) and (D or E or F) are true,” this problem is converted into a propositional logic formula and whether the formula is satisfiable is determined.
Such problem setting plays an important role in many application fields, for example, circuit design, program analysis, problems in the field of artificial intelligence, and cryptography theory. From a theoretical aspect, it is known that the algorithm that can solve the SAT problem is an “NP-complete problem” and no efficient solution method has been found for large-scale problems with current computers. Therefore, this is a field of technology where research is still being conducted to improve algorithm efficiency, such as increasing speed and developing heuristic search algorithms.
Here, “NP-complete problems” are often referred to as “NP problems,” where NP stands for non-deterministic polynomial time and refers to a class of problems in which it is possible to verify whether a given candidate solution is correct or not in polynomial time. This is a problem in which “given a solution, it is easy to verify that it satisfies the constraints of the problem, but it is difficult to find the solution,” or in more prosaic terms, “the problem is easy to compute but difficult to find a solution.
One of the most famous mathematical conjectures of the 21st century is the “P≠NP Conjecture” which is an unproven mathematical proof of the NP problem. This is the prediction that P (polynomial-time: the set of problems whose solutions can be calculated in polynomial time) and NP (nondeterministic polynomial-time: the set of problems whose solutions can be calculated in polynomial time) are not equal, and if P=NP, then all NP problems that could not be solved before If P=NP, all NP problems that could not be solved before can be solved in polynomial time, which is a prediction that is not so convenient. Incidentally, if P=NP, major modern ciphers using the difficulty of prime factorization would be broken.
Reference books on the P≠NP conjecture include “P≠NP” Problem: A Very Difficult Problem in Modern Mathematics” and “The P≠NP Prediction You Will Understand Next Time” as introductory books.
SAT solver
Returning to the SAT solver, as mentioned above, a SAT solver is a program that takes a propositional logic formula as input and determines its satisfiability, and operates based on an algorithm developed to efficiently determine whether a propositional logic formula is satisfiable.
The SAT solver is one of the most commonly used tools in the fields of automatic design of semiconductor chips and software engineering. For example, as described in “Computational Elements of Computers and Semiconductor Chips” a semiconductor chip is realized by a combination of logic elements using transistors that switch on and off to achieve a desired result. used for hardware verification to check whether the circuit works as expected, and thus it is one that can determine the sufficiency of a logic circuit.
SAT solvers are also used in the aspect of software verification. Specifically, program specifications can be expressed in the form of Boolean logic expressions or constraint satisfaction problems (CSP), and the SAT solver can be used to check whether the program satisfies these specifications, or whether the code generated by the compiler produces the correct output for a particular input, or whether the universal conditions of the code hold, software verification using SAT is known to be very accurate.
One such is alloy, a SAT-based program specification checker that describes a model representing the functionality, behavior, and interface of an application as a logical specification, which is then automatically verified.
SAT solver algorithms can be divided into two main categories. One is the complete search algorithm and the other is the non-complete search algorithm.
- Complete Search Algorithm: A complete search algorithm searches for all assignments of a propositional logic formula to check for satisfiability. The main algorithm is the Davis-Putnam-Logemann-Loveland (DPLL) algorithm, which recursively searches the search space and checks for satisfiability using single literal rules, single clause rules, and splitting rules.
- Non-Complete Search Algorithm: The non-complete search algorithm is more efficient than the complete search algorithm. Major algorithms include the WalkSAT, GSAT, and CDCL (Conflict-Driven Clause Learning) algorithms. The CDCL algorithm is an evolution of the DPLL algorithm and is widely used as a faster and more efficient SAT solver.
- Other Algorithms: SAT solvers are also accelerated using modern technologies such as parallel computing. Recently, SAT solvers using GPUs and SAT solvers using quantum computers have been studied.
Many SAT solvers using such algorithms exist and are being evaluated in the SAT Competition.” The latest trends and techniques of SAT solvers” summarizes information on these SAT solvers, although it is a little old information. This section describes some representative SAT solvers.
- MiniSat: one of the most popular SAT solvers in use today, fast and highly efficient.
- Glucose: A SAT solver derived from MiniSat that is considered to be faster than MiniSat.
- Lingeling: A SAT solver that has shown high performance in SAT contests and is capable of handling large problems.
- CaDiCaL: A SAT solver that supports parallel processing and has fast computing performance.
- PicoSAT: A small and simple SAT solver that is available for a variety of platforms.
Other SAT solvers include zChaff、WalkSAT、GRASP、CryptoMiniSat、MapleSAT、Scavel
Applications of the SAT solver in combination with artificial intelligence techniques
In addition to automated software and hardware verification, the SAT solver can be combined with machine learning and artificial intelligence techniques to provide fast and accurate solutions to complex problems. Typical applications are described below.
- Enhancing Computer Security
SAT solvers are used in the security field to crack passwords, break encryption, etc. By combining machine learning techniques, SAT solvers can handle sophisticated attacks that are difficult to solve using existing methods. Specifically, in order to check how a security policy works, the SAT solver can be used to determine the satisfiability of logical expressions, and the SAT solver can be used to attempt to break encryption.
- Application to the Machine Learning Field
The SAT solver can also be used in the field of artificial intelligence. For example, in machine learning, in the case of parameter optimization for training a model, the SAT solver can be used to efficiently perform parameter optimization problems.
- Solving Combinatorial Optimization Problems
SAT solvers are also used for combinatorial optimization problems. These include logistics optimization and scheduling problems. In addition, machine learning techniques can be combined to achieve faster and more accurate solutions.
- Faster Natural Language Processing
SAT solvers are also used to accelerate natural language processing. This includes, for example, document retrieval and document classification. By combining machine learning techniques, fast and accurate search and classification can be achieved.
AI development for board games such as chess
SAT solvers can also be used to develop AI for board games. For example, the state of the board in games such as chess and Go can be converted into propositional logic formulas, and the SAT solver can search for optimal moves. Furthermore, by combining these with machine learning techniques such as reinforcement learning, more advanced play is expected to be realized.
SAT Reference Books
The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability, by Donald E. Knuth, also mentioned in “Tex/Latex, the world standard tool for writing papers, and Mathjax, the web math display tool.”
The preface to this book is as follows. “This booklet is Fascicle 6 of Volume 4 of Techniques of Computer Programming: Combinatorial Algorithms.” As I explained in the preface to Volume 1, I am distributing the material in this preliminary form because I know that it will take many years to complete Volume 4. This lengthy text contains Section 7.2.2.2 of a long, long chapter on combinatorial algorithms. Chapter 7 will eventually fill at least four volumes (i.e., volumes 4A, 4B, 4C, and 4D). Volume 4A begins with a short review of graph theory and a lengthy discussion of “0s and 1s” (Section 7.1), and the volume concludes with Section 7.2, “Generating Basic Combinatorial Patterns,” the first part of Section 7.2, “Generating All Possibilities.” In Volume 4B, we plan to resume talking about backtracking in general in Section 7.2.2 and describe a family of “dancing link” techniques for updating data structures during backtracking in Section 7.2.2.1. Section 7.2.2.1 will then describe a family of techniques called “dancing links” for updating data structures during backtracking. This sets the stage for this section, which applies these ideas to the key problem of Boolean satisfiability, aka “SAT.” Section 7.2.2.2 is the longest section in “SAT,” and the SAT problem is clearly the killer app, because it is the key to solving many other problems. There was no clean way to split this section into separate subsections. (And anyway, the TAOCP format does not allow for a section 7.2.2.1.) I attempted to remedy the reader’s navigation problem by adding subheadings at the top of each page on the right hand side. In addition, as in the other sections, the exercises are presented in much the same order as the corresponding topics are covered in the text. Numerous cross-references are provided.
Satisfaction is important, mainly because Boolean algebra is so versatile. Almost any problem can be formulated in terms of basic logical operations, and the formulation is particularly simple in a great many cases.Section 7.2.2.2 begins with ten typical applications, which vary widely, and concludes with the following It turns out that all of these problems are special cases of SATs.116 and 117 (my favorite pages in the book). The satisfaction story is a triumphant tale of software engineering, replete with beautiful math. Thanks to the elegant new data structure and other techniques, modern SAT solvers can now be handled routinely. section 7.2.2.2 explains how this miracle happened by presenting the full details of the seven SAT solvers. Algorithms A and B to the state-of-the-art methods of Algorithms W, L, and C. (Well, we have to hedge a little: new techniques are being discovered all the time, so the SAT techniques keep evolving and the story keeps progressing. Algorithms W, L, and C can be reasonably compared to the best algorithms What was known in its class back in 2010. No longer state-of-the-art, but still amazingly good).
The book is over 300 pages, but I had to constantly “cut, cut, cut” because I knew there was so much more to it. Even as I was writing, I kept coming across interesting topics that were still unexplored, and it would have taken me a lifetime to get to the bottom of them. Still, I knew I had to move on. Therefore, I have selected a significant portion of the concepts that I believe will become most important as time goes on, and I have tried to address them here. To prepare this material, I have written over 300 computer programs. This is because you cannot understand things without programming them.
Of course, most of these programs are very short, but some of them are quite substantial and will be of interest to others. So we have posted some of them on the following web page: http://www-cs-faculty.stanford.edu/~knuth/programs.html You can also download SATexamples.tgz from this page.
Volume 4B begins with a special tutorial and review of probability theory in an unnumbered section entitled “Mathematical Preliminaries Redux.” References to its equations and exercises use the abbreviation “MPR.” (The word “improvement” is abbreviated below.)”
Example of SAT implementation
2-SAT, described in the Advanced Graph Algorithms section, is one example of a simple SAT application. Here, the “Priest Hohn’s Busiest Day” problem is used to automatically determine the possible schedules for a priest to attend multiple weddings.
Article on using Z3, a multi-platform SAT solver, in python. To get used to using it, it is better to install it with “pip install z3-solver” and then use it as a normal pyhton.
PySAT integrates a number of widely used state-of-the-art SAT solvers. All provided solvers are original low-level implementations that are installed with PySAT. The solver source code is not part of the project source tree, but is downloaded and patched each time PySAT is installed. (CaDiCaL (rel-1.0.3), CaDiCaL (rel-1.5.3), Glucose (3.0), Glucose (4.1), Lingeling (bbc-9230380-160707), MapleLCMDistChronoBT (SAT competition 2018 version), MapleCM (SAT competition 2018 version), Maplesat (MapleCOMSPS_LRB), Mergesat (3.0), Minicard (1.2), Minisat (2.2 release), Minisat ( GitHub version))
Rolling Stones is a Clojure interface to Sat4j’s SAT solver, which uses a brute-force search and using a combination of clever heuristics.
[rolling-stones "1.0.3"]
(require '[rolling-stones.core :as sat :refer [! at-least at-most exactly]])
=> (sat/solve [[1] [1 2] [-1 2 -3]])
[1 -2 -3]
=> (sat/solutions [[1] [1 2] [-1 2 -3]])
([1 -2 -3] [1 2 -3] [1 2 3])
コメント