This repository has been archived on 2023-08-20. You can view files and clone it, but cannot push or open issues or pull requests.
yap-6.3/packages/swi-minisat2/minisat.pl
2014-08-23 14:47:40 -05:00

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).