SAT/SMTソルバを自作してみる話
この記事は Kobe University Advent Calendar 2017 - Adventar 17日目の記事です。
1年ぐらい前にC3というSMTソルバをC言語でスクラッチから作ったので、その話でもします。
よりによってなぜSMTソルバをCで書いたかというと、若気の至りでハイパーバイザに組み込んだりして遊んでたからです。
ゲストシステムの検証をランタイムにしてくれる超軽量なハイパーバイザあったらカッコイイじゃないですか。
という割と適当な理由で作ったんですが、労力に対する成果があまりにも見合わなさすぎて、今はアプローチを変えています。
そういうわけで過去の遺物から生まれたC言語製SMTソルバC3なのですが、このままお蔵入りさせるのも何なのでコードの解説とかSMTソルバがどうやって動いてるのかみたいな話をしてみます。
あ あと、私は一介の情報系学生で論理学徒ではないので、ところどころ不正確な表現があるかもしれないので指摘していただければ幸いです。
1. SATソルバとは
SMTソルバの説明の前にまずSATソルバの説明をします。
SATとはsatisfiability problem(充足可能性問題)の略です。
充足可能性問題というのは、一つの命題論理式が与えられたとき、それに含まれる変数の値を偽 (False) あるいは真 (True) にうまく定めることによって全体の値を'真'にできるか、という問題でクラスとしてはNP完全問題になります。
SATソルバは入力として命題論理式を受け取り、式全体の値を'真'にできる(SAT)場合は各変数に対する具体的な真偽値割り当てを出力し、そうでない場合は充足不能(UNSAT)である旨を出力します。
例えば以下のような論理式が与えられた時、
x1=真, x2=偽, を代入すると論理式は真になるので、(1,0)というような出力をします。
もう少しパッとする例として数独を解いてみましょう。
数独というのは以下のような感じで、
. .|. 4 . .|1 2 ---+---- . 1|4 3 4 3|2 1
- 各マスに 1 から 4 のいずれかが入る
- 各行に同じ数字が 2 回以上現れない
- 各列に同じ数字が 2 回以上現れない
- 各ブロックに同じ数字が 2 回以上現れない
のルールを満たすような数字を空いてる箇所に入れるという物です。よく新聞なんかに載ってるやつですね。
でこいつは実は充足可能性問題に落とし込めます。
詳しくは以下を見ていただければ良いですが、
SAT ソルバで数独を解く方法 - まめめも
要するに各マスに変数を割り当てて
a b|c d e f|g h ---+--- i j|k l m n|o p
各変数に対して1~4のどの数字が入るかをa1-a4という変数で表すことにします。つまり
- a1 が true のとき、a のマスには 1 が入る
- a2 が true のとき、a のマスには 2 が入る
- a3 が true のとき、a のマスには 3 が入る
- a4 が true のとき、a のマスには 4 が入る
てな感じです。
あとはこれら変数を使って数独のルール通りに論理式を組み立てて行くんですが、説明するのが面倒なので詳しくは上のURLを見てください。
で、私が作ったC3ソルバはSATソルバもあるので実際に解いてみましょう。
GitHub - RKX1209/c3: The C3, SMT/SAT solver written in C.
で、
$ make $ ./test/sudoku/gen_cnf.sh /usr/bin/c3 -D /tmp/sudoku.cnf > /tmp/c3-test/gen_cnf-BIfeLg/out 2> /tmp/c3-test/gen_cnf-BIfeLg/err
とかやると上に書いた数独の答えが /tmp/c3-test/gen_cnf-BIfeLg/err に出力されてます。
$ tail /tmp/c3-test/gen_cnf-BIfeLg/err (x1 or x3) and (!x3) and (!x27) and (!x38) and (!x3) and (!x38) and (!x27) and (!x3) and (!x27) and (!x38) found one literal -3(0x2431850) (x1) and (!x27) and (!x38) and (!x38) and (!x27) and (!x27) and (!x38) found one literal -27(0x2432b90) (x1) and (!x38) and (!x38) and (!x38) found one literal -38(0x2433960) (x1) found one literal 1(0x242f880) s SATISFIABLE v 1 -2 -3 -4 -5 6 -7 -8 -9 -10 11 -12 -13 -14 -15 16 -17 -18 19 -20 -21 -22 -23 24 25 -26 -27 -28 -29 30 -31 -32 -33 34 -35 -36 37 -38 -39 -40 -41 -42 -43 44 -45 -46 47 -48 -49 -50 -51 52 -53 -54 55 -56 -57 58 -59 -60 61 -62 -63 -64 0
はい。なんかログがドバっと出てますが大事なのは
s SATISFIABLE v 1 -2 -3 -4 -5 6 -7 -8 -9 -10 11 -12 -13 -14 -15 16 -17 -18 19 -20 -21 -22 -23 24 25 -26 -27 -28 -29 30 -31 -32 -33 34 -35 -36 37 -38 -39 -40 -41 -42 -43 44 -45 -46 47 -48 -49 -50 -51 52 -53 -54 55 -56 -57 58 -59 -60 61 -62 -63 -64 0
です。 これが結果で、a1,a2,a3,a4, b1,b2,b3...... p1,p2,p3,p4という64個の変数が内部で1~64まで番号付けされており、結果の1というのは1 = trueで-2というのは2=falseというように符号が-であればfalseを表します。
で、こいつを数独の結果に当てはめると
a1 = true, b2=true, c3=true, e3=true, f4=true, i2=true (既に数字が入ってる変数は省略)
です。盤面に起こすと
1 2|3 4 3 4|1 2 ---+---- 2 1|4 3 4 3|2 1
はい。正しく解けてます。
というわけでC3は充足可能性問題の応用例の一つとして数独も解けます。
2. DIMACSフォーマット
上でSATソルバの基本を説明しました。
殆どのSATソルバは入力として連言標準形(CNF)を受け取ります。
ソルバのアルゴリズム的にもCNFを対象とした方が何かと都合が良いケースが多いためです。
論理式クラスをCNFに絞ったSATを特にCNF-SATと言って、一般に殆どのSATソルバはCNF-SATを解く物になっています。
任意の命題論理式をCNFに変換するためのアルゴリズム(Tseitin Encoding)があるのでSATソルバ自体は入力をCNFに絞っても問題ないわけです。ちなみにCNF-SATもNP完全問題です。
さてこのCNFをSATソルバに入力として与える際のフォーマットというのがあって、DIMACSというのがデファクトスタンダードです。
DIMACSについては以下参照。まあとても単純なフォーマットです。
2009-02-08 - ひとり勉強会
C3は-DオプションをつけることでDIMACS形式を読んでSATソルバで解くことが出来ます。
$ ./c3 -D ./test/simple.cnf c: comment c: comment p: header size=3, val=5 1 -5 4 -1 5 3 4 -3 -4 (x1 or !x5 or x4) and (!x1 or x5 or x3 or x4) and (!x3 or !x4) assume 5 (x1 or x4) and (!x4 or !x3) pure literal -3 0x5626677ed030 (x1 or x4) pure literal 1 0x5626677ed030 s SATISFIABLE v 1 2 -3 4 5 0 Verifying.... [SUCCESS]
3. SMTソルバ
さて、ではSMTソルバの説明を簡単にします。
SMTはSatisfiable Modulo Theoriesの略で、一階述語論理式の充足可能性を判定してくれる点がSATソルバと異なります。命題論理よりも表現力が上がるので、ソフトウェアの検証や定理証明等に応用されます。
SMTソルバの基本的な構成は"SATソルバ" + "理論ソルバ"です。大まかな構図は以下のようになっています。
つまりa > 0やb-2c >= 0といった理論に依存する項の内容をAbstractionによって論理変数に変換し、
SATソルバに充足可能性を解いてもらった後、Abstractionによって失われたセマンティクスを理論ソルバ側で考慮して、本当に可能な真偽値割り当てなのかを検証した後、フィードバック的に再度制約を追加するという物です。
4. BitVectorセオリー
さて、SMTソルバで扱える理論には整数や有理数の算術、関数や等号に関する理論等あるのですが、今回C3で実装したのは、BitVectorと呼ばれる理論です。
この理論は主にソフトウェア、ハードウェアの検証に使用するためにメモリのモデル化を目指したものです。
具体的には、ソフトウェア上で扱われる整数等を2進数のバイナリbitとして扱い、プロセッサ同様に加減乗除算や符号拡張操作といったビット演算を扱う理論です。
具体的な文法は以下のようになっています。
formula : formula ∨ formula | ¬formula | atom atom : term rel term | Boolean-Identifier | term[ constant ] rel : = | < term : term op term | identifier | ∼ term | constant | atom?term:term | term[ constant : constant ] | ext( term ) op : + | − | · | / | << | >> | & | | | ⊕ | ◦ ∼ x: bit-wise negation of x ext(x): sign- or zero-extension of x x << d: left shift with distance d x ◦ y: concatenation of x and y
例えばa+bという式はBitVectorでは全加算器をモデルとして以下のように扱われます。
http://www.decision-procedures.org/slides/bit-vectors.pdfより
1-bitの加算は全加算器の論理式をCNFに変換し、図の下にあるような命題論理で表せます。
まあ要するにCPUのプロセッサー(論理回路)が行っている論理演算をそれぞれCNFに変換していくような理論です。
プログラムのような複雑な論理演算の集合も、全てCNFに変換してSATソルバに食わせるというのがBitVectorを実装したSMTソルバの概要です。
よって理論ソルバも必要ありません。なぜならそもそもBitVectorでは各変数がビット0/1を表すような理論であるため、Boolean Abstraction等の操作を行わなくても、CNFにさえ変換してしまえばそのままSATソルバに食わせられるからです。
BitVecotrについて詳しくは以下参照。
Bit-Vectors: Decision Procedures An Algorithmic Point of View
http://www.decision-procedures.org/slides/bit-vectors.pdf
5. 実装(SMTソルバ)
さて、ではC3のコードを見ながらSMTソルバの実装についてちょろっと解説します。
SMTソルバは検証したい条件式などをSMTLIB2というフォーマットで記述したファイルを入力として受け取ります。
SMTLIB2の仕様書はいかにあります。
The SMT-LIB Standard Version 2.5
SMT-LIB The Satisfiability Modulo Theories Library
C3のレポジトリにもサンプルがあります。
$ cat test/sign-extend.smt2 (set-logic QF_BV) (set-info :smt-lib-version 2.0) (echo "This is simple Sign Extend test") (declare-fun x () (_ BitVec 2)) ; sext1(x[2:]) < 0[3:] xor x[2:] < 0[2:] ; sext1(x) < 0 is equivalence to x < 0 ; This proposition must be true. Result of oppsition should become unsat (i.e. no counter example). (assert (xor (bvslt ((_ sign_extend 1) x) (_ bv0 3)) (bvslt x (_ bv0 2)))) (exit)
;はコメントです。まず(set-logic QF_BV)を指定する事でBitVector理論を使用する事を宣言します。
基本文法はS式です。 assertが証明したい仮定です。後はxorとかbvsltとかいろいろ演算がありますが、要するにこのサンプルが示したい仮定は
sext1(x) < 0 <=> x < 0
です。xが負数である事とxを符号拡張した物も同じく負数である事が同値であると言っています。
まあ直感的にも明らかですが、この仮定は正しいです。実際このassertはUNSATになります。
sext1(x) < 0 xor x < 0がUNSATなので、両者が1,0や0,1といった異なる真偽値を取る事が無い、つまり同値である
という事です。
ではC3の実装を見てみましょう。
C3は上記のようなSMTLIB2フォーマットファイルを受け取るとまず字句解析と構文解析を行います。
(flexとbisonを使用しています)
まずは字句解析ですが、まあこれは変数名に該当する字句規則を見つけたらテーブルに記録するぐらいしか特筆する事はないです。
parser/smt2.lex
c3/smt2.lex at master · RKX1209/c3 · GitHub
%{
/* C3 Theorem Prover - Apache v2.0 - Copyright 2017 - rkx1209 */
#include <stdbool.h>
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
#include <c3_core.h>
#include "parsesmt2.h"
extern char *yytext;
char *string_lit = NULL;
static int lookup(char *s) {
char * cleaned = NULL;
size_t len;
// The SMTLIB2 specifications sez that the outter bars aren't part of the
// name. This means that we can create an empty string symbol name.
if (s[0] == '|' && s[(len = strlen(s))-1] == '|') {
cleaned = (char*) malloc(len);
strncpy(cleaned,s+1,len-2); // chop off first and last characters.
cleaned[len-2] = '\0';
s = cleaned;
}
bool found = false;
ASTNode *sym_ast;
if ((sym_ast = c3_lookup_symbol(&c3, s))) {
found = true;
}
if (found) {
if (cleaned) {
free (cleaned);
}
yylval.node = ast_dup_node (sym_ast);
if (ast_get_type (yylval.node) == BOOLEAN_TYPE) {
printf ("FORMID: %s\n", s);
return FORMID_TOK;
} else {
printf ("TERMID: %s\n", s);
return TERMID_TOK;
}
} else {
if (cleaned)
free (cleaned);
yylval.str = strdup (s);
printf ("LITERAL: %s\n", s);
return STRING_TOK;
}
}
%}
%option noyywrap
LETTER ([a-zA-Z])
DIGIT ([0-9])
OPCHAR ([~!@$%^&*\_\-+=<>\.?/])
ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
%%
[ \n\t\r\f] { /* skip */ }
{DIGIT}+ { yylval.uintval = strtoul(yytext, NULL, 10); return NUMERAL_TOK; }
bv{DIGIT}+ { yylval.str = strdup(yytext + 2); return BVCONST_DECIMAL_TOK; }
#b{DIGIT}+ { yylval.str = strdup(yytext + 2); return BVCONST_BINARY_TOK; }
#x({DIGIT}|[a-fA-F])+ { yylval.str = strdup(yytext + 2); return BVCONST_HEXIDECIMAL_TOK; }
{DIGIT}+"."{DIGIT}+ { return DECIMAL_TOK; }
<STRING_LITERAL>. {
size_t old = strlen (string_lit);
if (!(string_lit = realloc (string_lit, old + 2))) {
c3_fatal_error ("string expansion failed\n");
}
string_lit[old] = *yytext;
string_lit[old + 1] = '\0'; }
<STRING_LITERAL>"\n" {
size_t old = strlen (string_lit);
if (!(string_lit = realloc (string_lit, old + 2))) {
c3_fatal_error ("string expansion failed\n");
}
string_lit[old] = *yytext;
string_lit[old + 1] = '\0'; }
/* Valid character are: ~ ! @ # $ % ^ & * _ - + = | \ : ; " < > . ? / ( ) */
"(" { return LPAREN_TOK; }
")" { return RPAREN_TOK; }
"_" { return UNDERSCORE_TOK; }
"!" { return EXCLAIMATION_MARK_TOK; }
":" { return COLON_TOK; }
/* Set info types */
/* This is a very restricted set of the possible keywords */
":source" { return SOURCE_TOK;}
":category" { return CATEGORY_TOK;}
":difficulty" { return DIFFICULTY_TOK; }
":smt-lib-version" { return VERSION_TOK; }
":status" { return STATUS_TOK; }
/* Attributes */
":named" { return NAMED_ATTRIBUTE_TOK; }
/* COMMANDS */
"assert" { return ASSERT_TOK; }
"check-sat" { return CHECK_SAT_TOK; }
"check-sat-assuming" { return CHECK_SAT_ASSUMING_TOK;}
"declare-const" { return DECLARE_CONST_TOK;}
.... (省略) ...
({LETTER}|{OPCHAR})({ANYTHING})* { return lookup (yytext); }
\|([^\|]|\n)*\| { return lookup(yytext); }
. { yyerror("Illegal input character."); }
%%
あとは構文解析ですが、SMTLIB2の仕様を読みながらそのまま書いていくだけです。
パースしながらASTを組み立てて行きます。
parser/smt2.y
c3/smt2.y at master · RKX1209/c3 · GitHub
%{
#include <stdint.h>
#include <stdio.h>
#include <string.h>
#include <parser/ast.h>
#include <parser/parser.h>
#include <c3_core.h>
#include <c3_utils.h>
/* C3 Theorem Prover - Apache v2.0 - Copyright 2017 - rkx1209 */
extern FILE* yyin;
extern char* yytext;
extern int yylineno;
int yyerror(const char *s) {
printf ("syntax error: line %d token: %s\n", yylineno, yytext);
return 1;
}
%}
%union {
unsigned uintval;
char *str;
ASTNode *node;
ASTVec vec;
};
%start cmd
%type <node> status
%type <vec> an_formulas an_terms function_params an_mixed
%type <node> an_term an_formula function_param
%token <uintval> NUMERAL_TOK
%token <str> BVCONST_DECIMAL_TOK
%token <str> BVCONST_BINARY_TOK
%token <str> BVCONST_HEXIDECIMAL_TOK
/* We have this so we can parse :smt-lib-version 2.0 */
%token DECIMAL_TOK
%token <node> FORMID_TOK TERMID_TOK
%token <str> STRING_TOK BITVECTOR_FUNCTIONID_TOK BOOLEAN_FUNCTIONID_TOK
/* set-info tokens */
%token SOURCE_TOK
%token CATEGORY_TOK
%token DIFFICULTY_TOK
%token VERSION_TOK
%token STATUS_TOK
/* ASCII Symbols */
/* Semicolons (comments) are ignored by the lexer */
%token UNDERSCORE_TOK
%token LPAREN_TOK
%token RPAREN_TOK
/* Used for attributed expressions */
%token EXCLAIMATION_MARK_TOK
%token NAMED_ATTRIBUTE_TOK
.... (省略) ...
var_decl:
/* (func () (_ BitVec 8)) */
STRING_TOK LPAREN_TOK RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK
{
ASTNode *ast_sym = c3_create_variable (0, $7, $1);
c3_add_symbol (&c3, $1, ast_sym);
} /* (func () Bool) */
.... (省略) ...
| LPAREN_TOK EQ_TOK an_term an_term RPAREN_TOK
{
ASTNode *n = ast_create_node2 (EQ, $3, $4);
$$ = n;
}
.... (省略) ...
上のコードでは適当に2つ程ルールを載せてみましたが、(func () (_ BitVec 8))のような関数宣言ではc3_create_variableや c3_add_symbol を使って宣言した関数名をシンボルとして追加してます。
あとはEQ_TOK(=)演算子が来た時は、ast_create_node2で2つの子を持つASTノードを生成してます。
あとは生成したASTノードを命題論理式に変換するBitBlastingという処理を行います。
tosat/bitblaster.c
c3/bitblaster.c at master · RKX1209/c3 · GitHub
/* C3 Theorem Prover - Apache v2.0 - Copyright 2017 - rkx1209 */ #include <parser/ast.h> #include <tosat/bitblaster.h> #include <stdlib.h> C3BitBlast *bb; /* (a == b) <=> (a[0] <-> b[0] && a[1] <-> b[1] && ... a[n] <-> b[n]) */ ASTNode *c3_bitblast_equal(ASTVec left, ASTVec right) { ASTNode *result, *node, *node2; C3ListIter *iter, *iter2; ASTVec ands = ast_vec_new (); if (c3_list_length (left) > 1) { iter2 = right->head; c3_list_foreach (left, iter, node) { node2 = (ASTNode *)iter2->data; ASTNode *biteq = ast_create_node2 (IFF, node, node2); ast_vec_add (ands, biteq); iter2 = iter2->n; } result = ast_create_node (AND, ands); } else { result = ast_create_node2 (IFF, (ASTNode *)left->head->data, (ASTNode *)right->head->data); } return result; } static ASTNode *c3_bitblast_bvle (ASTVec left, ASTVec right, bool sign, bool bvlt) { C3ListIter *lit, *rit; ASTNode *prevbit = bb->ASTTrue; lit = left->head; rit = right->head; while (lit->n != left->tail) { ASTNode *lnode = (ASTNode *)lit->data; ASTNode *rnode = (ASTNode *)rit->data; ASTNode *thisbit = ast_create_node3 (ITE, ast_create_node2 (IFF, rnode, lnode), prevbit, rnode); prevbit = thisbit; lit = lit->n; rit = rit->n; } ASTNode *lmsb = (ASTNode *)lit->data; ASTNode *rmsb = (ASTNode *)lit->data; if (sign) { lmsb = ast_create_node1 (NOT, lmsb); rmsb = ast_create_node1 (NOT, rmsb); } ASTNode *msb = ast_create_node3 (ITE, ast_create_node2 (IFF, rmsb, lmsb), prevbit, rmsb); if (bvlt) { msb = ast_create_node1 (NOT, msb); } return msb; } .... (省略) ... ASTVec c3_bitblast_term(ASTNode *term) { const ASTKind k = ast_get_kind (term); ASTVec children = term->children, result; unsigned int numbits = term->value_width; switch (k) { case BVNOT: { const ASTVec kids = c3_bitblast_term ((ASTNode *)children->head->data); result = c3_bitblast_neg (kids); break; } case BVSX: case BVZX: { printf ("BVSX¥n"); /* TODO: */ result = term; break; } case BVCONST: { printf ("BVCONST¥n"); ASTVec cnts = ast_vec_new (); ASTBVConst *bvconst = term->bvconst; unsigned int i; for (i = 0; i < numbits; i++) { ast_vec_add (cnts, ast_bvc_bit_test (bvconst, i) ? bb->ASTTrue : bb->ASTFalse); } result = cnts; break; } default: break; } return result; } .... (省略) ... ASTNode *c3_bitblast_form(ASTNode *form) { ASTNode *result, *child; ASTVec children = form->children; ASTVec echildren = ast_vec_new (); C3ListIter *iter; const ASTKind k = ast_get_kind (form); switch (k) { case TRUE: result = bb->ASTTrue; break; case FALSE: result = bb->ASTFalse; break; case NOT: result = ast_create_node1 (NOT, c3_bitblast_form ((ASTNode *)children->head->data)); break; case ITE: result = ast_create_node3 (ITE, c3_bitblast_form ((ASTNode *)children->head->data), c3_bitblast_form ((ASTNode *)children->head->n->data), c3_bitblast_form ((ASTNode *)children->head->n->n->data)); break; case AND: case OR: case NAND: case NOR: case IFF: case XOR: case IMPLIES: { printf ("TWO¥n"); c3_list_foreach (children, iter, child) { c3_list_append (echildren, c3_bitblast_form (child)); } result = ast_create_node (k, echildren); break; } case EQ: { ASTVec left = c3_bitblast_term ((ASTNode *)children->head->data); ASTVec right = c3_bitblast_term ((ASTNode *)children->head->n->data); result = c3_bitblast_equal (left, right); break; } case BVLE: case BVGE: case BVGT: case BVLT: case BVSLE: case BVSGE: case BVSGT: case BVSLT: { printf ("BVSLT¥n"); result = c3_bitblast_cmp (form); break; } default: break; } return result; } void c3_bitblast(C3 *c3, ASTNode *assertq) { bb = c3_bitblast_new (); assertq = c3_bitblast_form (assertq); c3_bitblast_free (bb); }
で、実はこのBitBlastingの処理がまだ全てのAST項に対応しきれていないので一部変換ができないのですが、
何をやってるかと言うと例えばa == bというSMTの式をa[0] <-> b[0] && a[1] <-> b[1] && ... a[n] <-> b[n]といった命題論理式のASTに変換してるわけです。
こうして命題論理式で表されるASTが生成された後、最後にTseitin EncodingでCNFに変換します。
Tseitin Encodingについては以下参照。
SATソルバを使うためにCNFを作る - soutaroブログ
6.実装(SATソルバ)
前節でSMTLIB2フォーマットの記述をCNFで表される命題論理式に変換する所までできたので、あとはこいつをSATソルバに食わせれば充足可能性を判定できます。
さて、C3はSATソルバも自前で用意しているので、その実装も少し見てみます。
アルゴリズムはDPLLを使っています。
DPLLアルゴリズム - Wikipedia
割と直感的なアルゴリズムで、以下のルールに従います。
- 1リテラル規則（one literal rule, unit rule）
リテラル L 1つだけの節があれば、L を含む節を除去し,他の節の否定リテラル ¬L を消去する。
- 純リテラル規則（pure literal rule, affirmative-nagative rule）
節集合の中に否定と肯定の両方が現れないリテラル（純リテラル） L があれば、L を含む節を除去する。
- 分割規則（splitting rule, rule of case analysis）
節集合 F の中に否定と肯定の両方があるリテラル L があれば、そのリテラルを真偽に解釈してえられる2つの節集合に分割する。
まあ要するに、明らかに真偽値が分かるようなリテラルを削除していって論理式のサイズを減らして行き、そうでない場合は分割規則で真偽値を2パターンはめてみて探索するという物です。
core.c
c3/core.c at master · RKX1209/c3 · GitHub
/* C3 Theorem Prover - Apache v2.0 - Copyright 2017 - rkx1209 */ #include <unistd.h> #include <stdarg.h> #include <stdbool.h> #include <stdio.h> #include <stdlib.h> #include <string.h> #include <getopt.h> #include <c3_core.h> #include <c3_utils.h> #include <parser/parsecnf.h> #include <parser/parser.h> #include <tosat/bitblaster.h> .... (省略) ... /* one literal rule */ static C3_STATUS _c3_dpll_simplify1(C3 *c3, C3List *cnf, int32_t *res) { bool simplify; C3_STATUS status = C3_NONE; C3ListIter *iter, *next; C3List *disj; do { simplify = false; iter = cnf->head; while (iter && (disj = iter->data)) { next = iter->n; if (c3_list_length (disj) == 1) { /* Found alone literal */ int32_t* onep = c3_list_head_data (disj); int32_t one = *onep; int32_t oneab = abs(one); int32_t value = (one < 0) ? -1 : 1; debug_log (1, "found one literal %d(%p)\n", one, onep); if (res[oneab - 1] && res[oneab - 1] != value) { /* literal is already set. inconsistent */ return C3_UNSAT; } res[oneab - 1] = value; simplify = true; _c3_dpll_remove2 (c3, cnf, one); status = C3_SIMPLIFY; _c3_print_cnf (cnf); } iter = next; } } while (simplify); return status; } /* pure literal rule */ static bool _c3_dpll_simplify2(C3 *c3, C3List *cnf, int32_t *res) { C3ListIter *iter, *iter2, *next; C3List *disj; int32_t *num, i, absi; bool *flag; C3_STATUS status = C3_NONE; /* Memorize all symbols */ c3_list_foreach (cnf, iter, disj) { c3_list_foreach (disj, iter2, num) { flag = malloc (sizeof(bool)); if (!flag) { return false; } *flag = true; c3_hmap_add_int32 (c3->literals, *num, flag); //c3_bstree_add (c3->literals2, num, c3_compare_value); } } /* Delete if literal is pure */ for (i = -c3->valnum; i <= c3->valnum; i++) { if (!c3_hmap_get_int32 (c3->literals, i)) { continue; } if (c3_hmap_get_int32 (c3->literals, -i)) { /* not pure. */ continue; } absi = abs(i); int32_t value = (i < 0) ? -1 : 1; if (res[absi - 1] && res[absi - 1] != value) { /* literal is already set. inconsistent */ return C3_UNSAT; } res[absi - 1] = value; iter = cnf->head; debug_log (1, "pure literal %d\t%p\n", i, iter); while (iter) { disj = iter->data; next = iter->n; if (c3_list_find (disj, &i, c3_compare_value)) { c3_list_clear (disj); c3_listiter_delete (cnf, iter); } iter = next; } status = C3_SIMPLIFY; _c3_print_cnf (cnf); } c3_hmap_clear (c3->literals); return status; } /* Simplification rules */ static C3_STATUS _c3_dpll_simplify(C3 *c3, C3List *cnf, int32_t *res) { C3_STATUS status1 = C3_NONE, status2 = C3_NONE; do { status1 = _c3_dpll_simplify1(c3, cnf, res); if (status1 == C3_UNSAT) return C3_UNSAT; status2 = _c3_dpll_simplify2(c3, cnf, res); if (status2 == C3_UNSAT) return C3_UNSAT; } while (status1 == C3_SIMPLIFY || status2 == C3_SIMPLIFY); return C3_NONE; } static C3_STATUS _c3_derive_dpll(C3 *c3, C3List *cnf, int32_t *res); .... (省略) ... /* DPLL algorithm */ static C3_STATUS _c3_derive_dpll(C3 *c3, C3List *cnf, int32_t *res) { C3ListIter *iter; C3List *disj; /* Simplify */ if (_c3_dpll_simplify (c3, cnf, res) == C3_UNSAT) { return C3_UNSAT; } if (c3_list_empty (cnf)) { return C3_SAT; } c3_list_foreach (cnf, iter, disj) { if (c3_list_empty (disj)) { return C3_UNSAT; } } return _c3_dpll_split (c3, cnf, res); } C3_STATUS c3_derive_sat(C3 *c3, int32_t *res) { if (c3 && res) { C3List *cnf2 = c3_dup_cnf (c3->cnf); C3_STATUS status = _c3_derive_dpll (c3, cnf2, res); c3_del_cnf (cnf2); return status; } return C3_INVALID; } .... (省略) ... int main(int argc, char **argv, char **envp) { .... (省略) ... /* Init */ c3_init (&c3); .... (省略) ... } else { /* SMT mode */ c3_smt2_parse (cnfp); c3_list_foreach (c3.asserts, iter, assertq) { c3_solve_by_sat (&c3, assertq); } } /* Finish */ fclose (cnfp); c3_fini (&c3); }
はい。 _c3_dpll_simplify1/2とかがリテラル規則になります。
興味ある人はgithubのコード読んでいただければと思います。
7.おわりに
息抜きのつもりで記事書いてたら1日潰れたが？？
SAT/SMTソルバ作りたい人間なんて本当にいるのか？という懐疑的な気持ちを抱きつつ、まあ自作まではやらなくてもどういう仕組みで動いてるかのザックリした理解は役立つかもしれないですね。
特にBitVectorに関してはソフトウェア/ハードウェア検証屋さんとか、脆弱性検出とかやってるセキュリティ研究屋さんとか。
