我2017年7月加入Pivotal，伴随着被收购，2020年4月成为了VMware的员工。Greenplum近期招聘了非常多优秀的年轻人，充满希望。在看到了今年中国区编程比赛的报名通知的时候，我立刻把信息转发给某个manager，建议组织一些年轻人去打，最好拿个奖回来，多少扬扬名。然后Greenplum团队组了两个绝对年轻的队伍，全部是入职一年以内（或者出头一点点）。比赛昨天结束，两个队伍一个第一，一个第二，成绩很优异。
我没有参加，但是下午的时候，我看了一眼题目，第一反应肯定是NP问题，第二反应，这种东西，就应该用声明式编程语言求搞定。然后我花了一点点时间，写了一个Python程序，把题目编译成SMT程序，然后丢给Z3求解器去搞定。没有做什么优化，可以跑出8组解，感觉如果继续加入一些人类经验去优化，应该可以搞定大部分(有点装得不负责任)。
题目
给定一个0,1矩阵，可以算出它的DNA，DNA是每行的编码和每列的编码。编码是有损的，比如[0,1,0,1,1]的编码[1,2]，[1,1,1]的编码是[3]，[0,0,0]的编码是[0]，[1,1,0,1,1]的编码是[2,2]。给定这个0-1矩阵，是否存在另一个不同的0-1矩阵，DNA和它一模一样呢？
比如[[1,0],[0, 1]]和[[0,1],[1,0]]这俩的DNA就一样。
我的方案
死啦死啦一直推销他的方案,继续往我们死守的机场投送兵力,拖延甚至压垮鬼子空虚的后防!
《我的团长我的团》——兰晓龙
我没有用“我的算法”作为这小节的标题，是因为我满脑子都是兰晓龙的这句旁白（是的我又再N刷团长了）也因为我搞出来后，一直向年轻人推销我的方案，但是年轻人有年轻人的骄傲，他们用自己的程序拿到了头名。
我的方案就是每一行（每一列）编译成一个SMT约束，然后再把和自己不同这个条件编译出来，就可以丢给Z3了。
这里需要先根据输入的行，算出编码，然后根据编码，推理所有可能的组合。这是整个过程给你唯一需要用一点点脑力的地方，而这一步，也是可以加入很多人类经验用于剪枝的。然而其实人类可以推理出来，这一点点z3一定可以解决的。这一步用递归非常容易解决是下面函数的compute_line_from_dna这个函数。今天用我最喜欢的语言Erlang重写了这个过程。
-module(z3compiler).
-type dna() :: [integer()].
-type method() :: [{StartIndex::integer(), Len::integer()}].
-type direction() :: row | col.
-type matrix() :: [rows()].
-type rows() :: [integer()].
-type ir_exp() :: ir:ir_exp().
-export([gen_ir_code/1]).
-spec compute_dna_for_oneline([integer()]) -> dna().
compute_dna_for_oneline([]) -> [];
compute_dna_for_oneline(L) ->
L1 = lists:dropwhile(fun (I) -> I =:= 0 end, L),
case L1 of
[] ->
[0];
_ ->
L2 = lists:dropwhile(fun (I) -> I =:= 1 end, L1),
Numof1 = length(L1) - length(L2),
case compute_dna_for_oneline(L2) of
[0] ->
[Numof1];
D ->
[Numof1|D]
end
end.
-spec compute_line_from_dna(integer(), integer(), dna()) -> [method()].
compute_line_from_dna(_StartIdx, _EndIdx, []) -> [[]];
compute_line_from_dna(_StartIdx, _EndIdx, [0]) -> [[]];
compute_line_from_dna(StartIdx, EndIdx, [C|DNA]) ->
StartPos = case StartIdx =< EndIdx of
true ->
lists:seq(StartIdx, EndIdx);
false ->
[]
end,
FirstStepChoices = [{I, C}
|| I <- StartPos, I+C-1 =< EndIdx],
lists:append([lists:map(fun (M) -> [{I, L}|M] end,
compute_line_from_dna(I+L+1, EndIdx, DNA))
|| {I, L} <- FirstStepChoices]).
-spec gen_ir_code(matrix()) -> ir_exp().
gen_ir_code(M=[_LL|_]) ->
Mp = transform(M),
ir:make_and_ir([
gen_ir_code_for_lines(M, row),
gen_ir_code_for_lines(Mp, col),
gen_ir_code_not_self(M),
gen_ir_code_range(M)
]).
-spec gen_ir_code_for_line([integer()], integer(), direction()) -> ir_exp().
gen_ir_code_for_line(Line, LineId, Direct) ->
DNA = compute_dna_for_oneline(Line),
Methods = compute_line_from_dna(0, length(Line)-1, DNA),
IRs = [gen_ir_code_for_one_method(Method, LineId, Direct, length(Line))
|| Method <- Methods],
ir:make_or_ir(IRs).
-spec gen_ir_code_for_lines([[integer()]], direction()) -> ir_exp().
gen_ir_code_for_lines(Lines, Direct) ->
IRs = [gen_ir_code_for_line(Line, Id, Direct)
|| {Id, Line} <- lists:zip(lists:seq(0, length(Lines)-1), Lines)],
ir:make_and_ir(IRs).
-spec gen_ir_code_for_one_method(method(), integer(),
direction(), integer()) -> ir_exp().
gen_ir_code_for_one_method(Method, LineId, Direction, Length) ->
Sets = build_set(Method),
R = [{I, case sets:is_element(I, Sets) of
true ->
1;
false ->
0
end}
|| I <- lists:seq(0, Length-1)],
IRs = [case Direction of
row ->
ir:make_eq_ir(LineId, I, V);
col ->
ir:make_eq_ir(I, LineId, V)
end
|| {I, V} <- R],
ir:make_and_ir(IRs).
-spec gen_ir_code_not_self(matrix()) -> ir_exp().
gen_ir_code_not_self(M=[LL|_]) ->
RowIds = lists:seq(0, length(M)-1),
ColIds = lists:seq(0, length(LL)-1),
IRs1 = lists:append([[ir:make_eq_ir(I, J, 0) || {J, Bit} <- lists:zip(ColIds, Line), Bit =:= 1]
|| {I, Line} <- lists:zip(RowIds, M)]),
IRs2 = lists:append([[ir:make_eq_ir(I, J, 1) || {J, Bit} <- lists:zip(ColIds, Line), Bit =:= 0]
|| {I, Line} <- lists:zip(RowIds, M)]),
IRs = case length(IRs1) > length(IRs2) of
true ->
IRs2;
false ->
IRs1
end,
ir:make_or_ir(IRs).
-spec gen_ir_code_range(matrix()) -> ir_exp().
gen_ir_code_range(M=[LL|_]) ->
NRows = length(M),
NCols = length(LL),
ir:make_and_ir(lists:append([[ir:make_ge_ir(I, J, 0), ir:make_le_ir(I, J, 1)]
|| I <- lists:seq(0, NRows-1),
J <- lists:seq(0, NCols-1)]));
gen_ir_code_range(_) -> erlang:error(empty_matrix).
-spec build_set(method()) -> sets:sets(integer()).
build_set(M) ->
S = sets:new(),
build_set(M, S).
build_set([], S) -> S;
build_set([{I, L}|M], S) ->
NewS = sets:union(sets:from_list(lists:seq(I, I+L-1)), S),
build_set(M, NewS).
-spec transform(matrix()) -> matrix().
transform(M=[L|_]) ->
NCols = length(L),
[[lists:nth(R, Rows) || Rows <- M]
|| R <- lists:seq(1, NCols)];
transform(_) -> erlang:error(matrix_empty).
然后是一个从中间表示编译成字符串z3代码的模块：
-module(ir).
-type ir_exp() :: {eq, integer(), integer(), integer()}
| {le, integer(), integer(), integer()}
| {ge, integer(), integer(), integer()}
| {'and', [ir_exp()]}
| {'or', [ir_exp()]}.
-export_type([ir_exp/0]).
-export([to_z3/1, to_z3_file/2]).
-export([make_eq_ir/3, make_and_ir/1, make_or_ir/1, make_ge_ir/3, make_le_ir/3]).
-spec make_eq_ir(integer(), integer(), integer()) -> ir_exp().
make_eq_ir(I, J, V) ->
{eq, I, J, V}.
-spec make_and_ir([ir_exp()]) -> ir_exp().
make_and_ir([IR]) -> IR;
make_and_ir(IRs) ->
{'and', IRs}.
-spec make_or_ir([ir_exp()]) -> ir_exp().
make_or_ir([IR]) -> IR;
make_or_ir(IRs) ->
{'or', IRs}.
-spec make_ge_ir(integer(), integer(), integer()) -> ir_exp().
make_ge_ir(I, J, V) ->
{'ge', I, J, V}.
-spec make_le_ir(integer(), integer(), integer()) -> ir_exp().
make_le_ir(I, J, V) ->
{'le', I, J, V}.
-spec to_z3(ir_exp()) -> string().
to_z3({eq, I, J, V}) ->
io_lib:format("(= ~p (A ~p ~p))", [V, I, J]);
to_z3({ge, I, J, V}) ->
io_lib:format("(<= ~p (A ~p ~p))", [V, I, J]);
to_z3({le, I, J, V}) ->
io_lib:format("(>= ~p (A ~p ~p))", [V, I, J]);
to_z3({'and', IRs}) ->
"(and " ++ string:join([to_z3(IR) || IR <- IRs], "\n") ++ ")";
to_z3({'or', IRs}) ->
"(or " ++ string:join([to_z3(IR) || IR <- IRs], "\n") ++ ")".
to_z3_file(IR, File) ->
Head = "(declare-fun A (Int Int) Int)",
Assert = "(assert",
Code = to_z3(IR),
Foot = ")",
Check = "(check-sat)",
S = string:join([Head, Assert, Code, Foot, Check], "\n"),
file:write_file(File, list_to_binary(S)).
你可以这么跑下面的程序:
Eshell V10.6.4 (abort with ^G)
1> c(z3compiler).
{ok,z3compiler}
2> c(ir).
{ok,ir}
3> Matrix = [[0,1], [1,0]].
[[0,1],[1,0]]
4> IR = z3compiler:gen_ir_code(Matrix).
{'and',[{'and',[{'or',[{'and',[{eq,0,0,1},{eq,0,1,0}]},
{'and',[{eq,0,0,0},{eq,0,1,1}]}]},
{'or',[{'and',[{eq,1,0,1},{eq,1,1,0}]},
{'and',[{eq,1,0,0},{eq,1,1,1}]}]}]},
{'and',[{'or',[{'and',[{eq,0,0,1},{eq,1,0,0}]},
{'and',[{eq,0,0,0},{eq,1,0,1}]}]},
{'or',[{'and',[{eq,0,1,1},{eq,1,1,0}]},
{'and',[{eq,0,1,0},{eq,1,1,1}]}]}]},
{'or',[{eq,0,1,0},{eq,1,0,0}]},
{'and',[{ge,0,0,0},
{le,0,0,1},
{ge,0,1,0},
{le,0,1,1},
{ge,1,0,0},
{le,1,0,1},
{ge,1,1,0},
{le,1,1,1}]}]}
5> ir:to_z3_file(IR, "/tmp/m.z3").
ok
然后丢给z3:
gpadmin@zlyu:~$ z3 -smt2 /tmp/m.z3
sat
(model
(define-fun A ((x!0 Int) (x!1 Int)) Int
(ite (and (= x!0 0) (= x!1 0)) 1
(ite (and (= x!0 1) (= x!1 1)) 1
0)))
)
推荐资料
后记和思考
整个过程也图一乐，对于SMT2语言我也只是会个101，了解皮毛的皮毛，这是为啥也就图一乐呵。我感觉数据库里很多地方可以用到，如分区表的剪枝，direct dispatch的推理等等。还有很多地方应该可以用到Prolog或者其他逻辑编程工具。