Inspired by other verification system projects, I want to further explore the means of verification they used such as SMT solver, SAT solver, Coq and so on. I’ll start with this report from an advanced SAT solver — CryptoMinisat. (I have written a report about STP which is a SMT solver.)
The Boolean Satisfiability Problem (SAT for short) is the problem of determining if there exists an interpretation that satisfies a given boolean formula. In other words, it asks whether the variables of a given boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. Otherwise, the formula is unsatisfiable.
SAT solvers have recently been enjoying a boom in the application front: more and more applications can and do make use of SAT solvers to accomplish tasks ranging from the fairly trivial to the very complex. The benefit of the incredible improvements in the design of efficient SAT solvers those recent years is now reaching our lives: The Intel Core7 processor for instance has been designed with the help of SAT technology, while the device drivers of Windows 7 are being certified thanks to an SMT solver (based on a SAT solver).
Build and Test
This is the 5th version of CryptoMinisat which means the install instruction is very prefect now. To build and test this project, all we have to do is following the instruction. Firstly, we need to install many dependencies. Then, it is very simple to build by “make”. The following is part of the output.
Testing this project is very easy by the script written by the authors. Typing “make test” and waiting for a moment, we will get this output which means the tests are correct.
Run This Project
This is a very mature project which can be run from the terminal or used as a C++/Python library. In this report, I just choose the first way.
As I said before, this project is a SAT solver which means it could find out the situations which fulfill the input or return error. The grammar is very simple just like this.
The first line means this input has 2 variables and 4 clauses. Every line is a clause which is ended by “0”. Using the third line as an example, it says that 2 is TRUE and 3 is FALSE. I use this file as an input and run it in the terminal. The result is shown as follows. It means 1 is TRUE, 2 and 3 are FALSE is the only solution to this problem.
This is another example and the result.
It means there isn’t a solution to this problem.
How It Works
There are many improvements and techniques included in this project. It uses “Minisat” as its core and uses Gaussian Elimination on top-level. This is another part of its techniques.
- Variable elimination and replacement, strengthening and subsumption;
- Gate-based clause shortening and removal;
- No time or memory-outs on weird CNFs;
- Variable renumbering and variable number hiding. due to this, XOR clauses are cut and the added variables are always consistently displayed;
- Temporary results are stored in SQLite which supports high speed update;
- XOR recovery.
本文链接： http://home.meng.uno/articles/7d26fe8/ 欢迎转载！