361 lines
7.4 KiB
Prolog
361 lines
7.4 KiB
Prolog
%%============================================================================
|
|
%% The SWI-Prolog interface to MiniSat SAT solver
|
|
%% http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/MiniSat.html
|
|
%%
|
|
%% Copyright (c) 2006, Michael Codish, Vitaly Lagoon, and Peter J. Stuckey
|
|
%%
|
|
%% Permission is hereby granted, free of charge, to any person obtaining a
|
|
%% copy of this software and associated documentation files (the
|
|
%% "Software"), to deal in the Software without restriction, including
|
|
%% without limitation the rights to use, copy, modify, merge, publish,
|
|
%% distribute, sublicense, and/or sell copies of the Software, and to
|
|
%% permit persons to whom the Software is furnished to do so, subject to
|
|
%% the following conditions:
|
|
%%
|
|
%% The above copyright notice and this permission notice shall be included
|
|
%% in all copies or substantial portions of the Software.
|
|
%%
|
|
%% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
|
|
%% OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
|
|
%% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
|
%% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
|
|
%% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
|
|
%% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
|
|
%% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
|
|
|
:- module(minisat,[
|
|
solve/1,
|
|
sat/1,
|
|
sat_init/0,
|
|
sat_deinit/0,
|
|
sat_add_clauses/3,
|
|
sat_solve/1,
|
|
|
|
minimize/2,
|
|
maximize/2,
|
|
minimize_v1/2,
|
|
maximize_v1/2,
|
|
minimize_v2/2,
|
|
maximize_v2/2,
|
|
minimize_v3/2,
|
|
maximize_v3/2
|
|
]).
|
|
|
|
|
|
:- use_module(library(lists)).
|
|
|
|
:- load_foreign_library('pl-minisat',install).
|
|
|
|
:- dynamic tmp/1.
|
|
|
|
|
|
|
|
%%
|
|
%%
|
|
sat_init :-
|
|
minisat_new_solver, % - create the new solve
|
|
minisat_add_clause([-1]), % - add zero
|
|
minisat_add_clause([2]). % - add one
|
|
|
|
%%
|
|
%%
|
|
sat_deinit :-
|
|
minisat_delete_solver.
|
|
|
|
|
|
|
|
%%
|
|
%%
|
|
sat_add_clauses(Cs, Vs, MiniSat_Vs) :-
|
|
term_variables(Cs,CsVars),
|
|
\+ \+ (
|
|
bind2index(CsVars),
|
|
add_cnf_clauses(Cs),
|
|
asserta(tmp(Vs))
|
|
),
|
|
retract(tmp(MiniSat_Vs)).
|
|
|
|
add_cnf_clauses([]).
|
|
add_cnf_clauses([Cl|Cls]) :-
|
|
to_minisat(Cl,MiniSatCl),
|
|
minisat_add_clause(MiniSatCl),
|
|
add_cnf_clauses(Cls).
|
|
|
|
to_minisat([],[]).
|
|
to_minisat([L|Ls],[N|Ns]) :-
|
|
minisat_aux(L,N),
|
|
to_minisat(Ls,Ns).
|
|
|
|
minisat_aux(0,1) :- !.
|
|
minisat_aux(1,2) :- !.
|
|
minisat_aux(-(1),1) :- !.
|
|
minisat_aux(-(0),2) :- !.
|
|
minisat_aux(N,NN) :- NN is N.
|
|
|
|
|
|
bind2index(Vs) :-
|
|
minisat_nvars(N),
|
|
N1 is N+1,
|
|
bind2index_aux(Vs,N1).
|
|
|
|
bind2index_aux([],_N).
|
|
bind2index_aux([V|Ns],N) :-
|
|
var(V),
|
|
!,
|
|
V=N,
|
|
N1 is N+1, bind2index_aux(Ns,N1).
|
|
bind2index_aux([V|Ns],N) :-
|
|
integer(V),
|
|
bind2index_aux(Ns,N).
|
|
|
|
%%
|
|
%%
|
|
sat_solve(As) :-
|
|
to_minisat(As,MINISAT_As),
|
|
minisat_solve(MINISAT_As).
|
|
|
|
|
|
%%
|
|
%%
|
|
sat_get_values([],[]).
|
|
sat_get_values([SAT_V|SVs],[PL_V|PL_Vs]) :-
|
|
minisat_get_var_assignment(SAT_V,N),
|
|
( N<0 -> PL_V=0 ; PL_V=1),
|
|
sat_get_values(SVs,PL_Vs).
|
|
|
|
|
|
|
|
|
|
%%
|
|
%% sat(+CNF): succeds if CNF is satisfaiable, it does not bind the variables in CNF
|
|
%%
|
|
|
|
sat(CNF) :-
|
|
sat_init,
|
|
sat_add_clauses(CNF,_,_),
|
|
sat_solve([]),
|
|
sat_deinit,
|
|
!.
|
|
sat(_CNF) :-
|
|
sat_deinit,
|
|
!,
|
|
fail.
|
|
|
|
|
|
%%
|
|
%% solve(+CNF): like CNF/1 but bind the variables of CNF to the solution
|
|
%%
|
|
solve(CNF) :-
|
|
sat_init,
|
|
term_variables(CNF,CNF_Vs),
|
|
sat_add_clauses(CNF,CNF_Vs,SAT_Vs),
|
|
sat_solve([]),
|
|
sat_get_values(SAT_Vs,CNF_Vs),
|
|
sat_deinit,
|
|
!.
|
|
solve(_) :-
|
|
sat_deinit,
|
|
!,
|
|
fail.
|
|
|
|
|
|
%%
|
|
%%
|
|
%%
|
|
minimize(Vec,CNF) :- minimize_v1(Vec,CNF).
|
|
maximize(Vec,CNF) :- maximize_v1(Vec,CNF).
|
|
|
|
|
|
%%
|
|
%%
|
|
minimize_v1(Vec,CNF) :-
|
|
minimize_v1_aux(Vec,CNF),
|
|
sat(CNF).
|
|
|
|
minimize_v1_aux([],_CNF).
|
|
minimize_v1_aux([B|Bs],CNF) :-
|
|
minimize_v1_aux(Bs,CNF),
|
|
( (B=0, sat(CNF)) -> true ; B=1 ).
|
|
|
|
|
|
%%
|
|
%%
|
|
maximize_v1(Vec,CNF) :-
|
|
maximize_v1_aux(Vec,CNF),
|
|
sat(CNF).
|
|
|
|
maximize_v1_aux([],_CNF).
|
|
maximize_v1_aux([B|Bs],CNF) :-
|
|
maximize_v1_aux(Bs,CNF),
|
|
( (B=1, sat(CNF)) -> true ; B=0 ).
|
|
|
|
|
|
|
|
|
|
%%
|
|
%%
|
|
minimize_v2(Vec,CNF) :-
|
|
retractall(tmp(_)),
|
|
reverse(Vec,Vec_MSB),
|
|
term_variables(CNF,CNF_Vars),
|
|
sat_init,
|
|
sat_add_clauses(CNF,[Vec_MSB,CNF_Vars],[Vec_MSB_SVars,CNF_SVars]),
|
|
minimize_v2_loop(Vec_MSB_SVars),
|
|
sat_get_values(CNF_SVars,CNF_Vars),
|
|
sat_deinit,
|
|
!.
|
|
|
|
minimize_v2_loop([]) :-
|
|
sat_solve([]).
|
|
minimize_v2_loop([V|Vs]) :-
|
|
( sat_solve([-V]) ->
|
|
eliminate_prefix(Vs,0,New_Vs)
|
|
;
|
|
sat_add_clauses([[V]],_,_),
|
|
New_Vs=Vs
|
|
),
|
|
minimize_v2_loop(New_Vs).
|
|
|
|
|
|
|
|
%%
|
|
%%
|
|
maximize_v2(Vec,CNF) :-
|
|
reverse(Vec,Vec_MSB),
|
|
term_variables(CNF,CNF_Vars),
|
|
sat_init,
|
|
sat_add_clauses(CNF,[Vec_MSB,CNF_Vars],[Vec_MSB_SVars,CNF_SVars]),
|
|
maximize_v2_loop(Vec_MSB_SVars),
|
|
sat_get_values(CNF_SVars,CNF_Vars),
|
|
sat_deinit,
|
|
!.
|
|
|
|
maximize_v2_loop([]) :-
|
|
sat_solve([]).
|
|
maximize_v2_loop([V|Vs]) :-
|
|
( sat_solve([V]) ->
|
|
eliminate_prefix(Vs,1,New_Vs)
|
|
;
|
|
sat_add_clauses([[V]],_,_),
|
|
New_Vs=Vs
|
|
),
|
|
maximize_v2_loop(New_Vs).
|
|
|
|
|
|
|
|
|
|
|
|
%%
|
|
%%
|
|
minimize_v3(Vec,CNF) :-
|
|
retractall(tmp(_)),
|
|
term_variables(CNF,CNF_Vars),
|
|
sat_init,
|
|
sat_add_clauses(CNF,[Vec,CNF_Vars],[Vec_SVars,CNF_SVars]),
|
|
sat_solve([]),
|
|
sat_get_values(Vec_SVars,Curr_Min),
|
|
sat_get_values(CNF_SVars,Curr_Sol),
|
|
minimize_v3_loop(Vec_SVars,CNF_SVars,Curr_Min,Curr_Sol,Vec,CNF_Vars),
|
|
minisat_delete_solver,
|
|
!.
|
|
|
|
minimize_v3_loop(Vec,CNF_SVars,Last_Min,_Last_Sol,Final_Min,Final_Sol) :-
|
|
xs_gt_ys(Last_Min,Vec,CNF-[]),
|
|
sat_add_clauses(CNF,_,_),
|
|
sat_solve([]),
|
|
sat_get_values(Vec,Curr_Min),
|
|
sat_get_values(CNF_SVars,Curr_Sol),
|
|
!,
|
|
minimize_v3_loop(Vec,CNF_SVars,Curr_Min,Curr_Sol,Final_Min,Final_Sol).
|
|
minimize_v3_loop(_Vec,_CNF_SVars,Final_Min,Final_Sol,Final_Min,Final_Sol) :-
|
|
!.
|
|
|
|
|
|
|
|
%%
|
|
%%
|
|
maximize_v3(Vec,CNF) :-
|
|
retractall(tmp(_)),
|
|
term_variables(CNF,CNF_Vars),
|
|
sat_init,
|
|
sat_add_clauses(CNF,[Vec,CNF_Vars],[Vec_SVars,CNF_SVars]),
|
|
sat_solve([]),
|
|
sat_get_values(Vec_SVars,Curr_Max),
|
|
sat_get_values(CNF_SVars,Curr_Sol),
|
|
maximize_v3_loop(Vec_SVars,CNF_SVars,Curr_Max,Curr_Sol,Vec,CNF_Vars),
|
|
minisat_delete_solver,
|
|
!.
|
|
|
|
maximize_v3_loop(Vec,CNF_SVars,Last_Max,_Last_Sol,Final_Max,Final_Sol) :-
|
|
xs_gt_ys(Vec,Last_Max,CNF-[]),
|
|
sat_add_clauses(CNF,_,_),
|
|
sat_solve([]),
|
|
sat_get_values(Vec,Curr_Max),
|
|
sat_get_values(CNF_SVars,Curr_Sol),
|
|
!,
|
|
maximize_v3_loop(Vec,CNF_SVars,Curr_Max,Curr_Sol,Final_Max,Final_Sol).
|
|
maximize_v3_loop(_Vec,_CNF_SVars,Final_Max,Final_Sol,Final_Max,Final_Sol) :-
|
|
!.
|
|
|
|
|
|
|
|
|
|
%%
|
|
%%
|
|
eliminate_prefix([],_Bit,[]) :- !.
|
|
eliminate_prefix([V|Vs],Bit,New_Vs) :-
|
|
sat_get_values([V],[VVal]),
|
|
VVal = Bit,
|
|
( Bit = 0 -> sat_add_clauses([[-V]],_,_) ; sat_add_clauses([[V]],_,_) ),
|
|
!,
|
|
eliminate_prefix(Vs,Bit,New_Vs).
|
|
eliminate_prefix(Vs,Vs).
|
|
|
|
|
|
|
|
%%
|
|
%%
|
|
% B == (Xs = Ys)
|
|
xs_eq_ys([X],[Y],B,Cnf1-Cnf2) :-
|
|
!,
|
|
eq(X,Y,B,Cnf1-Cnf2).
|
|
xs_eq_ys([X|Xs],[Y|Ys],B,Cnf1-Cnf4) :-
|
|
eq(X,Y,B1,Cnf1-Cnf2),
|
|
xs_eq_ys(Xs,Ys,B2,Cnf2-Cnf3),
|
|
and(B1,B2,B,Cnf3-Cnf4).
|
|
|
|
%%
|
|
xs_gt_ys(Xs,Ys,[[B]|Cnf1]-Cnf2) :-
|
|
xs_gt_ys(Xs,Ys,B,Cnf1-Cnf2).
|
|
|
|
%%
|
|
%%
|
|
xs_gt_ys([X],[Y],B,Cnf1-Cnf2) :- !,
|
|
gt(X,Y,B,Cnf1-Cnf2).
|
|
xs_gt_ys(Xs,Ys,B, Cnf1-Cnf6) :-
|
|
split(Xs,LoXs,HiXs),
|
|
split(Ys,LoYs,HiYs),
|
|
xs_gt_ys(HiXs,HiYs,B1,Cnf1-Cnf2),
|
|
xs_eq_ys(HiXs,HiYs,B2,Cnf2-Cnf3),
|
|
xs_gt_ys(LoXs,LoYs,B3,Cnf3-Cnf4),
|
|
and(B2,B3,Tmp, Cnf4-Cnf5),
|
|
or(B1,Tmp,B,Cnf5-Cnf6).
|
|
|
|
% Z == X > Y (equivalently Z == X * -Y)
|
|
gt(X,Y,Z,[[Z,-X,Y],[-Z,X],[-Z,-Y]|Cnf]-Cnf).
|
|
|
|
% Z == (X == Y)
|
|
eq(X,Y,Z, [[-Z,-X,Y],[-Z,X,-Y],
|
|
[Z,X,Y],[Z,-X,-Y] | Cnf]-Cnf).
|
|
|
|
% Z == X or Y
|
|
or(X,Y,Z, [[Z,-X],[Z,-Y],[-Z,X,Y] | Cnf]-Cnf).
|
|
|
|
% Z == X and Y
|
|
and(X,Y,Z, [[Z,X,Y],[-Z,X],[-Z,Y] | Cnf]-Cnf).
|
|
|
|
%
|
|
split(Xs,As,Bs) :-
|
|
length(Xs,N), M is N // 2,
|
|
length(As,M), append(As,Bs,Xs).
|