1 | /* | |
2 | * Exposes Glucose API to SICStus Prolog | |
3 | * | |
4 | * Based on SWI Prolog Minisat Integration by | |
5 | * Michael Codish, Vitaly Lagoon, Peter J. Stuckey | |
6 | */ | |
7 | ||
8 | :- module(satsolver, [init_satsolver/0, sat/1, sat/2, bt_sat/1, multi_sat/3, b_sat/2]). | |
9 | ||
10 | :- use_module('../../src/module_information.pl'). | |
11 | :- module_info(group,experimental). | |
12 | :- module_info(description,'This is the interface between ProB and the Glucose SAT solver'). | |
13 | ||
14 | :- use_module(b_to_cnf). | |
15 | ||
16 | :- use_module(library(lists), [maplist/2,maplist/3]). | |
17 | ||
18 | foreign_resource('satsolver', [new_solver,solve,delete_solver, | |
19 | add_clause,assign_model,get_model]). | |
20 | ||
21 | foreign(new_solver, c, new_solver([-integer])). | |
22 | foreign(solve, c, solve(+integer)). | |
23 | foreign(delete_solver, c, delete_solver(+integer)). | |
24 | foreign(add_clause, c, add_clause(+integer,+term)). | |
25 | foreign(assign_model, c, assign_model(+integer,+term)). | |
26 | foreign(get_model, c, get_model(+integer,+term)). | |
27 | ||
28 | :- dynamic is_initialised/0. | |
29 | ||
30 | init_satsolver :- is_initialised,!. | |
31 | init_satsolver :- | |
32 | catch(load_foreign_resource(library(satsolver)),_,(print('*** LOADING satsolver library failed'),nl,fail)), | |
33 | assert(is_initialised). | |
34 | ||
35 | b_sat(BFormula,State) :- | |
36 | init_satsolver, | |
37 | b_to_cnf(BFormula,State,CNF),!, | |
38 | bt_sat(CNF). | |
39 | ||
40 | sat(CNF):- | |
41 | sat(CNF,Solved),!, | |
42 | Solved=1. | |
43 | ||
44 | sat([],1):-!. | |
45 | sat([[]],0):-!. | |
46 | sat(F,Solved):- | |
47 | new_solver(SolverID), | |
48 | setup_solver(SolverID), | |
49 | (addCnf2Solver(SolverID,F,FVars) | |
50 | -> (solve(SolverID) | |
51 | -> assign_model(SolverID,[1|FVars]), Solved = 1 | |
52 | ; Solved = 0) | |
53 | ; Solved=0), | |
54 | delete_solver(SolverID),!. | |
55 | ||
56 | bt_sat(F) :- | |
57 | new_solver(SolverID), | |
58 | bt_sat_aux(SolverID,F). | |
59 | ||
60 | bt_sat_aux(SolverID,F) :- | |
61 | setup_solver(SolverID), | |
62 | addCnf2Solver(SolverID,F,FVars), | |
63 | solve(SolverID), | |
64 | get_model(SolverID,[_|Model]), | |
65 | bt_sat(SolverID,FVars,Model). | |
66 | bt_sat_aux(SolverID,_) :- | |
67 | delete_solver(SolverID), fail. | |
68 | ||
69 | bt_sat(SolverID,FVars,_Model) :- | |
70 | assign_model(SolverID,[1|FVars]). | |
71 | bt_sat(SolverID,FVars,Model) :- | |
72 | add_negated_model(SolverID,Model), | |
73 | solve(SolverID), | |
74 | get_model(SolverID,[_|NewModel]), | |
75 | bt_sat(SolverID,FVars,NewModel). | |
76 | ||
77 | multi_sat([],_,1):-!. | |
78 | multi_sat([[]],_,0):-!. | |
79 | multi_sat(F,MaxSols,SolCount):- | |
80 | new_solver(SolverID), | |
81 | setup_solver(SolverID), | |
82 | (addCnf2Solver(SolverID,F,FVars) | |
83 | -> satMultiModels(SolverID,MaxSols,Models), | |
84 | delete_solver(SolverID),!, | |
85 | length(Models,SolCount), | |
86 | (SolCount == 0 ; assignMultiSols(Models,FVars)) | |
87 | ; delete_solver(SolverID),!,SolCount=0),!. | |
88 | ||
89 | satMultiModels(SolverID,MaxSols,Models):- | |
90 | MaxSols > 0,!, | |
91 | (solve(SolverID) | |
92 | -> get_model(SolverID,[_|Model]), | |
93 | Models=[Model|MoreModels], | |
94 | MaxSols1 is MaxSols - 1, | |
95 | ((MaxSols1 > 0, add_negated_model(SolverID,Model)) | |
96 | -> satMultiModels(SolverID,MaxSols1,MoreModels) | |
97 | ; MoreModels=[]) | |
98 | ; Models=[]). | |
99 | satMultiModels(_,_,[]):-!. | |
100 | ||
101 | add_negated_model(SolverID,Model):- | |
102 | maplist(neg,Model,NoAsgn), | |
103 | add_clause(SolverID,NoAsgn). | |
104 | ||
105 | neg(V,VN) :- VN is -V. | |
106 | ||
107 | assignMultiSols(Models,FVars):-!, | |
108 | length(FVars,VarLen), | |
109 | length(SoFar,VarLen), | |
110 | maplist(=([]),SoFar),!, | |
111 | assignMultiSols(Models,SoFar,FVars). | |
112 | ||
113 | assignMultiSols([],SoFar,SoFar):-!. | |
114 | assignMultiSols([M|Models],SoFar,Vars):-!, | |
115 | addModel2Vars(M,SoFar,NVars),!, | |
116 | assignMultiSols(Models,NVars,Vars). | |
117 | ||
118 | addModel2Vars([],[],[]). | |
119 | addModel2Vars([M|Ms],[V|Vs],[[NV|V]|NVs]):- | |
120 | (M>0 -> NV=1 ; NV= -1), | |
121 | addModel2Vars(Ms,Vs,NVs). | |
122 | ||
123 | addCnf2Solver(SolverID,Cnf,FVars):- | |
124 | term_variables(Cnf,FVars),!, | |
125 | \+ \+ (bind2index(FVars,3,FN), | |
126 | add_cnf_clauses(Cnf,SolverID), | |
127 | neg(FN,FNeg), | |
128 | add_cnf_clauses([[FN,FNeg]],SolverID)). | |
129 | ||
130 | add_cnf_clauses([Cl|Cls],SolverID):-!, | |
131 | maplist(to_minisat_cl,Cl,MiniSatCl), | |
132 | add_clause(SolverID,MiniSatCl), | |
133 | add_cnf_clauses(Cls,SolverID). | |
134 | add_cnf_clauses([],_):-!. | |
135 | ||
136 | setup_solver(SolverID) :- | |
137 | add_clause(SolverID,[1]), % true | |
138 | add_clause(SolverID,[-2]). | |
139 | ||
140 | to_minisat_cl(pred_true,1) :- !. | |
141 | to_minisat_cl(pred_false,2) :- !. | |
142 | to_minisat_cl(X,X). | |
143 | ||
144 | bind2index([N|Ns],N,FN) :- N1 is N+1, bind2index(Ns,N1,FN). | |
145 | bind2index([],N,FN):-!, FN is N - 1. |