1 | % (c) 2019-2025 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | :- module(cdclt_sat_solver, [b_to_cnf_safe/3, | |
6 | create_solver_state/1, | |
7 | sat/3, | |
8 | sat/4, | |
9 | sat/5, | |
10 | restarts/1, | |
11 | is_backjumping/0, | |
12 | announce_bt_from_smt_solution/0, | |
13 | store_idl_unsat_core/1, | |
14 | log_theory_propagation_sat_stack/4, | |
15 | set_variable_references_in_clauses/3, | |
16 | remove_idl_unsat_core/0, | |
17 | unit_propagate_cnf/4, | |
18 | get_bindings_from_ids/6, | |
19 | portray_cnf/1, | |
20 | cnf_to_smt/2, | |
21 | clear_pending_theory_propagations/0, | |
22 | unfixed_deferred_set_error_occurred/0, | |
23 | severe_error_occurred/0, | |
24 | assignment_timeout_occurred/0, | |
25 | log_det_theory_timeout/1, | |
26 | sat_bindings_to_smt_formula/2]). | |
27 | ||
28 | :- meta_predicate asserta_once(0). | |
29 | :- meta_predicate retract_if_exists(0). | |
30 | :- meta_predicate retract_once(0). | |
31 | :- meta_predicate bt_asserta(0). | |
32 | :- meta_predicate bt_retract(0). | |
33 | ||
34 | :- use_module(library(lists)). | |
35 | :- use_module(library(sets), [subtract/3]). | |
36 | :- use_module(library(heaps)). | |
37 | :- use_module(library(ordsets)). | |
38 | :- use_module(library(timeout)). | |
39 | :- use_module(library(samsort)). | |
40 | :- use_module(library(plunit)). | |
41 | ||
42 | :- use_module(smt_solvers_interface(ast_optimizer_for_smt)). | |
43 | :- use_module(cdclt_solver('cdclt_stats')). | |
44 | :- use_module(cdclt_solver('cdclt_pred_to_sat')). | |
45 | :- use_module(cdclt_solver('cdclt_settings')). | |
46 | :- use_module(cdclt_solver('symmetry_check/sat_symmetry_breaking')). | |
47 | :- use_module(probsrc(b_global_sets), [list_contains_unfixed_deferred_set_id/1]). | |
48 | :- use_module(probsrc(bsyntaxtree),[get_texpr_expr/2, | |
49 | find_typed_identifier_uses/3, | |
50 | safe_create_texpr/4, | |
51 | create_texpr/4, | |
52 | disjunct_predicates/2, | |
53 | conjunct_predicates/2, | |
54 | conjunction_to_list/2]). | |
55 | :- use_module(probsrc(debug)). | |
56 | :- use_module(probsrc(preferences), [temporary_set_preference/3, | |
57 | reset_temporary_preference/2]). | |
58 | :- use_module(probsrc(error_manager), [add_internal_error/2, | |
59 | add_error_fail/3, | |
60 | check_error_occured/2, | |
61 | error_occurred_in_error_scope/0]). | |
62 | :- use_module(probsrc(translate), [translate_bexpression/2]). | |
63 | :- use_module(extrasrc(unsat_cores), [unsat_core_with_fixed_conjuncts/3, | |
64 | unsat_chr_core_list_with_auto_time_limit/5]). | |
65 | :- use_module(probsrc(module_information), [module_info/2]). | |
66 | :- use_module(extension('banditfuzz/welldef')). | |
67 | ||
68 | :- use_module(extension('fibonacci_heap/fibonacci_heap')). | |
69 | %:- use_module(probsrc(tools_portability), [exists_source/1]). | |
70 | ||
71 | :- module_info(group, cdclt). | |
72 | :- module_info(description,'This module provides the SAT solver for CDCL(T) implementing CDCL with backjumping and further improvements.'). | |
73 | ||
74 | :- public solver_name/1. % but not used at the moment | |
75 | :- dynamic solver_name/1, backjump_clause/6, backjump_level/1, conflict_stats/3, saved_phase/2, restarts/1, | |
76 | bt_from_smt_solution/0, is_restart/0, | |
77 | %exclude_sat_solution_clause/1, | |
78 | total_lbd_sum/1, recent_lbds_dl/2, recent_stack_sizes_dl/2, luby_counter/1, | |
79 | %amount_clause_reductions/1, | |
80 | amount_learned_clauses/1, idl_unsat_core/1, pending_theory_prop/2, unfixed_deferred_set_error/0, assignment_count_on_cur_level/1, | |
81 | glue_level/3, glue_clauses/1, allow_partial_model/0, assignment_timeout_occurred/0. | |
82 | ||
83 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
84 | % A sat solver utilising delay declaration to implement watched literals. | |
85 | % Authors: Jacob Howe and Andy King | |
86 | % | |
87 | % Extended for CDCL(T) with first UIP conflict-driven clause learning, | |
88 | % theory propagation, branching heuristics, phase saving for rapid restarts, | |
89 | % learned clause reduction, clause minimization, random restarts, and static SMT symmetry breaking. | |
90 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
91 | ||
92 | % possible improvements: | |
93 | % (- FirstNewCutscheme (cf. https://www.aaai.org/Papers/JAIR/Vol22/JAIR-2210.pdf)) | |
94 | % [] improve implying constraint detection (e.g., :cdclt x > y & gt : {x+1} & y > gt) | |
95 | % -> might be overkill at some point | |
96 | % [] clause minimization (cf. Definition 9, "Towards Understanding and Harnessing the Potential of Clause Learning") | |
97 | % [] check out "Advances in Symmetry Breaking for SAT Modulo Theories" by Dinliwal et al. for static SMT symmetry breaking | |
98 | ||
99 | %:- if(exists_source(library(mutdict))). | |
100 | %:- use_module(library(mutdict)). | |
101 | %:- else. | |
102 | % mutdict throws a segmentation fault in SICStus 4.8.0, don't use it until the bug is fixed | |
103 | :- use_module(library(avl)). | |
104 | %mutdict_empty(Dict) :- | |
105 | % get_mutable(Avl, Dict), | |
106 | % empty_avl(Avl). | |
107 | ||
108 | new_mutdict(Dict) :- | |
109 | empty_avl(Avl), | |
110 | create_mutable(Avl, Dict). | |
111 | ||
112 | mutdict_put(Dict, Key, Value) :- | |
113 | get_mutable(Avl, Dict), | |
114 | avl_store(Key, Avl, Value, NewAvl), | |
115 | update_mutable(NewAvl, Dict). | |
116 | ||
117 | mutdict_get(Dict, Key, Value) :- | |
118 | get_mutable(Avl, Dict), | |
119 | avl_fetch(Key, Avl, Value). | |
120 | ||
121 | mutdict_keys(Dict, Keys) :- | |
122 | get_mutable(Avl, Dict), | |
123 | avl_domain(Avl, Keys). | |
124 | ||
125 | mutdict_update(Dict, Key, OldValue, NewValue) :- | |
126 | get_mutable(Avl, Dict), | |
127 | avl_change(Key, Avl, OldValue, NewAvl, NewValue), | |
128 | update_mutable(NewAvl, Dict). | |
129 | ||
130 | %mutdict_delete(Dict, Key) :- | |
131 | % get_mutable(Avl, Dict), | |
132 | % avl_delete(Key, Avl, _, NewAvl), | |
133 | % update_mutable(NewAvl, Dict). | |
134 | ||
135 | mutdict_items(Dict, Items) :- | |
136 | get_mutable(Avl, Dict), | |
137 | avl_to_list(Avl, Items). | |
138 | ||
139 | %mutdict_values(Dict, Values) :- | |
140 | % get_mutable(Avl, Dict), | |
141 | % avl_range(Avl, Values). | |
142 | %:- endif. | |
143 | ||
144 | pretty_print_clause([], []). | |
145 | pretty_print_clause([_-Pol-Var-Name|T], [Pol-Var-Name|NT]) :- | |
146 | pretty_print_clause(T, NT). | |
147 | ||
148 | pretty_print_vars([], []). | |
149 | pretty_print_vars([strip-Var|T], [NVar|NT]) :- | |
150 | !, | |
151 | pretty_print_clause(Var, NVar), | |
152 | pretty_print_vars(T, NT). | |
153 | pretty_print_vars([Var|T], [Var|NT]) :- | |
154 | pretty_print_vars(T, NT). | |
155 | ||
156 | debug_format_sat(_, _) :- | |
157 | print_logs(false), | |
158 | !. | |
159 | debug_format_sat(Msg, Vars) :- | |
160 | append(Msg, " (CDCL(T) SAT Solver)~n", NCodes), | |
161 | atom_codes(NMsg, NCodes), | |
162 | pretty_print_vars(Vars, NVars), | |
163 | format(NMsg, NVars), !. | |
164 | ||
165 | debug_format_sat(_, _, _) :- | |
166 | print_logs(false), | |
167 | !. | |
168 | debug_format_sat(Msg, Vars, Pred) :- | |
169 | format(Msg, Vars), | |
170 | translate:print_bexpr(Pred), nl, !. | |
171 | ||
172 | unfixed_deferred_set_error_occurred :- | |
173 | unfixed_deferred_set_error. | |
174 | ||
175 | assignment_count_on_cur_level(0). | |
176 | ||
177 | reset_assignment_count_on_level :- | |
178 | retract(assignment_count_on_cur_level(Old)), | |
179 | asserta(assignment_count_on_cur_level(0)), | |
180 | ( true | |
181 | ; retract(assignment_count_on_cur_level(_)), | |
182 | asserta(assignment_count_on_cur_level(Old)), | |
183 | fail | |
184 | ). | |
185 | ||
186 | get_next_assignment_count_on_level(NCount) :- | |
187 | retract(assignment_count_on_cur_level(Count)), | |
188 | NCount is Count + 1, | |
189 | asserta(assignment_count_on_cur_level(NCount)), | |
190 | ( true | |
191 | ; retract(assignment_count_on_cur_level(_)), | |
192 | asserta(assignment_count_on_cur_level(Count)), | |
193 | fail | |
194 | ). | |
195 | ||
196 | clear_pending_theory_propagations :- | |
197 | retractall_once(pending_theory_prop(_,_)). | |
198 | ||
199 | % this is just to replay the same order as is propagated to ProB using coroutines | |
200 | plvar_sort(_-(_-_-_-(_,(DLevel1,ACount1),_,_)), _-(_-_-_-(_,(DLevel2,ACount2),_,_))) :- | |
201 | ground(DLevel1), ground(DLevel2), | |
202 | ( DLevel1 < DLevel2 | |
203 | -> true | |
204 | ; DLevel1 == DLevel2 | |
205 | -> ACount1 < ACount2 | |
206 | ; fail | |
207 | ). | |
208 | ||
209 | sat_bindings_to_smt_formula(PlVars, SmtFormula) :- | |
210 | mutdict_items(PlVars, PlItems), | |
211 | samsort(plvar_sort, PlItems, SPlItems), | |
212 | sat_bindings_to_smt_formula_aux(SPlItems, b(truth,pred,[]), SmtFormula). | |
213 | ||
214 | sat_bindings_to_smt_formula_aux([], Acc, Acc). | |
215 | sat_bindings_to_smt_formula_aux([_-(PrologVar-_-TTheoryConstraint-_)|T], Acc, SmtFormula) :- | |
216 | ground(PrologVar), | |
217 | !, | |
218 | get_smt_formula_for_sat_pol(TTheoryConstraint, PrologVar, TheoryConstraint), | |
219 | safe_create_texpr(conjunct(Acc,TheoryConstraint), pred, [], NAcc), | |
220 | sat_bindings_to_smt_formula_aux(T, NAcc, SmtFormula). | |
221 | sat_bindings_to_smt_formula_aux([_|T], Acc, SmtFormula) :- | |
222 | sat_bindings_to_smt_formula_aux(T, Acc, SmtFormula). | |
223 | ||
224 | %% get_bindings_from_ids(+SatVars, -StackBindings, -SatBindings, -SatVarNames, -IdPrologVarTuples, -PrologSatVarTriple). | |
225 | % Given a set of boolean B identifiers. Create a list of bindings containing terms bind/2 | |
226 | % and a list of tuples of B identifier and corresponding Prolog variable used for sat solving. | |
227 | % StackBindings contain the bind/2 terms as well as the StackInfo in order to unify Prolog variables in b_to_cnf_safe/3. | |
228 | get_bindings_from_ids(SatVars, StackBindings, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple) :- | |
229 | new_mutdict(EmptyDict), | |
230 | get_bindings_from_ids_acc(SatVars, [], [], [], [], EmptyDict, StackBindings, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple), !. | |
231 | ||
232 | get_bindings_from_ids_acc([], AccStackBindings, AccBindings, AccNames, AccTuples, AccPlVars, AccStackBindings, AccBindings, AccNames, AccTuples, AccPlVars). | |
233 | get_bindings_from_ids_acc([b(identifier(Name),IdType,IdInfo)|T], AccStackBindings, AccBindings, AccNames, AccTuples, AccPlVars, StackBindings, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple) :- | |
234 | NewAccBindings = [bind(Name,PrologVar)|AccBindings], | |
235 | % we add Prolog variables for stack infos to each var so that we do not have to maintain a genuine stack | |
236 | StackInfo = (_PropType, _Level, _Pol, _OriginalClause), | |
237 | NewAccStackBindings = [bind(Name,PrologVar)-StackInfo|AccStackBindings], | |
238 | NewAccTuples = [(b(identifier(Name),IdType,IdInfo),PrologVar,StackInfo)|AccTuples], | |
239 | !, | |
240 | ? | ( member(smt_formula(SmtFormula), IdInfo) |
241 | -> mutdict_put(AccPlVars, Name, PrologVar-Name-SmtFormula-StackInfo) | |
242 | ; % plain SAT variable which is not reified with a theory solver, e.g., introduced by CNF optimization rewriting | |
243 | OptEq = b(equal(b(identifier(Name),boolean,[]),b(boolean_true,boolean,[])),pred,[]), | |
244 | mutdict_put(AccPlVars, Name, PrologVar-Name-OptEq-StackInfo) | |
245 | ), | |
246 | get_bindings_from_ids_acc(T, NewAccStackBindings, NewAccBindings, [Name|AccNames], NewAccTuples, AccPlVars, StackBindings, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple). | |
247 | get_bindings_from_ids_acc([_|T], AccStackBindings, AccBindings, AccNames, AccTuples, AccPlVars, StackBindings, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple) :- | |
248 | get_bindings_from_ids_acc(T, AccStackBindings, AccBindings, AccNames, AccTuples, AccPlVars, StackBindings, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple). | |
249 | ||
250 | %% sat(+SolverName, +SolverEnv, +Clauses). | |
251 | % SolverEnv is a list [sat_vars:_, sat_varnames:_, sat_bindings:_, t2b_env:_, pl_vars:_]. | |
252 | % sat_vars are boolean b/3 identifier ASTs for corresponding SAT variables in Clauses. | |
253 | % sat_bindings is a list of terms bind/2 as used by the ProB constraint solver. | |
254 | % t2b_env is the environment mapping SAT variable names and theory formulae used to | |
255 | % translate B predicates to SAT. | |
256 | % pl_vars is a dict of tuples PrologVar-SatVarName-SmtFormula-StackInfo. | |
257 | sat(SolverName, SolverEnv, Clauses) :- | |
258 | debug_format_sat("Start SAT solving with solver ~w ", [SolverName]), | |
259 | init_dynamic_solver_state(SolverName), | |
260 | create_solver_state(StateMutable), | |
261 | get_from_solver_env(SolverEnv, binary_clause_vars, VarsFromBinaryClauses), | |
262 | init_decision_heuristic(StateMutable, VarsFromBinaryClauses, Clauses), | |
263 | sat_stateful_pre(SolverEnv, StateMutable, Clauses). | |
264 | ||
265 | %% sat(+SolverName, +SolverEnv, +StateMutable, +Clauses). | |
266 | sat(SolverName, SolverEnv, StateMutable, Clauses) :- | |
267 | sat(SolverName, SolverEnv, StateMutable, Clauses, []). | |
268 | ||
269 | %% sat(+SolverName, +SolverEnv, +StateMutable, +Clauses, +Options). | |
270 | % Options: | |
271 | % allow_partial_model: only for SMT solving: possibly does not assign all SAT variables, | |
272 | % but the reification with ProB ensures that all coroutines are triggered | |
273 | sat(SolverName, SolverEnv, StateMutable, Clauses, Options) :- | |
274 | debug_format_sat("Start SAT solving with solver ~w ", [SolverName]), | |
275 | init_dynamic_solver_state(SolverName), | |
276 | ( memberchk(allow_partial_model, Options) | |
277 | -> asserta(allow_partial_model) | |
278 | ; true | |
279 | ), | |
280 | get_from_solver_env(SolverEnv, binary_clause_vars, VarsFromBinaryClauses), | |
281 | ? | init_decision_heuristic(StateMutable, VarsFromBinaryClauses, Clauses), |
282 | ? | sat_stateful_pre(SolverEnv, StateMutable, Clauses). |
283 | ||
284 | % Wrapper for sat_stateful_restart_cp/3 to enable backjumping to level 0 several times. | |
285 | sat_stateful_pre(SolverEnv, StateMutable, Clauses) :- | |
286 | \+ severe_error_occurred, | |
287 | ? | sat_stateful_restart_cp(SolverEnv, StateMutable, Clauses). |
288 | ||
289 | sat_stateful_restart_cp(SolverEnv, StateMutable, Clauses) :- | |
290 | ? | ( sat_stateful(SolverEnv, StateMutable, Clauses) |
291 | ; % we either learned a unit-clause from conflict analysis or randomly restart | |
292 | % in both cases, we learn all asserted backjump clauses | |
293 | retract(backjump_level(0)), | |
294 | ( retract(is_restart) | |
295 | -> debug_format_sat("backjump to level 0 random restart", []), | |
296 | backjump_clause(LearnFromLevel,_,_,_,_,_) | |
297 | ; debug_format_sat("backjump to level 0", []), | |
298 | LearnFromLevel = 0 | |
299 | ), | |
300 | learn_backjump_clause(LearnFromLevel, SolverEnv, StateMutable), | |
301 | sat_stateful_pre(SolverEnv, StateMutable, Clauses) | |
302 | ). | |
303 | ||
304 | %% sat_stateful(+Clauses, +StateMutable, +Clauses). | |
305 | % CDCL with first UIP conflict-driven clause learning, two-watched literals, EVSIDS branching heuristic, | |
306 | % random glucose restarts, and phase saving for rapid restarts. | |
307 | % See create_solver_state/1 for variable StateMutable. | |
308 | sat_stateful(SolverEnv, StateMutable, Clauses) :- | |
309 | ? | problem_setup(SolverEnv, StateMutable, Clauses), |
310 | %static_sat_symmetry_breaking(Clauses, SolverEnv, CurLevelMut, NewSolverEnv), | |
311 | ? | elim_vars(SolverEnv, StateMutable). |
312 | ||
313 | %% elim_vars(+SolverEnv, +StateMutable). | |
314 | elim_vars(SolverEnv, StateMutable) :- | |
315 | \+ severe_error_occurred, | |
316 | get_full_state(StateMutable, cur_level, CurLevel), | |
317 | NextLevel is CurLevel + 1, | |
318 | ? | reset_assignment_count_on_level, |
319 | ( % solution found | |
320 | fibonacci_heap:is_empty | |
321 | -> true | |
322 | ; elim_vars_from_asserted_heuristic_rapid_restart(SolverEnv, StateMutable, NextLevel) | |
323 | ). | |
324 | ||
325 | learn_backjump_clause(CurLevel, SolverEnv, StateMutable) :- | |
326 | retract(backjump_clause(BjLevel, BjClause, _, BjSatVars, UsedVars, AC)), | |
327 | ( CurLevel == BjLevel | |
328 | -> true | |
329 | ; add_error_fail(learn_backjump_clause, 'Inconsistent backjump level: ', [BjLevel,CurLevel]) | |
330 | ), | |
331 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
332 | set_variable_references_in_clause(PlVars, BjClause, BjClauseRef), | |
333 | ? | clause_setup(SolverEnv, StateMutable, BjClauseRef), |
334 | ? | update_heuristic_scores_for_vars(BjSatVars, AC), |
335 | ( bump_scores_for_bj_clause_only(true) | |
336 | ; % additionally bump scores for all variables used during conflict analysis | |
337 | bump_scores_for_bj_clause_only(false), | |
338 | ? | update_heuristic_scores_for_vars(UsedVars, AC) |
339 | ), !. | |
340 | ||
341 | possibly_backjump(_, _, _). | |
342 | possibly_backjump(SolverEnv, StateMutable, NextLevel) :- | |
343 | % backjumping to a level other than 0; skip for restart since we then backjump to level 0 | |
344 | \+ is_restart, | |
345 | backjump_level(C), | |
346 | debug_format_sat("Current level is ~w and bj level is ~w", [NextLevel,C]), | |
347 | C == NextLevel, | |
348 | retract(backjump_level(C)), | |
349 | debug_format_sat("~nbackjump branch prop level ~w", [NextLevel]), | |
350 | learn_backjump_clause(C, SolverEnv, StateMutable), | |
351 | possibly_bump_glue_variable_scores(NextLevel), | |
352 | possibly_backjump(SolverEnv, StateMutable, NextLevel). | |
353 | ||
354 | possibly_bump_glue_variable_scores(CurLevel) :- | |
355 | ( ( glue_bumping(true), | |
356 | glue_clauses(GC), | |
357 | GC \== 0 | |
358 | ) | |
359 | -> bump_glue_variable_scores(GC, CurLevel) | |
360 | ; true | |
361 | ). | |
362 | ||
363 | bump_glue_variable_scores(GC, CurLevel) :- | |
364 | ( bt_retract(glue_level(GlueVar,GlueLevel,AlreadyBumped)) | |
365 | -> ( ( \+ AlreadyBumped, | |
366 | GlueLevel > CurLevel | |
367 | ) | |
368 | -> fibonacci_heap:get_priority_of(GlueVar, Score), | |
369 | bump_glue_variable_score(Score, GlueVar, GlueLevel, GC), | |
370 | bump_glue_variable_scores(GC, CurLevel), | |
371 | bt_asserta(glue_level(GlueVar,GlueLevel,true)) | |
372 | ; bump_glue_variable_scores(GC, CurLevel), | |
373 | bt_asserta(glue_level(GlueVar,GlueLevel,AlreadyBumped)) | |
374 | ) | |
375 | ; true | |
376 | ). | |
377 | ||
378 | bump_glue_variable_score(Score, SatVarName, GlueLevel, GC) :- | |
379 | GlueBump is Score * (GlueLevel/GC), | |
380 | NScore is Score + GlueBump, | |
381 | fibonacci_heap:update_bt(SatVarName, NScore). | |
382 | ||
383 | %% elim_vars_from_asserted_heuristic_rapid_restart(+SolverEnv, +StateMutable, +NextLevel). | |
384 | elim_vars_from_asserted_heuristic_rapid_restart(SolverEnv, StateMutable, NextLevel) :- | |
385 | \+ backjump_level(_), | |
386 | \+ idl_unsat_core(_), | |
387 | ? | get_sat_var_with_max_heuristic(SatVarName, MaxScore), |
388 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
389 | mutdict_get(PlVars, SatVarName, Var-SatVarName-_-StackInfo), % we need the variable's references | |
390 | debug_format_sat("Max heuristic value with score ~w is ~w", [MaxScore,SatVarName]), | |
391 | ? | possibly_backjump(SolverEnv, StateMutable, NextLevel), |
392 | ( saved_phase(SatVarName, SavedPol) | |
393 | -> % restore phase/polarity from cache for rapid restart | |
394 | SelectedPol = SavedPol, | |
395 | retract(saved_phase(SatVarName, _)), % don't undo when backtracking | |
396 | debug_format_sat("Restore phase of ~w", [SatVarName]) | |
397 | ; % uninformed phase/polarity selection: start with truth | |
398 | SelectedPol = pred_true | |
399 | ), | |
400 | elim_var_for_phase(SatVarName, StackInfo, SelectedPol, Var, SolverEnv, StateMutable, NextLevel). | |
401 | ||
402 | %% elim_var_for_phase(+SatVarName, +StackInfo, +SavedPol, +Var, +SolverEnv, +StateMutable, +NextLevel). | |
403 | elim_var_for_phase(SatVarName, StackInfo, SavedPol, Var, SolverEnv, StateMutable, NextLevel) :- | |
404 | ( ground(Var) | |
405 | -> add_error_fail(elim_var_for_phase, 'Decision variable is already ground: probably an error in the decision heuristic.', [SatVarName]) | |
406 | ; true | |
407 | ), | |
408 | update_full_state(StateMutable, cur_level, NextLevel), | |
409 | ? | get_next_assignment_count_on_level(ACount), |
410 | ( StackInfo = (branch,(NextLevel,ACount),SavedPol,_OriginalClause), | |
411 | ? | bt_log_sat_stack(StateMutable, SatVarName, SavedPol), |
412 | debug_format_sat("Decide variable ~w with polarity ~w on level ~w", [SatVarName,SavedPol,NextLevel]), | |
413 | log_boolean_decision, | |
414 | Var = SavedPol | |
415 | ; \+ backjump_level(_), | |
416 | \+ severe_error_occurred, | |
417 | negate_polarity(SavedPol, NegSavedPol), | |
418 | StackInfo = (branch,(NextLevel,ACount),NegSavedPol,_OriginalClause), | |
419 | bt_log_sat_stack(StateMutable, SatVarName, NegSavedPol), | |
420 | debug_format_sat("Decide variable ~w with polarity ~w on level ~w", [SatVarName,NegSavedPol,NextLevel]), | |
421 | log_boolean_decision, | |
422 | Var = NegSavedPol | |
423 | ), | |
424 | ? | elim_vars(SolverEnv, StateMutable). |
425 | ||
426 | %% checkout_sat_variable(+SatVarName, +OriginalClause). | |
427 | % Remove a SAT variable's information if it has been propagated. | |
428 | checkout_sat_variable(SatVarName, OriginalClause) :- | |
429 | ? | delete_from_heuristic(SatVarName), |
430 | retract_if_exists(saved_phase(SatVarName, _)), | |
431 | ( allow_partial_model | |
432 | ? | -> worsen_scores_for_vars_in_clause(OriginalClause) |
433 | ; true | |
434 | ). | |
435 | ||
436 | worsen_scores_for_vars_in_clause([]). | |
437 | worsen_scores_for_vars_in_clause([_-_-_-SatVarName|T]) :- | |
438 | ( fibonacci_heap:get_priority_of_silent_fail(SatVarName, Score) | |
439 | -> ( Score > 1, | |
440 | ? | fibonacci_heap:dec_priority_of_bt(SatVarName, 1) |
441 | ; Score =< 1, | |
442 | ? | fibonacci_heap:delete_elm_bt(SatVarName) |
443 | ), | |
444 | ? | worsen_scores_for_vars_in_clause(T) |
445 | ? | ; worsen_scores_for_vars_in_clause(T) |
446 | ). | |
447 | ||
448 | problem_setup(_, _, []). | |
449 | problem_setup(SolverEnv, StateMutable, [Clause|Clauses]) :- | |
450 | ? | clause_setup(SolverEnv, StateMutable, Clause), |
451 | ? | problem_setup(SolverEnv, StateMutable, Clauses). |
452 | ||
453 | clause_setup(SolverEnv, StateMutable, Clause) :- | |
454 | Clause = [StackInfo-Pol-Var-SatVarName|Triples], | |
455 | ? | set_watch(SolverEnv, StateMutable, Clause, Triples, Var, Pol, SatVarName, StackInfo). |
456 | ||
457 | set_polarity_of_var_explicitly(_, _, [], []). | |
458 | set_polarity_of_var_explicitly(SatVarName, Pol, [CPol-CVar-CName|T], ConflictClause) :- | |
459 | var(CVar), | |
460 | SatVarName == CName, | |
461 | !, | |
462 | ConflictClause = [CPol-Pol-CName|T]. | |
463 | set_polarity_of_var_explicitly(SatVarName, Pol, [Triple|T], [Triple|NT]) :- | |
464 | set_polarity_of_var_explicitly(SatVarName, Pol, T, NT). | |
465 | ||
466 | set_watch(_, _, OriginalClause, [], Var, Pol, SatVarName, _) :- | |
467 | Var == Pol, | |
468 | checkout_sat_variable(SatVarName, OriginalClause). | |
469 | set_watch(SolverEnv, StateMutable, OriginalClause, [], Var, Pol, _, _) :- | |
470 | ground(Var), | |
471 | Var \== Pol, | |
472 | \+ severe_error_occurred, | |
473 | \+ backjump_level(_), | |
474 | debug_format_sat("sat conflict", []), | |
475 | clause_learning(true), | |
476 | possibly_bt_from_smt_solution(SolverEnv,StateMutable, _, _), | |
477 | get_full_state(StateMutable, current_stack_size, StackSize), | |
478 | get_full_state(StateMutable, cur_level, CurLevel), | |
479 | assignment_count_on_cur_level(ACount), | |
480 | ACount \== 1, % at least one unit-propagation for CDCL, otherwise just backtrack to the last decision | |
481 | compute_and_assert_backjump_clause(SolverEnv, StateMutable, StackSize, CurLevel, OriginalClause), | |
482 | fail. | |
483 | set_watch(SolverEnv, StateMutable, OriginalClause, [], Var, Pol, SatVarName, StackInfo) :- | |
484 | var(Var), | |
485 | \+ severe_error_occurred, | |
486 | \+ backjump_level(_), | |
487 | get_full_state(StateMutable, cur_level, CurLevel), | |
488 | debug_format_sat("unit propagation of ~w with polarity ~w on level ~w due to clause ~w", [SatVarName,Pol,CurLevel,strip-OriginalClause]), | |
489 | %translate:print_bexpr(TheoryFormula),nl, | |
490 | ? | get_next_assignment_count_on_level(ACount), |
491 | StackInfo = (unit,(CurLevel,ACount),Pol,OriginalClause), | |
492 | ? | bt_log_sat_stack(StateMutable, SatVarName, Pol), |
493 | log_unit_propagation, | |
494 | ? | ( checkout_sat_variable(SatVarName, OriginalClause), |
495 | Var = Pol, | |
496 | ? | ( true |
497 | ; % remove idl unsat core from higher decision level when backtracking | |
498 | remove_idl_unsat_core, | |
499 | fail | |
500 | ) | |
501 | ; % theory conflict: if Var = Pol triggered a SAT conflict instead, | |
502 | % a backjump clause has been computed and backjump_level/1 is asserted | |
503 | clause_learning(true), | |
504 | \+ severe_error_occurred, | |
505 | \+ backjump_level(_), % skip when backjumping | |
506 | get_last_decision_level(StateMutable, LastDLevel), % skip if no decision so far | |
507 | LastDLevel > 0, % just backtrack if last decision level is 1 or 0 | |
508 | possibly_bt_from_smt_solution(SolverEnv,StateMutable, SatVarName, Pol), | |
509 | ( learn_idl_core(StateMutable, SolverEnv, SatVarName, Pol) | |
510 | -> true | |
511 | ; debug_format_sat("theory conflict on level ~w", [CurLevel]), | |
512 | get_conflict_clause_for_theory_conflict(SolverEnv, SatVarName, Pol, SolverEnv, TConflictClause), | |
513 | % explicitly set the polarity which failed to be assigned above in line 414 for conflict analysis (possibly part of the unsat core) | |
514 | set_polarity_of_var_explicitly(SatVarName, Pol, TConflictClause, ConflictClause), | |
515 | ( ConflictClause = [SStackInfo-CPol-SingletonVar-SingletonName] | |
516 | -> % singleton theory conflict: backjump to level 0 | |
517 | debug_format_sat("backjump to level 0 after finding singleton theory conflict for SAT variable ~w", [SingletonName]), | |
518 | ( ground(SingletonVar) | |
519 | -> negate_polarity(SingletonVar, NSingletonPol) | |
520 | ; % static WD PO theory contradiction | |
521 | debug_format_sat("Force static theory conflict of WD condition to be false for ~w.", [SingletonName]), | |
522 | NSingletonPol = CPol | |
523 | ), | |
524 | BjClause = [SStackInfo-NSingletonPol-SingletonVar-SingletonName], | |
525 | debug_format_sat("learn unit clause ~w", [strip-BjClause]), | |
526 | BjLevel = 0, | |
527 | compute_lbd_score(BjClause, LbdScore), | |
528 | count_found_conflict(NewTotal, _, _), | |
529 | asserta(backjump_clause(BjLevel, BjClause, LbdScore, [SingletonName], [], NewTotal)), | |
530 | asserta(backjump_level(BjLevel)) | |
531 | ; get_maximum_decision_level(ConflictClause, ConflictLevel), | |
532 | % it can be the case that ProB first recognizes unsatisfiable after grounding waitflags; the last decision level is then not necessarily the conflict level | |
533 | debug_format_sat("theory conflict on level ~w after unsat core computation", [ConflictLevel]), | |
534 | get_full_state(StateMutable, current_stack_size, StackSize), | |
535 | compute_and_assert_backjump_clause_get_level(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause, _BjLevel) | |
536 | ) | |
537 | ), | |
538 | fail | |
539 | ). | |
540 | set_watch(SolverEnv, StateMutable, OriginalClause, [StackInfo2-Pol2-Var2-Name2|Triples], Var1, Pol1, Name1, StackInfo1):- | |
541 | \+ backjump_level(_), | |
542 | watch(SolverEnv, StateMutable, OriginalClause, StackInfo1, Var1, Pol1, Name1, StackInfo2, Var2, Pol2, Name2, Triples). | |
543 | ||
544 | :- block watch(?, ?, ?, ?, -, ?, ?, ?, -, ?, ?, ?). | |
545 | watch(SolverEnv, StateMutable, OriginalClause, StackInfo1, Var1, Pol1, Name1, StackInfo2, Var2, Pol2, Name2, Triples) :- | |
546 | ( nonvar(Var1) | |
547 | ? | -> update_watch(SolverEnv, StateMutable, OriginalClause, StackInfo1, Var1, Pol1, Name1, StackInfo2, Var2, Pol2, Name2, Triples) |
548 | ? | ; update_watch(SolverEnv, StateMutable, OriginalClause, StackInfo2, Var2, Pol2, Name2, StackInfo1, Var1, Pol1, Name1, Triples) |
549 | ). | |
550 | ||
551 | update_watch(SolverEnv, StateMutable, OriginalClause, _, Var1, Pol1, Name1, StackInfo2, Var2, Pol2, Name2, Triples) :- | |
552 | ( Var1 == Pol1 | |
553 | ? | -> checkout_sat_variable(Name1, OriginalClause) |
554 | ? | ; set_watch(SolverEnv, StateMutable, OriginalClause, Triples, Var2, Pol2, Name2, StackInfo2) |
555 | ). | |
556 | ||
557 | retract_once(Assertion) :- | |
558 | retract(Assertion), | |
559 | !. | |
560 | ||
561 | severe_error_occurred :- | |
562 | error_occurred_in_error_scope, | |
563 | check_error_occured(ErrorName, _), | |
564 | ErrorName \= warning(_), | |
565 | ErrorName \== clpfd_overflow, | |
566 | ErrorName \== smt_symmetry_breaking, | |
567 | ErrorName \== well_definedness_error, | |
568 | ErrorName \== smt_solvers_interface, | |
569 | ErrorName \== internal_error(smt_solvers_interface). | |
570 | ||
571 | %% is_backjumping. | |
572 | is_backjumping :- | |
573 | backjump_level(_). | |
574 | ||
575 | assert_update_pending_theory_propagation(SatVarName, Pol) :- | |
576 | retract(pending_theory_prop(SatVarName,_)), | |
577 | !, | |
578 | asserta(pending_theory_prop(SatVarName,Pol)). | |
579 | assert_update_pending_theory_propagation(SatVarName, Pol) :- | |
580 | asserta(pending_theory_prop(SatVarName,Pol)). | |
581 | ||
582 | % We use a time limit in b_interpreter:b_convert_bool_timeout/7 which is observed here. | |
583 | % It can be the case that ProB/CLP(FD) exceeds the predefined global time limit | |
584 | % when assigning a SAT variable in the deterministic propagation phase (b_convert_bool). | |
585 | % Simply setting a time limit on the SAT variable's unification in the SAT solver is not possible | |
586 | % since CDCL etc. would also be affected by this time limit due to coroutines. | |
587 | :- block log_det_theory_timeout(-). | |
588 | log_det_theory_timeout(TORes) :- | |
589 | ( TORes == time_out | |
590 | -> asserta(assignment_timeout_occurred) | |
591 | ; true | |
592 | ). | |
593 | ||
594 | %% log_theory_propagation_sat_stack(+StateMutable, +SatVarName, +SatPrologVar, +StackInfo). | |
595 | log_theory_propagation_sat_stack(StateMutable, SatVarName, SatPrologVar, StackInfo) :- | |
596 | get_full_state(StateMutable, cur_level, CurLevel), | |
597 | log_theory_propagation, | |
598 | !, | |
599 | debug_format_sat("Theory propagation of ~w with polarity ~w", [SatVarName,SatPrologVar]), | |
600 | ( SatPrologVar == pred_true -> Pol = pred_true; Pol = pred_false), | |
601 | assert_update_pending_theory_propagation(SatVarName, Pol), | |
602 | % explanation (OriginalClause) is computed lazily for conflict analysis if necessary, see explain_theory_propagation/5 | |
603 | get_next_assignment_count_on_level(ACount), | |
604 | StackInfo = (theory,(CurLevel,ACount),Pol,_), | |
605 | bt_log_sat_stack(StateMutable, SatVarName, Pol). | |
606 | ||
607 | %% learn_idl_core(+StateMutable, +SolverEnv, +LastSatVarName, +FailedPol). | |
608 | learn_idl_core(StateMutable, SolverEnv, LastSatVarName, FailedPol) :- | |
609 | retract(idl_unsat_core(Core)), | |
610 | remove_idl_unsat_core, | |
611 | !, | |
612 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
613 | get_conflict_clause_from_unsat_core(Core, SolverEnv, TConflictClause), | |
614 | % explicitly assign the polarity which was undone due to the conflict | |
615 | set_polarity_of_var_explicitly(LastSatVarName, FailedPol, TConflictClause, TTConflictClause), | |
616 | set_variable_references_in_clause(PlVars, TTConflictClause, ConflictClause), | |
617 | get_full_state(StateMutable, current_stack_size, StackSize), | |
618 | get_full_state(StateMutable, cur_level, CurLevel), | |
619 | compute_and_assert_backjump_clause(SolverEnv, StateMutable, StackSize, CurLevel, ConflictClause). | |
620 | ||
621 | save_phase(SatVarName, Pol) :- | |
622 | (retract(saved_phase(SatVarName, _)), !; true), | |
623 | asserta(saved_phase(SatVarName, Pol)). | |
624 | ||
625 | % Log variable assignments. | |
626 | % Effect is undone when backtracking. Cache phase when backtracking and unassigning a variable. | |
627 | bt_log_sat_stack(StateMutable, SatVarName, Pol) :- | |
628 | increase_stack_size(StateMutable), | |
629 | ( true | |
630 | ; save_phase(SatVarName, Pol), | |
631 | fail | |
632 | ). | |
633 | ||
634 | increase_stack_size(StateMutable) :- | |
635 | get_full_state(StateMutable, current_stack_size, Old), | |
636 | New is Old + 1, !, | |
637 | update_full_state(StateMutable, current_stack_size, New). | |
638 | ||
639 | %% possibly_bt_from_smt_solution(+SolverEnv,+StateMutable, +SatVarName, +Pol). | |
640 | % Backtracking from an SMT solution which should not be handled as a theory conflict. | |
641 | possibly_bt_from_smt_solution(_SolverEnv,StateMutable, _SatVarName, _Pol) :- | |
642 | retract(bt_from_smt_solution), | |
643 | !, | |
644 | %( ground(SatVarName) | |
645 | %-> get_complete_theory_lemma_fixed_binding(SolverEnv, SatVarName, Pol, TheoryLemmaClause) | |
646 | %; get_complete_theory_lemma(SolverEnv, TheoryLemmaClause) | |
647 | %), | |
648 | % backjump to the last decision level without computing a conflict clause | |
649 | % but excluding the last SAT solution when backtracking after finding an SMT solution | |
650 | get_last_decision_level(StateMutable, Level), | |
651 | %asserta(exclude_sat_solution_clause(TheoryLemmaClause)), % not used currently | |
652 | asserta(backjump_level(Level)), | |
653 | fail. | |
654 | possibly_bt_from_smt_solution(_,_, _, _). | |
655 | ||
656 | % Just wrap with negation but prevent double negation. | |
657 | negate_smt_formula(b(negation(Smt),pred,_), NegSmt) :- | |
658 | !, | |
659 | NegSmt = Smt. | |
660 | negate_smt_formula(Smt, b(negation(Smt),pred,[])). | |
661 | ||
662 | % iterate over all Prolog variables to find the propagated literals: usually a stack is used but we store stack infos besides each | |
663 | % variable in the clauses; explanation of theory propagations is rare and maintaining a genuine stack is more expensive | |
664 | get_propagated_sat_vars([], _, []). | |
665 | get_propagated_sat_vars([SatVarName-(_-_-_-(_,(Level,_ACount),Pol,_))|T], TheoryPropLevel, SatVarNameTuples) :- | |
666 | ground(Level), | |
667 | Level < TheoryPropLevel, | |
668 | !, | |
669 | SatVarNameTuples = [(SatVarName-Pol)|NT], | |
670 | get_propagated_sat_vars(T, TheoryPropLevel, NT). | |
671 | get_propagated_sat_vars([_|T], TheoryPropLevel, NT) :- | |
672 | get_propagated_sat_vars(T, TheoryPropLevel, NT). | |
673 | ||
674 | %% explain_theory_propagation(+SolverEnv, +TheoryPropSatVar, +TheoryPropLevel, +TheoryPropPol, -ExplainingClause). | |
675 | explain_theory_propagation(SolverEnv, TheoryPropSatVar, _, _, ExplainingClause) :- | |
676 | minimize_theory_explanations(false), | |
677 | !, | |
678 | debug_format_sat("Use complete lemma for theory explanation of ~w", [TheoryPropSatVar]), | |
679 | get_from_solver_env(SolverEnv, sat_bindings, SatBindings), | |
680 | get_clause_from_ground_bindings(SatBindings, _, _, [], TExplainingClause), | |
681 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
682 | set_variable_references_in_clause(PlVars, TExplainingClause, ExplainingClause), | |
683 | debug_format_sat("finished explanation.", []). | |
684 | explain_theory_propagation(SolverEnv, TheoryPropSatVar, TheoryPropLevel, TheoryPropPol, ExplainingClause) :- | |
685 | debug_format_sat("Explain theory propagation of ~w", [TheoryPropSatVar]), | |
686 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
687 | mutdict_items(PlVars, PlVarsList), | |
688 | get_propagated_sat_vars(PlVarsList, TheoryPropLevel, SatVarNameTuples), | |
689 | get_from_solver_env(SolverEnv, sat_vars, SatVars), | |
690 | get_smt_formula_from_vars_for_sat_pol(SatVars, TheoryPropSatVar, TheoryPropPol, SmtFormula), | |
691 | negate_smt_formula(SmtFormula, NegSmt), | |
692 | debug_format_sat("Compute unsat core for explanation: ", [], NegSmt), | |
693 | get_explanation_candidate_formula(SatVars, SatVarNameTuples, CandidateFormula), | |
694 | ( SatVarNameTuples = [_] | |
695 | -> safe_create_texpr(conjunct(CandidateFormula,NegSmt), pred, [], UnsatCore) | |
696 | ; temporary_set_preference(time_out, 25, Change1), | |
697 | temporary_set_preference(unsat_core_algorithm, linear, Change2), | |
698 | call_cleanup(unsat_core_with_fixed_conjuncts(CandidateFormula, NegSmt, TTUnsatCore), | |
699 | (reset_temporary_preference(unsat_core_algorithm, Change2), | |
700 | reset_temporary_preference(time_out, Change1))), | |
701 | safe_create_texpr(conjunct(TTUnsatCore,NegSmt), pred, [], TUnsatCore), | |
702 | ( strip_pos_keep_toplevel_conj(TUnsatCore, UnsatCore) | |
703 | -> true | |
704 | ; add_error_fail(strip_pos_keep_toplevel_conj, 'Removing WD POs for CDCL(T) failed for explaining theory propagation.', [unsat_core_with_wd:TUnsatCore]) | |
705 | ) | |
706 | ), | |
707 | get_from_solver_env(SolverEnv, t2b_env, T2BEnv), | |
708 | debug_format_sat("Computed unsat core for explanation: ", [], UnsatCore), | |
709 | ( | |
710 | ( | |
711 | predicate_to_sat(only_reuse, [], SatVars, T2BEnv, UnsatCore, _NewEnv, _, UnsatCoreSat, _NewSatVars), | |
712 | sat_conj_negate_to_clause(UnsatCoreSat, TExplainingClause) | |
713 | ) | |
714 | -> true | |
715 | ; add_error_fail(sat_conj_negate_to_clause, 'Explaining theory propagation failed: Explanation cannot be transformed to SAT.', [unsat_core:UnsatCore]) | |
716 | ), | |
717 | debug_format_sat("finished explanation.", []), | |
718 | set_variable_references_in_clause(PlVars, TExplainingClause, TTExplainingClause), | |
719 | sort(TTExplainingClause, ExplainingClause). | |
720 | ||
721 | get_explanation_candidate_formula(SatVars, [SatVarName-Pol|T], CandidateFormula) :- | |
722 | get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula), | |
723 | !, | |
724 | get_explanation_candidate_formula_acc(SatVars, T, SmtFormula, CandidateFormula). | |
725 | get_explanation_candidate_formula(SatVars, [_|T], CandidateFormula) :- | |
726 | % can be artificial SAT variable introduced by cnf rewriting | |
727 | get_explanation_candidate_formula(SatVars, T, CandidateFormula). | |
728 | ||
729 | get_explanation_candidate_formula_acc(_, [], Acc, Acc). | |
730 | get_explanation_candidate_formula_acc(SatVars, [SatVarName-Pol|T], Acc, CandidateFormula) :- | |
731 | get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula), | |
732 | !, | |
733 | safe_create_texpr(conjunct(SmtFormula,Acc), pred, [], NAcc), | |
734 | get_explanation_candidate_formula_acc(SatVars, T, NAcc, CandidateFormula). | |
735 | get_explanation_candidate_formula_acc(SatVars, [_|T], Acc, CandidateFormula) :- | |
736 | get_explanation_candidate_formula_acc(SatVars, T, Acc, CandidateFormula). | |
737 | ||
738 | get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula) :- | |
739 | memberchk(b(identifier(SatVarName),_,Info), SatVars), | |
740 | member(smt_formula(TSmtFormula), Info), | |
741 | get_smt_formula_for_sat_pol(TSmtFormula, Pol, SmtFormula). | |
742 | ||
743 | get_smt_formula_for_sat_pol(TSmtFormula, Pol, SmtFormula) :- | |
744 | ( Pol == pred_true | |
745 | -> SmtFormula = TSmtFormula | |
746 | ; TSmtFormula = b(negation(SmtFormula),pred,[]) | |
747 | -> true | |
748 | ; TSmtFormula = b(_,_,Info), | |
749 | SmtFormula = b(negation(TSmtFormula),pred,Info) | |
750 | ). | |
751 | ||
752 | %% get_sat_var_with_max_heuristic(-SatVarName, -MaxScore). | |
753 | get_sat_var_with_max_heuristic(SatVarName, MaxScore) :- | |
754 | %\+ fibonacci_heap:is_empty, | |
755 | ( print_logs(true) | |
756 | -> fibonacci_heap:get_max_priority(MaxScore) | |
757 | ; MaxScore = -1 | |
758 | ), | |
759 | ? | fibonacci_heap:get_and_remove_max_value_bt(SatVarName). |
760 | ||
761 | retract_if_exists(Assertion) :- | |
762 | ( cdclt_sat_solver:Assertion | |
763 | -> retract(cdclt_sat_solver:Assertion) | |
764 | ; true | |
765 | ). | |
766 | ||
767 | % Periodically decay heuristic scores for VSIDS heuristic. | |
768 | % Not undone when backtracking. | |
769 | possibly_decay_heuristic_values :- | |
770 | decision_heuristic(vsids), | |
771 | conflict_stats(total(AC), _, _), | |
772 | AC \== 0, | |
773 | vsids_decay_frequency(I), | |
774 | C is AC mod I, | |
775 | C == 0, | |
776 | debug_format_sat("~nDecay heuristic scores", []), | |
777 | !, | |
778 | vsids_decay_value(Val), | |
779 | decay_heuristic_values(Val). | |
780 | possibly_decay_heuristic_values. | |
781 | ||
782 | %% decay_heuristic_values(+DecayValue). | |
783 | % Not undone when backtracking. | |
784 | decay_heuristic_values(DecayValue) :- | |
785 | Decay is (1/DecayValue), | |
786 | fibonacci_heap:mult_priority_of_all(Decay). | |
787 | ||
788 | %% init_decision_heuristic(+StateMutable, +VarsFromBinaryClauses, +Clauses). | |
789 | % Each variable is initially assigned the number of its occurrences in all clauses as its score. | |
790 | % Variable scores are not split for polarities. | |
791 | init_decision_heuristic(StateMutable, VarsFromBinaryClauses, Clauses) :- | |
792 | count_var_occurrences_in_clauses(Clauses, VarScoreTuples), | |
793 | binary_boost_factor(BoostFactor), | |
794 | ? | add_heuristic_tuples(StateMutable, BoostFactor, VarsFromBinaryClauses, VarScoreTuples). |
795 | ||
796 | add_heuristic_tuples(_, _, _, []). | |
797 | add_heuristic_tuples(StateMutable, BoostFactor, VarsFromBinaryClauses, [SatVarName-Score|T]) :- | |
798 | ? | ( select(SatVarName, VarsFromBinaryClauses, TVarsFromBinaryClauses) |
799 | -> NScore is Score * BoostFactor | |
800 | ; NScore = Score, | |
801 | TVarsFromBinaryClauses = VarsFromBinaryClauses | |
802 | ), | |
803 | fibonacci_heap:push(NScore, SatVarName), | |
804 | ? | add_heuristic_tuples(StateMutable, BoostFactor, TVarsFromBinaryClauses, T). |
805 | ||
806 | count_var_occurrences_in_clauses(Clauses, DictItems) :- | |
807 | new_mutdict(Dict), | |
808 | ? | count_var_occurrences_dict(Dict, Clauses), !, |
809 | mutdict_items(Dict, DictItems), !. | |
810 | ||
811 | count_var_occurrences_dict(_, []). | |
812 | count_var_occurrences_dict(Dict, [Clause|T]) :- | |
813 | ? | count_var_occurrences_from_clause_dict(Dict, Clause), |
814 | ? | count_var_occurrences_dict(Dict, T). |
815 | ||
816 | count_var_occurrences_from_clause_dict(_, []). | |
817 | count_var_occurrences_from_clause_dict(Dict, [_-_-Pol-SatVarName|T]) :- | |
818 | var(Pol), % skip variables that are already propagated by deterministic unit propagation | |
819 | !, | |
820 | ( mutdict_get(Dict, SatVarName, Score) | |
821 | -> Score1 is Score + 1, | |
822 | mutdict_update(Dict, SatVarName, _, Score1) | |
823 | ; mutdict_put(Dict, SatVarName, 1) | |
824 | ), | |
825 | ? | count_var_occurrences_from_clause_dict(Dict, T). |
826 | count_var_occurrences_from_clause_dict(Dict, [_|T]) :- | |
827 | count_var_occurrences_from_clause_dict(Dict, T). | |
828 | ||
829 | update_heuristic_scores_for_vars(UsedVars, AC) :- | |
830 | decision_heuristic(Type), | |
831 | ? | update_heuristic_scores(AC, Type, UsedVars). |
832 | ||
833 | %% update_heuristic_scores(+AmountOfConflitsAtLevel, +Type, +SatVarNames). | |
834 | % Type is either vsids, evsids, vmtf or acids. | |
835 | % SatVarNames are the variable names occurring in learned clauses. | |
836 | update_heuristic_scores(_, _, []). | |
837 | update_heuristic_scores(TotalConflicts, Type, [SatVarName|T]) :- | |
838 | ( fibonacci_heap:get_priority_of_silent_fail(SatVarName, OldScore) | |
839 | -> bump_heuristic_score_for_type(Type, TotalConflicts, OldScore, NewScore), | |
840 | fibonacci_heap:update(SatVarName, NewScore), | |
841 | update_heuristic_scores(TotalConflicts, Type, T) | |
842 | ; % SAT variable has already been propagated. | |
843 | % For instance, this is the case when learning a clause on a level greater zero while | |
844 | % a specific SAT variable of this clause has already been propagated on a previous level. | |
845 | ? | update_heuristic_scores(TotalConflicts, Type, T) |
846 | ). | |
847 | ||
848 | % v_s + 1 | |
849 | bump_heuristic_score_for_type(vsids, _, OldScore, NewScore) :- | |
850 | NewScore is OldScore + 1. | |
851 | % k | |
852 | bump_heuristic_score_for_type(vmtf, TotalConflicts, _, NewScore) :- | |
853 | NewScore is TotalConflicts. | |
854 | % (v_s + k) / 2 | |
855 | bump_heuristic_score_for_type(acids, TotalConflicts, OldScore, NewScore) :- | |
856 | NewScore is (OldScore + TotalConflicts) / 2. | |
857 | % v_s + f^(-k), where f is evsids_f_value/1 and it is/was the k-th conflict when finding this clause via conflict analysis | |
858 | bump_heuristic_score_for_type(evsids, TotalConflicts, OldScore, NewScore) :- | |
859 | evsids_f_value(FVal), | |
860 | catch(NewScore is OldScore + FVal**(-TotalConflicts), error(evaluation_error(float_overflow),_), NewScore = 1.35743634973696E+308). | |
861 | ||
862 | % Literal Block Distance (LBD) as defined in "Predicting Learnt Clauses Quality in Modern SAT Solvers", | |
863 | % i.e., the amount of different decision levels in a clause. | |
864 | compute_lbd_score(BjClause, LbdScore) :- | |
865 | compute_lbd_score(BjClause, [], LbdScore). | |
866 | ||
867 | compute_lbd_score([], Acc, LbdScore) :- | |
868 | length(Acc, LbdScore). | |
869 | compute_lbd_score([(_,(Level,_),_,_)-_-_-_|T], Acc, LbdScore) :- | |
870 | !, | |
871 | ord_add_element(Acc, Level, NewAcc), | |
872 | compute_lbd_score(T, NewAcc, LbdScore). | |
873 | ||
874 | %% count_found_conflict(-NewTotal, -NewSinceRestart, -NewSinceReduction). | |
875 | count_found_conflict(Total1, SRes1, SRed1) :- | |
876 | log_conflict, | |
877 | retract(conflict_stats(total(Total), since_restart(SRes), since_reduction(SRed))), | |
878 | Total1 is Total + 1, | |
879 | SRes1 is SRes + 1, | |
880 | SRed1 is SRed + 1, | |
881 | asserta(conflict_stats(total(Total1), since_restart(SRes1), since_reduction(SRed1))). | |
882 | ||
883 | %% compute_and_assert_backjump_clause(+SolverEnv, +StateMutable, +StackSize, +ConflictClause). | |
884 | compute_and_assert_backjump_clause(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause) :- | |
885 | compute_and_assert_backjump_clause_get_level(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause, _). | |
886 | ||
887 | cnf_to_smt(BoolPred, Smt) :- | |
888 | BoolPred = b(Expr,_,_), | |
889 | ? | cnf_to_smt_e(Expr, Smt). |
890 | ||
891 | cnf_to_smt_e(falsity, b(falsity,pred,[])). | |
892 | cnf_to_smt_e(truth, b(truth,pred,[])). | |
893 | cnf_to_smt_e(conjunct(A,B), Smt) :- | |
894 | ? | cnf_to_smt(A, NA), |
895 | ? | cnf_to_smt(B, NB), |
896 | safe_create_texpr(conjunct(NA,NB), pred, [], Smt). | |
897 | cnf_to_smt_e(disjunct(A,B), Smt) :- | |
898 | ? | cnf_to_smt(A, NA), |
899 | ? | cnf_to_smt(B, NB), |
900 | safe_create_texpr(disjunct(NA,NB), pred, [], Smt). | |
901 | cnf_to_smt_e(equal(b(identifier(_),_,Info),b(BoolExpr,boolean,_)), Smt) :- | |
902 | ? | member(smt_formula(TSmt), Info), |
903 | ( BoolExpr == boolean_true | |
904 | -> Smt = TSmt | |
905 | ; safe_create_texpr(negation(TSmt), pred, [], Smt) | |
906 | ). | |
907 | ||
908 | /*cnf_to_smt([], _, Acc, SmtFromCnf) :- | |
909 | conjunct_predicates(Acc, SmtFromCnf). | |
910 | cnf_to_smt([Clause|T], PrologSatVarTriple, Acc, SmtFromCnf) :- | |
911 | clause_to_smt(PrologSatVarTriple, Clause, SmtClause), | |
912 | cnf_to_smt(T, PrologSatVarTriple, [SmtClause|Acc], SmtFromCnf).*/ | |
913 | ||
914 | %clause_to_smt(PlVars, Clause, SmtFormula) :- | |
915 | % clause_to_smt(PlVars, Clause, [], SmtFormula). | |
916 | % | |
917 | %clause_to_smt(_, [], Acc, SmtFormula) :- | |
918 | % disjunct_predicates(Acc, SmtFormula). | |
919 | %clause_to_smt(PlVars, [_-Pol-_-SatVarName|T], Acc, SmtClause) :- | |
920 | % mutdict_get(PlVars, SatVarName, _-SatVarName-TSmtFormula-_), | |
921 | % !, | |
922 | % get_smt_formula_for_sat_pol(TSmtFormula, Pol, SmtFormula), | |
923 | % clause_to_smt(PlVars, T, [SmtFormula|Acc], SmtClause). | |
924 | %clause_to_smt(_, [_-_-SatVarName|_], _, _) :- | |
925 | % add_error_fail(clause_to_smt, 'Unknown SAT variable.', [SatVarName]). | |
926 | ||
927 | bump_glue_levels([]). | |
928 | bump_glue_levels([_-_-_-SatVarName|T]) :- | |
929 | ( retract(glue_level(SatVarName, GlueLevel,AlreadyBumped)) | |
930 | -> NGlueLevel is GlueLevel + 1 | |
931 | ; NGlueLevel = 1, | |
932 | AlreadyBumped = false | |
933 | ), | |
934 | asserta(glue_level(SatVarName,NGlueLevel,AlreadyBumped)), | |
935 | bump_glue_levels(T). | |
936 | ||
937 | %% compute_and_assert_backjump_clause_get_level(+SolverEnv, +StateMutable, +StackSize, +ConflictLevel, +ConflictClause, -BjLevel). | |
938 | compute_and_assert_backjump_clause_get_level(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause, BjLevel) :- | |
939 | get_last_decision_level(StateMutable, _), | |
940 | %possibly_discard_learned_clauses, % TODO: adapt to new bj clause handling; yet, forgetting clauses has not shown to be beneficial so far | |
941 | debug_format_sat("~nConflict clause is ~w", [strip-ConflictClause]), | |
942 | debug_format_sat("~nStart CDCL..", []), | |
943 | ( ( | |
944 | get_backjump_clause_conflict_resolution(SolverEnv, StateMutable, ConflictLevel, ConflictClause, BjClause, BjLevel, BjSatVars, UsedVars), | |
945 | BjLevel \== -1 | |
946 | ) | |
947 | ; add_error_fail(compute_and_assert_backjump_clause_get_level, 'SMT solver\'s conflict resolution failed', []) | |
948 | ), | |
949 | debug_format_sat("done.", []), | |
950 | debug_format_sat("Backjump clause is ~w", [strip-BjClause]), | |
951 | debug_format_sat("Backjump level is ~w", [BjLevel]), | |
952 | compute_lbd_score(BjClause, LbdScore), | |
953 | debug_format_sat("LBD Score is ~w", [LbdScore]), | |
954 | ( ( glue_bumping(true), | |
955 | LbdScore == 2 | |
956 | ) | |
957 | -> retract(glue_clauses(Old)), | |
958 | New is Old + 1, | |
959 | asserta(glue_clauses(New)), | |
960 | bump_glue_levels(BjClause) | |
961 | ; true | |
962 | ), | |
963 | count_found_conflict(NewTotal, NewSinceRestart, _), | |
964 | asserta(backjump_clause(BjLevel, BjClause, LbdScore, BjSatVars, UsedVars, NewTotal)), | |
965 | asserta(backjump_level(BjLevel)), | |
966 | store_recent_stack_size(StackSize), | |
967 | count_learned_clause, | |
968 | possibly_decay_heuristic_values, | |
969 | ( \+ clear_lbd_values_or_fail(StateMutable), | |
970 | BjLevel \== 0 | |
971 | -> store_recent_lbd_score(LbdScore), | |
972 | update_total_lbd_sum(LbdScore), | |
973 | (random_restart(NewTotal, NewSinceRestart), !; true) | |
974 | ; true | |
975 | ), !. | |
976 | ||
977 | count_learned_clause :- | |
978 | retract(amount_learned_clauses(Old)), | |
979 | New is Old + 1, | |
980 | asserta(amount_learned_clauses(New)). | |
981 | ||
982 | %% store_recent_lbd_score(+LbdScore). | |
983 | % The stored list of recent LBDs is a difference list and we insert at the end of the list. | |
984 | % The first LBD is thus the oldest one and removed when exceeding the maximum size | |
985 | % defined by recent_lbd_threshold/1. | |
986 | store_recent_lbd_score(LbdScore) :- | |
987 | retract(recent_lbds_dl(Lbds-Diff, Amount)), | |
988 | glucose_restart_recent_lbds_threshold(Thresh), | |
989 | Diff = [LbdScore|NDiff], | |
990 | ( Amount < Thresh | |
991 | -> Amount1 is Amount + 1, | |
992 | asserta(recent_lbds_dl(Lbds-NDiff, Amount1)) | |
993 | ; Lbds = [_|RLbds], | |
994 | asserta(recent_lbds_dl(RLbds-NDiff, Amount)) | |
995 | ). | |
996 | ||
997 | store_recent_stack_size(StackSize) :- | |
998 | retract(recent_stack_sizes_dl(StackSizes-Diff, Amount)), | |
999 | glucose_restart_trail_threshold(Thresh), | |
1000 | Diff = [StackSize|NDiff], | |
1001 | ( Amount < Thresh | |
1002 | -> Amount1 is Amount + 1, | |
1003 | asserta(recent_stack_sizes_dl(StackSizes-NDiff, Amount1)) | |
1004 | ; StackSizes = [_|RStackSizes], | |
1005 | asserta(recent_stack_sizes_dl(RStackSizes-NDiff, Amount)) | |
1006 | ). | |
1007 | ||
1008 | %% update_total_lbd_sum(+LbdScore). | |
1009 | update_total_lbd_sum(LbdScore) :- | |
1010 | retract(total_lbd_sum(Old)), | |
1011 | New is Old + LbdScore, | |
1012 | asserta(total_lbd_sum(New)). | |
1013 | ||
1014 | %% random_restart(+AmountOfConflicts, +AmountOfConflictsSinceRestart). | |
1015 | % "Randomly" restart after an amount of conflicts since the last restart. | |
1016 | random_restart(_AC, ACR) :- | |
1017 | restart_policy(luby), | |
1018 | random_luby_restart(ACR), !. | |
1019 | random_restart(AC, _ACR) :- | |
1020 | restart_policy(glucose), | |
1021 | random_glucose_restart(AC), !. | |
1022 | ||
1023 | do_random_restart :- | |
1024 | log_restart, | |
1025 | retract(restarts(OldR)), | |
1026 | NewR is OldR + 1, | |
1027 | asserta(restarts(NewR)), | |
1028 | retract(backjump_level(_)), | |
1029 | asserta(backjump_level(0)), | |
1030 | retract(conflict_stats(total(Total), _, since_reduction(SRed))), | |
1031 | asserta(conflict_stats(total(Total), since_restart(0), since_reduction(SRed))), | |
1032 | asserta_once(is_restart), | |
1033 | debug_format_sat("~nRandom restart", []). | |
1034 | ||
1035 | %% random_glucose_restart(+AmountOfConflicts). | |
1036 | % Restart search if recent_lbds_dl/2 contains exactly glucose_restart_recent_lbds_threshold/1 amount | |
1037 | % of most recent LBDs and RecentAvg * Proportion > TotalAvg is satisfied, i.e., the recently learned clauses' | |
1038 | % LBDs got too large. | |
1039 | random_glucose_restart(AC) :- | |
1040 | total_lbd_sum(TotalLbdSum), | |
1041 | TotalAvg is TotalLbdSum / AC, | |
1042 | recent_lbds_dl(RLbds-[], LbdAmount), | |
1043 | glucose_restart_recent_lbds_threshold(LbdThresh), | |
1044 | LbdAmount == LbdThresh, % queue of recent LBDs is full | |
1045 | sumlist(RLbds, RSum), | |
1046 | RecentAvg is RSum / LbdAmount, | |
1047 | glucose_restart_margin_ratio(Proportion), | |
1048 | debug_format_sat("~nTotalAvg: ~w~nRecentAvg: ~w", [TotalAvg,RecentAvg]), | |
1049 | ( RecentAvg * Proportion > TotalAvg | |
1050 | -> do_random_restart, | |
1051 | clear_recent_lbds_state | |
1052 | ; true | |
1053 | ). | |
1054 | ||
1055 | % Favor SAT instances too by possibly clearing the recent LBD queue. | |
1056 | % Assumption: The queue of recent LBDs is full. | |
1057 | clear_lbd_values_or_fail(StateMutable) :- | |
1058 | glucose_restart_trail_threshold(TrailThresh), | |
1059 | glucose_restart_stack_avg_factor(StackSizeFactor), | |
1060 | recent_stack_sizes_dl(StackSizes-[], AmountStackSizes), | |
1061 | AmountStackSizes == TrailThresh, % queue of recent stack sizes on conflict is full | |
1062 | get_full_state(StateMutable, current_stack_size, StackSize), | |
1063 | sumlist(StackSizes, SSum), | |
1064 | StackSizesAvg is SSum / AmountStackSizes, | |
1065 | StackSize > StackSizeFactor * StackSizesAvg, | |
1066 | clear_recent_lbds_state. | |
1067 | ||
1068 | clear_recent_lbds_state :- | |
1069 | retract(recent_lbds_dl(_, _)), | |
1070 | asserta(recent_lbds_dl(Diff-Diff, 0)). | |
1071 | ||
1072 | %% random_luby_restart(+AmountOfConflictsSinceRestart). | |
1073 | % The amount of conflicts when to restart is defined by the Luby sequence, | |
1074 | % i.e., 1,1,2,1,1,2,4,1,1,2,1,1,2,4,8,.. etc., (cf. "Optimal speedup of Las Vegas algorithms") | |
1075 | % using a unit length of 32 (see luby_counter/1). | |
1076 | random_luby_restart(ACR) :- | |
1077 | restart_policy(luby), | |
1078 | get_next_luby_value(Luby), | |
1079 | !, | |
1080 | ( ACR == Luby | |
1081 | -> retract_once(luby_counter(_)), | |
1082 | do_random_restart | |
1083 | ; true | |
1084 | ). | |
1085 | random_luby_restart(_) :- | |
1086 | add_error_fail(random_restart, 'No more values in predefined Luby sequence', []). | |
1087 | ||
1088 | get_next_luby_value(LubyValue) :- | |
1089 | luby_counter(Luby), | |
1090 | luby_restart_unit_length(UnitLength), | |
1091 | LubyValue is UnitLength * Luby, | |
1092 | !. | |
1093 | ||
1094 | %% get_sat_solution_exclusion_clauses(+PlVars, -ExclClausesNoRef). | |
1095 | % We exclude SAT solutions when backtracking from finding an SMT solution to find a different assignment. | |
1096 | /*get_sat_solution_exclusion_clauses(PlVars, ExclClausesNoRef) :- | |
1097 | findall(ExclClause, | |
1098 | (exclude_sat_solution_clause(TExclClause), set_variable_references_in_clause(PlVars, TExclClause, ExclClause)), | |
1099 | ExclClausesNoRef), !.*/ | |
1100 | ||
1101 | %% set_variable_references_in_clauses(+PlVars, +Clauses, -RefClauses). | |
1102 | set_variable_references_in_clauses(_, [], []). | |
1103 | set_variable_references_in_clauses(PlVars, [Clause|T], [RefClause|NT]) :- | |
1104 | set_variable_references_in_clause(PlVars, Clause, RefClause), | |
1105 | set_variable_references_in_clauses(PlVars, T, NT). | |
1106 | ||
1107 | %% set_variable_references_in_clause(+PlVars, +Clause, -RefClauses). | |
1108 | % We need to set the correct variable references in a new learned clause | |
1109 | % to trigger co-routines etc. | |
1110 | set_variable_references_in_clause(_, [], Out) :- !, Out = []. | |
1111 | set_variable_references_in_clause(PlVars, [_-Pol-_-Name|T], [StackInfo-Pol-Var-Name|NT]) :- | |
1112 | mutdict_get(PlVars, Name, TVar-Name-_-TStackInfo), | |
1113 | !, | |
1114 | Var = TVar, | |
1115 | StackInfo = TStackInfo, | |
1116 | set_variable_references_in_clause(PlVars, T, NT). | |
1117 | set_variable_references_in_clause(_, [_-_-_-Name|_], _) :- | |
1118 | add_error_fail(set_variable_references_in_clause, 'Cannot set references: unknown SAT variable.', [Name]). | |
1119 | ||
1120 | get_from_solver_env(SolverEnv, Key, OutValue) :- | |
1121 | get_from_solver_env_ordered(Key, SolverEnv, Value), | |
1122 | !, | |
1123 | OutValue = Value. | |
1124 | get_from_solver_env(SolverEnv, Key, _) :- | |
1125 | add_error_fail(get_from_solver_env, | |
1126 | 'Wrong key or corrupt solver environment in CDCL(T) SAT solver', | |
1127 | [solver_env:SolverEnv,key:Key]). | |
1128 | ||
1129 | get_from_solver_env_ordered(sat_vars, [sat_vars:SatVars,_,_,_,_,_], SatVars). | |
1130 | get_from_solver_env_ordered(sat_varnames, [_,sat_varnames:SatVarNames,_,_,_,_], SatVarNames). | |
1131 | get_from_solver_env_ordered(sat_bindings, [_,_,sat_bindings:SatBindings,_,_,_], SatBindings). | |
1132 | get_from_solver_env_ordered(t2b_env, [_,_,_,t2b_env:Env,_,_], Env). | |
1133 | get_from_solver_env_ordered(pl_vars, [_,_,_,_,pl_vars:PlVars,_], PlVars). | |
1134 | get_from_solver_env_ordered(binary_clause_vars, [_,_,_,_,_,binary_clause_vars:VarsFromBinaryClauses], VarsFromBinaryClauses). | |
1135 | ||
1136 | bt_asserta(Assertion) :- | |
1137 | asserta(Assertion); (retract(Assertion), !, fail). | |
1138 | ||
1139 | bt_retract(Assertion) :- | |
1140 | ( retract(Assertion) | |
1141 | -> ( true | |
1142 | ; asserta(Assertion), | |
1143 | !, | |
1144 | fail | |
1145 | ) | |
1146 | ; fail | |
1147 | ). | |
1148 | ||
1149 | %% get_unsat_core_from_smt_formula(+FullFormula, +LastVarName, -UnsatCore). | |
1150 | % Assumption: unsat core computation only removes constraints and does not deduce new ones. | |
1151 | % Fails if +FullFormula is satisfiable. | |
1152 | get_unsat_core_from_smt_formula(FullFormula, LastVarName, UnsatCore) :- | |
1153 | debug_format_sat("Compute unsat core for: ", [], FullFormula), | |
1154 | preferences:temporary_set_preference(time_out, 25, Change), | |
1155 | ? | call_cleanup(time_out(unsat_chr_core_list_with_auto_time_limit(FullFormula, 30000, |
1156 | [auto_time_out_factor(180), % we add 80 % | |
1157 | ignore_if_sol_found, | |
1158 | inspect_quantifiers(false)], GlobalRes, CoreList), 30000, TimeoutResult), | |
1159 | reset_temporary_preference(time_out, Change)), | |
1160 | !, | |
1161 | ( GlobalRes = solution(_) | |
1162 | -> % the present theory conflict only occurs within the current state of ProB's waitflag store; there is at least one choice point | |
1163 | % in the theory solver which needs to be evaluated; we thus do not learn from this "spurious counterexample" but | |
1164 | % trigger chronological backtracking instead of backjumping | |
1165 | debug_format_sat("Spurious counterexample found. Skip backjumping and use chronological backtracking instead.", []), | |
1166 | fail | |
1167 | ; GlobalRes == time_out | |
1168 | -> % ignore core if global result is timeout | |
1169 | TUnsatCore = FullFormula | |
1170 | ; TimeoutResult == time_out | |
1171 | -> % don't waste too much time in unsat core computation | |
1172 | debug_format_sat("Canceled unsat core computation due to exceeding a timeout" ,[]), | |
1173 | TUnsatCore = FullFormula | |
1174 | ; ( CoreList == [] | |
1175 | -> add_error_fail(get_conflict_clause_for_theory_conflict, 'Conflict clause in SMT solving is not a conflict.', [LastVarName]) | |
1176 | ; conjunct_predicates(CoreList, TUnsatCore) | |
1177 | ) | |
1178 | ), | |
1179 | debug_format_sat("Computed unsat core with added WD POs: ", [], TUnsatCore), | |
1180 | ( strip_pos_keep_toplevel_conj(TUnsatCore, UnsatCore) | |
1181 | -> true | |
1182 | ; add_error_fail(strip_pos_keep_toplevel_conj, 'Removing WD POs for CDCL(T) failed.', [unsat_core_with_wd:TUnsatCore]) | |
1183 | ), | |
1184 | debug_format_sat("Computed unsat core: ", [], UnsatCore). | |
1185 | ||
1186 | %% get_conflict_clause_for_theory_conflict(+LastVarName, +LastVarValue, +SolverEnv, -ConflictClause). | |
1187 | % Translate current sat solution, which is a theory conflict, to the theory and compute | |
1188 | % the (minimum) unsat core. Return the negated theory conflict as a conflict clause. | |
1189 | % Note that an SMT formula passed to the theory solver is always a conjunction and | |
1190 | % thus the negated unsat core is a disjunction (clause). | |
1191 | get_conflict_clause_for_theory_conflict(SolverEnv, LastVarName, LastVarValue, SolverEnv, ConflictClause) :- | |
1192 | ( retract(idl_unsat_core(UnsatCore)) | |
1193 | -> true | |
1194 | ; get_from_solver_env(SolverEnv, sat_bindings, SatBindingsNoLast), | |
1195 | get_from_solver_env(SolverEnv, sat_vars, SatVars), | |
1196 | sat_to_predicate_from_solution(SatBindingsNoLast, SatVars, SmtFormulaNoLast), | |
1197 | findall(bind(PendingName,PendingPol), pending_theory_prop(PendingName,PendingPol), PendingTheoryProps), | |
1198 | sat_to_predicate_from_solution([bind(LastVarName,LastVarValue)|PendingTheoryProps], SatVars, FixedConj), | |
1199 | safe_create_texpr(conjunct(FixedConj,SmtFormulaNoLast), pred, [] , FullFormula), | |
1200 | get_unsat_core_from_smt_formula(FullFormula, LastVarName, UnsatCore) | |
1201 | ), !, | |
1202 | find_typed_identifier_uses(UnsatCore, [], UsedIds), | |
1203 | ( list_contains_unfixed_deferred_set_id(UsedIds) | |
1204 | -> asserta(unfixed_deferred_set_error) | |
1205 | ; true | |
1206 | ), | |
1207 | get_conflict_clause_from_unsat_core(UnsatCore, SolverEnv, TConflictClause), | |
1208 | sort(TConflictClause, TTConflictClause), % there can be duplicates due to added top-level WD POs; important to remove | |
1209 | ( TTConflictClause = [_] | |
1210 | -> % currently undiscovered static theory contradiction; SAT variable might not be propagated yet if added WD PO | |
1211 | ConflictClause = TTConflictClause | |
1212 | ; % remove not propagated top-level WD POs; we enforce WD POs in the theory solver but it can | |
1213 | % be the case that a theory conflict occurs before the WD POs are propagated in the SAT solver | |
1214 | remove_not_propagated(TTConflictClause, LastVarName, ConflictClause) | |
1215 | ), | |
1216 | !. | |
1217 | ||
1218 | remove_not_propagated([], _, []). | |
1219 | remove_not_propagated([Pol-Var-Name|T], LastVarName, [Pol-Var-Name|NT]) :- | |
1220 | ( ground(Var) | |
1221 | ; Name == LastVarName | |
1222 | ), | |
1223 | !, | |
1224 | remove_not_propagated(T, LastVarName, NT). | |
1225 | remove_not_propagated([_-_-Name|T], LastVarName, NT) :- | |
1226 | debug_format_sat("Remove not propagated SAT variable ~w from conflict clause.", [Name]), | |
1227 | remove_not_propagated(T, LastVarName, NT). | |
1228 | ||
1229 | %% get_conflict_clause_from_unsat_core(+UnsatCore, +SolverEnv, -ConflictClause). | |
1230 | get_conflict_clause_from_unsat_core(UnsatCore, SolverEnv, ConflictClause) :- | |
1231 | get_from_solver_env(SolverEnv, sat_vars, SatVars), | |
1232 | get_from_solver_env(SolverEnv, t2b_env, T2BEnv), | |
1233 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
1234 | ? | predicate_to_sat(only_reuse, [], SatVars, T2BEnv, UnsatCore, _NewEnv, _, UnsatCoreSat, _NewSatVars), |
1235 | sat_conj_negate_to_clause(UnsatCoreSat, TConflictClause), | |
1236 | set_variable_references_in_clause(PlVars, TConflictClause, ConflictClause), | |
1237 | !. | |
1238 | get_conflict_clause_from_unsat_core(_, _, _) :- | |
1239 | add_error_fail(get_conflict_clause_from_unsat_core, 'Unsat core to conflict clause failed.', []). | |
1240 | ||
1241 | :- public get_complete_theory_lemma/2. % not used at the moment, for Spider | |
1242 | %% get_complete_theory_lemma(+SolverEnv, -TheoryLemmaClause) :- | |
1243 | % Return the complete unsatisfiable SMT formula as a conflict clause. | |
1244 | get_complete_theory_lemma(SolverEnv, TheoryLemmaClause) :- | |
1245 | get_complete_theory_lemma_fixed_binding(SolverEnv, _, _, TheoryLemmaClause). | |
1246 | ||
1247 | %% get_complete_theory_lemma_fixed_binding(+SolverEnv, +SatVarName, +SatVarPol, -TheoryLemmaClause). | |
1248 | % Enforce +SatVarName to have +SatVarPol binding. This is important for theory conflicts since the last | |
1249 | % binding has been undone when backtracking. This is not applied if both inputs are variables, e.g., for SAT conflicts. | |
1250 | get_complete_theory_lemma_fixed_binding(SolverEnv, SatVarName, SatVarPol, TheoryLemmaClause) :- | |
1251 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
1252 | get_from_solver_env(SolverEnv, sat_bindings, SatBindings), | |
1253 | get_clause_from_negated_ground_bindings(SatBindings, SatVarName, SatVarPol, TTheoryLemmaClause), | |
1254 | set_variable_references_in_clause(PlVars, TTheoryLemmaClause, TheoryLemmaClause), !. | |
1255 | ||
1256 | %% get_clause_from_negated_ground_bindings(+SatBindings, +FSatVarName, +FSatVarPol, -TheoryLemmaClause) :- | |
1257 | % FSatVarName: name of SAT variable whose binding should be set to +FSatVarPol | |
1258 | get_clause_from_negated_ground_bindings(SatBindings, FSatVarName, FSatVarPol, TheoryLemmaClause) :- | |
1259 | get_clause_from_negated_ground_bindings(SatBindings, FSatVarName, FSatVarPol, [], TheoryLemmaClause). | |
1260 | ||
1261 | get_clause_from_negated_ground_bindings([], _, _, Acc, Acc). | |
1262 | get_clause_from_negated_ground_bindings([bind(SatVarName,_)|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :- | |
1263 | % theory propagations during grounding are possibly undone in the stack if finding a contradiction during grounding waitflags | |
1264 | % we restore such pending theory propagations here | |
1265 | pending_theory_prop(SatVarName, SatVarPol), | |
1266 | !, | |
1267 | negate_polarity(SatVarPol, NegPol), | |
1268 | get_clause_from_negated_ground_bindings(T, FSatVarName, FSatVarPol, [_-NegPol-_-SatVarName|Acc], TheoryLemmaClause). | |
1269 | get_clause_from_negated_ground_bindings([bind(SatVarName,_)|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :- | |
1270 | % set fixed polarity | |
1271 | SatVarName == FSatVarName, | |
1272 | !, | |
1273 | negate_polarity(FSatVarPol, NegPol), | |
1274 | get_clause_from_negated_ground_bindings(T, FSatVarName, FSatVarPol, [_-NegPol-_-SatVarName|Acc], TheoryLemmaClause). | |
1275 | get_clause_from_negated_ground_bindings([bind(SatVarName,Pol)|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :- | |
1276 | ground(Pol), | |
1277 | !, | |
1278 | negate_polarity(Pol, NegPol), | |
1279 | get_clause_from_negated_ground_bindings(T, FSatVarName, FSatVarPol, [_-NegPol-_-SatVarName|Acc], TheoryLemmaClause). | |
1280 | get_clause_from_negated_ground_bindings([_|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :- | |
1281 | get_clause_from_negated_ground_bindings(T, FSatVarName, FSatVarPol, Acc, TheoryLemmaClause). | |
1282 | ||
1283 | get_clause_from_ground_bindings([], _, _, Acc, Acc). | |
1284 | get_clause_from_ground_bindings([bind(SatVarName,_)|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :- | |
1285 | % theory propagations during grounding are possibly undone in the stack if finding a contradiction during grounding waitflags | |
1286 | % we restore such pending theory propagations here | |
1287 | pending_theory_prop(SatVarName, SatVarPol), | |
1288 | !, | |
1289 | get_clause_from_ground_bindings(T, FSatVarName, FSatVarPol, [_-SatVarPol-_-SatVarName|Acc], TheoryLemmaClause). | |
1290 | get_clause_from_ground_bindings([bind(SatVarName,Pol)|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :- | |
1291 | ground(Pol), | |
1292 | !, | |
1293 | get_clause_from_ground_bindings(T, FSatVarName, FSatVarPol, [_-Pol-_-SatVarName|Acc], TheoryLemmaClause). | |
1294 | get_clause_from_ground_bindings([_|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :- | |
1295 | get_clause_from_ground_bindings(T, FSatVarName, FSatVarPol, Acc, TheoryLemmaClause). | |
1296 | ||
1297 | % Fail if no decision has been made so far, i.e., the decision level is set to -1. | |
1298 | get_last_decision_level(StateMutable, Level) :- | |
1299 | get_full_state(StateMutable, cur_level, TLevel), | |
1300 | TLevel > 0, | |
1301 | !, | |
1302 | Level = TLevel. | |
1303 | ||
1304 | %negate_polarities([], []). | |
1305 | %negate_polarities([StackInfo-Pol-Var-Name|T], [StackInfo-NPol-Var-Name|NT]) :- | |
1306 | % negate_polarity(Pol, NPol), | |
1307 | % negate_polarities(T, NT). | |
1308 | ||
1309 | get_maximum_decision_level([(_,(Level,_),_,_)-_-_-_|T], ConflictLevel) :- | |
1310 | !, | |
1311 | get_maximum_decision_level(T, Level, ConflictLevel). | |
1312 | get_maximum_decision_level([_-_-_-Name|_], _) :- | |
1313 | add_error_fail(get_maximum_decision_level, 'The SAT variable has not been decided yet', [Name]). | |
1314 | ||
1315 | get_maximum_decision_level([], Acc, Acc). | |
1316 | get_maximum_decision_level([(_,(Level,_),_,_)-_-_-_|T], Acc, ConflictLevel) :- | |
1317 | !, | |
1318 | ( Level > Acc | |
1319 | -> NAcc = Level | |
1320 | ; NAcc = Acc | |
1321 | ), | |
1322 | get_maximum_decision_level(T, NAcc, ConflictLevel). | |
1323 | get_maximum_decision_level([_-_-_-Name|_], _, _) :- | |
1324 | add_error_fail(get_maximum_decision_level, 'The SAT variable has not been decided yet', [Name]). | |
1325 | ||
1326 | get_maximum_decision_level_other_than_current([_], _, _, BjLevel) :- | |
1327 | % zero if learning a unit clause | |
1328 | !, | |
1329 | BjLevel = 0. | |
1330 | get_maximum_decision_level_other_than_current(BjClause, BjLevelAcc, CurLevel, BjLevel) :- | |
1331 | get_maximum_decision_level_other_than_current_not_unit(BjClause, BjLevelAcc, CurLevel, BjLevel). | |
1332 | ||
1333 | get_maximum_decision_level_other_than_current_not_unit([], BjLevelAcc, _, BjLevelAcc). | |
1334 | get_maximum_decision_level_other_than_current_not_unit([(_,(Level,_),_,_)-_-_-_|T], BjLevelAcc, CurLevel, BjLevel) :- | |
1335 | ( (Level \== CurLevel, | |
1336 | Level > BjLevelAcc | |
1337 | ) | |
1338 | -> NBjLevelAcc = Level | |
1339 | ; NBjLevelAcc = BjLevelAcc | |
1340 | ), | |
1341 | get_maximum_decision_level_other_than_current_not_unit(T, NBjLevelAcc, CurLevel, BjLevel). | |
1342 | ||
1343 | %% get_antecedent_assignments(+SolverEnv, +ConflictDLevel, +SatVarName, +RPol, +RPropType, +ROriginalClause, -Antecedent). | |
1344 | get_antecedent_assignments(_, _, SatVarName, _, _, ROriginalClause, Antecedent) :- | |
1345 | is_list(ROriginalClause), | |
1346 | !, | |
1347 | select(_-_-_-SatVarName, ROriginalClause, TAntecedent), !, | |
1348 | Antecedent = TAntecedent. | |
1349 | get_antecedent_assignments(SolverEnv, ConflictDLevel, SatVarName, RPol, theory, ROriginalClause, Antecedent) :- | |
1350 | \+ is_list(ROriginalClause), | |
1351 | !, | |
1352 | explain_theory_propagation(SolverEnv, SatVarName, ConflictDLevel, RPol, OriginalClause), | |
1353 | ROriginalClause = OriginalClause, | |
1354 | select(_-_-_-SatVarName, OriginalClause, TAntecedent), !, | |
1355 | Antecedent = TAntecedent. | |
1356 | get_antecedent_assignments(_, _, SatVarName, _, _, _, _) :- | |
1357 | add_error_fail(get_antecedent_assignments, 'No antecedent assignments since variable has not been propagated.', SatVarName). | |
1358 | ||
1359 | %% join_assignments(+A1, +A2, +A2Full, -Joined). | |
1360 | join_assignments([], _, A, A). | |
1361 | join_assignments([StackInfo-Pol-Var-Name|T], A2, A3, Res) :- | |
1362 | ( select(_-_-_-Name, A2, A4) % removes dups assuming that A2 has no dups | |
1363 | -> join_assignments(T, A4, A3, Res) | |
1364 | ; join_assignments(T, A2, [StackInfo-Pol-Var-Name|A3], Res) | |
1365 | ). | |
1366 | ||
1367 | %% resolve(+SolverEnv, +TBjClause, +Resolver, +ROriginalClause, -NTBjClause). | |
1368 | % +Resolver is a SAT variable name to resolve next (i.e., expand its antecedent assignments). | |
1369 | resolve(SolverEnv, TBjClause, ConflictDLevel, Resolver, RPol, RPropType, ROriginalClause, NTBjClause) :- | |
1370 | get_antecedent_assignments(SolverEnv, ConflictDLevel, Resolver, RPol, RPropType, ROriginalClause, Antecedent), | |
1371 | join_assignments(Antecedent, TBjClause, TBjClause, TNTBjClause), % important to not have duplicates | |
1372 | select(_-_-_-Resolver, TNTBjClause, NTBjClause). | |
1373 | ||
1374 | add_used_vars_to_mutdict([], _). | |
1375 | add_used_vars_to_mutdict([_-_-_-SatVarName|T], VarNamesDict) :- | |
1376 | \+ mutdict_get(VarNamesDict, SatVarName, _), | |
1377 | !, | |
1378 | mutdict_put(VarNamesDict, SatVarName, SatVarName), | |
1379 | add_used_vars_to_mutdict(T, VarNamesDict). | |
1380 | add_used_vars_to_mutdict([_|T], VarNamesDict) :- | |
1381 | add_used_vars_to_mutdict(T, VarNamesDict). | |
1382 | ||
1383 | get_variables_used_in_cdcl(ResolvedSoFar, BjClause, UsedVars) :- | |
1384 | add_used_vars_to_mutdict(BjClause, ResolvedSoFar), | |
1385 | mutdict_keys(ResolvedSoFar, UsedVars). | |
1386 | ||
1387 | get_variable_names_in_clause([], []). | |
1388 | get_variable_names_in_clause([_-_-_-SatVarName|T], [SatVarName|NT]) :- | |
1389 | get_variable_names_in_clause(T, NT). | |
1390 | ||
1391 | % sort in reversed stack order | |
1392 | reversed_stack_sort((_,(DLevel1,ACount1),_,_)-_-_-_, (_,(DLevel2,ACount2),_,_)-_-_-_) :- | |
1393 | ground(DLevel1), ground(DLevel2), | |
1394 | ( DLevel1 > DLevel2 | |
1395 | -> true | |
1396 | ; DLevel1 == DLevel2 | |
1397 | -> ACount1 > ACount2 | |
1398 | ; fail | |
1399 | ). | |
1400 | ||
1401 | :- dynamic part_of_first_uip/1. | |
1402 | ||
1403 | % See https://cca.informatik.uni-freiburg.de/papers/SoerenssonBiere-SAT09.pdf | |
1404 | % Generate the 1-UIP clause. Mark all its literals. Remove those implied variables which have all their antecedent literals marked. | |
1405 | minimize_clause(SolverEnv, ConflictDLevel, BjClause, local, MinBjClause) :- | |
1406 | mark_literals(BjClause), | |
1407 | remove_where_all_antecedent_marked(BjClause, SolverEnv, ConflictDLevel, MinBjClause). | |
1408 | % Generate the 1-UIP clause. Mark its literals. Implied variables in 1-UIP clause are candidates for removal. | |
1409 | % Search implication graph. Start from antecedent literals of candidate. Stop at marked literals or decisions. | |
1410 | % If search always ends at marked literals, the candidate can be removed. | |
1411 | minimize_clause(SolverEnv, ConflictDLevel, BjClause, recursive, MinBjClause) :- | |
1412 | mark_literals(BjClause), | |
1413 | remove_recursively_stop_marked(BjClause, SolverEnv, ConflictDLevel, MinBjClause). | |
1414 | ||
1415 | remove_recursively_stop_marked([], _, _, []). | |
1416 | remove_recursively_stop_marked([(PropType,_,_,OriginalClause)-_-Pol-SatVarName|T], SolverEnv, ConflictDLevel, MinBjClause) :- | |
1417 | PropType \== branch, | |
1418 | get_antecedent_assignments(SolverEnv, ConflictDLevel, SatVarName, Pol, PropType, OriginalClause, Antecedent), | |
1419 | samsort(reversed_stack_sort, Antecedent, SAntecedent), % reverse assignment order | |
1420 | recursively_inspect_antecedent(SAntecedent, SolverEnv, ConflictDLevel), | |
1421 | !, | |
1422 | remove_recursively_stop_marked(T, SolverEnv, ConflictDLevel, MinBjClause). | |
1423 | remove_recursively_stop_marked([Lit|T], SolverEnv, ConflictDLevel, [Lit|NT]) :- | |
1424 | remove_recursively_stop_marked(T, SolverEnv, ConflictDLevel, NT). | |
1425 | ||
1426 | recursively_inspect_antecedent([], _, _). | |
1427 | recursively_inspect_antecedent([(PropType,_,_,OriginalClause)-_-Pol-SatVarName|T], SolverEnv, ConflictDLevel) :- | |
1428 | recursive_search_stops_at_marked_or_decision(PropType, OriginalClause, Pol, SatVarName, SolverEnv, ConflictDLevel), | |
1429 | recursively_inspect_antecedent(T, SolverEnv, ConflictDLevel). | |
1430 | ||
1431 | recursive_search_stops_at_marked_or_decision(_, _, _, SatVarName, _, _) :- | |
1432 | part_of_first_uip(SatVarName), | |
1433 | !. | |
1434 | recursive_search_stops_at_marked_or_decision(PropType, OriginalClause, Pol, SatVarName, SolverEnv, ConflictDLevel) :- | |
1435 | PropType \== branch, | |
1436 | get_antecedent_assignments(SolverEnv, ConflictDLevel, SatVarName, Pol, PropType, OriginalClause, Antecedent), | |
1437 | recursively_inspect_antecedent(Antecedent, SolverEnv, ConflictDLevel). | |
1438 | ||
1439 | all_literals_are_marked([]). | |
1440 | all_literals_are_marked([_-_-_-SatVarName|T]) :- | |
1441 | part_of_first_uip(SatVarName), | |
1442 | !, | |
1443 | all_literals_are_marked(T). | |
1444 | ||
1445 | remove_where_all_antecedent_marked([], _, _, []). | |
1446 | remove_where_all_antecedent_marked([(PropType,_,_,OriginalClause)-_-Pol-SatVarName|T], SolverEnv, ConflictDLevel, MinBjClause) :- | |
1447 | PropType == unit, | |
1448 | get_antecedent_assignments(SolverEnv, ConflictDLevel, SatVarName, Pol, PropType, OriginalClause, Antecedent), | |
1449 | all_literals_are_marked(Antecedent), | |
1450 | !, | |
1451 | remove_where_all_antecedent_marked(T, SolverEnv, ConflictDLevel, MinBjClause). | |
1452 | remove_where_all_antecedent_marked([Lit|T], SolverEnv, ConflictDLevel, [Lit|NT]) :- | |
1453 | remove_where_all_antecedent_marked(T, SolverEnv, ConflictDLevel, NT). | |
1454 | ||
1455 | mark_literals(Lits) :- | |
1456 | retractall(part_of_first_uip(_)), | |
1457 | mark_literals_state(Lits). | |
1458 | ||
1459 | mark_literals_state([]). | |
1460 | mark_literals_state([_-_-_-SatVarName|T]) :- | |
1461 | asserta(part_of_first_uip(SatVarName)), | |
1462 | mark_literals_state(T). | |
1463 | ||
1464 | %% get_backjump_clause_conflict_resolution(+SolverEnv, +StateMutable, +ConflictLevel, +ConflictClause, -BjClause, -BjLevel, -BjSatVars, -UsedVars). | |
1465 | % In the conflict graph each node corresponds to a variable assignment. | |
1466 | % The predecessors of node x are the antecedent assignments A^w(x) corresponding | |
1467 | % to the unit clause w (in its original form) that led to the propagation of x (logical implications). | |
1468 | % The directed edges from the nodes in A^w(x) to node x are all labeled with w. | |
1469 | % Nodes that have no predecessor correspond to decision/branching assignments | |
1470 | % (cf. GRASP: A Search Algorithm for Propositional Satisfiability, by Marques-Silva and Sakallah). | |
1471 | % As an improvement, we apply first UIP clause learning (cf. Efficient Conflict Driven Learning in a Boolean Satisfiability Solver, Zhang et al.). | |
1472 | % Compute the conflict graph for a conflicting unit-propagation of a variable and extract a backjump clause. | |
1473 | % -UsedVars are the SAT variables used during conflict analysis that are not part of the final bj clause (can be necessary for branching heuristic). | |
1474 | % -BjSatVars are the SAT variables in the final bj clause. | |
1475 | % Notes: | |
1476 | % - the variable references in the returned clause are not yet set | |
1477 | % - we do not create an actual graph but apply Boolean resolution | |
1478 | get_backjump_clause_conflict_resolution(SolverEnv, StateMutable, ConflictLevel, ConflictClause, BjClause, BjLevel, BjSatVars, UsedVars) :- | |
1479 | get_last_decision_level(StateMutable, _), | |
1480 | new_mutdict(ResolvedSoFar), | |
1481 | get_backjump_clause_and_level(SolverEnv, ConflictLevel, ResolvedSoFar, ConflictClause, BjClause, BjLevel, TUsedVars), | |
1482 | get_variable_names_in_clause(BjClause, BjSatVars), | |
1483 | subtract(TUsedVars, BjSatVars, UsedVars). | |
1484 | ||
1485 | %% get_backjump_clause_and_level(+SolverEnv, +ConflictDLevel, +ResolvedSoFar, +TBjClause, -BjClause, -BjLevel, -UsedVars). | |
1486 | get_backjump_clause_and_level(SolverEnv, ConflictDLevel, ResolvedSoFar, TBjClause, MinBjClause, BjLevel, UsedVars) :- | |
1487 | get_backjump_clause_and_level_sub(ConflictDLevel, 0, _, TBjClause, Resolver-RPol-RPropType-ROriginalClause, ThisLevelCount), | |
1488 | ( ThisLevelCount == 1 | |
1489 | -> % break, first UIP | |
1490 | BjClause = TBjClause, | |
1491 | clause_minimization(ClauseMinType), | |
1492 | ( ClauseMinType \== none | |
1493 | -> ( minimize_clause(SolverEnv, ConflictDLevel, BjClause, ClauseMinType, MinBjClause), ! | |
1494 | ; add_error_fail(minimize_clause, 'Clause minimization failed: ', [BjClause]) | |
1495 | ) | |
1496 | ; MinBjClause = BjClause | |
1497 | ), | |
1498 | get_maximum_decision_level_other_than_current(MinBjClause, 0, ConflictDLevel, BjLevel), | |
1499 | get_variables_used_in_cdcl(ResolvedSoFar, MinBjClause, UsedVars) | |
1500 | ; ground(Resolver), | |
1501 | resolve(SolverEnv, TBjClause, ConflictDLevel, Resolver, RPol, RPropType, ROriginalClause, NToExpand), | |
1502 | mutdict_put(ResolvedSoFar, Resolver, Resolver), | |
1503 | get_backjump_clause_and_level(SolverEnv, ConflictDLevel, ResolvedSoFar, NToExpand, MinBjClause, BjLevel, UsedVars) | |
1504 | ). | |
1505 | ||
1506 | get_backjump_clause_and_level_sub(_, ThisLevelCountAcc, ResolverAcc-_-RPol-RPropType-ROriginalClause, [], ResolverAcc-RPol-RPropType-ROriginalClause, ThisLevelCountAcc). | |
1507 | get_backjump_clause_and_level_sub(ConflictDLevel, ThisLevelCountAcc, ResolverAcc-RACount-RPol-RPropType-ROriginalClause, [(PropType,(Level,ACount),_,OriginalClause)-Pol-_-SatVarName|T], Resolver, ThisLevelCount) :- | |
1508 | ( Level == ConflictDLevel | |
1509 | -> NThisLevelCountAcc is ThisLevelCountAcc + 1 | |
1510 | ; NThisLevelCountAcc = ThisLevelCountAcc | |
1511 | ), | |
1512 | ( ( | |
1513 | Level == ConflictDLevel, | |
1514 | % unit or theory propagation | |
1515 | PropType \== branch, | |
1516 | % use last assigned literal to resolve next | |
1517 | ( var(ResolverAcc) | |
1518 | ; ACount > RACount | |
1519 | ) | |
1520 | ) | |
1521 | -> NResolverAcc = SatVarName-ACount-Pol-PropType-OriginalClause | |
1522 | ; NResolverAcc = ResolverAcc-RACount-RPol-RPropType-ROriginalClause | |
1523 | ), | |
1524 | get_backjump_clause_and_level_sub(ConflictDLevel, NThisLevelCountAcc, NResolverAcc, T, Resolver, ThisLevelCount). | |
1525 | ||
1526 | negate_polarity(pred_true, pred_false). | |
1527 | negate_polarity(pred_false, pred_true). | |
1528 | ||
1529 | retractall_once(Assertion) :- | |
1530 | retractall(cdclt_sat_solver:Assertion), | |
1531 | !. | |
1532 | ||
1533 | asserta_once(Assertion) :- | |
1534 | call(cdclt_sat_solver:Assertion), | |
1535 | !. | |
1536 | asserta_once(Assertion) :- | |
1537 | asserta(cdclt_sat_solver:Assertion). | |
1538 | ||
1539 | b_pred_or_bool_true(X) :- X == truth; X == boolean_true; X == value(pred_true). | |
1540 | %b_pred_or_bool_false(X) :- X == falsity; X == boolean_false; X == value(pred_false). | |
1541 | ||
1542 | sat_conj_negate_to_clause(Pred, Clause) :- | |
1543 | conjunction_to_list(Pred, List), | |
1544 | maplist(sat_equality_negate_to_literal, List, Clause). | |
1545 | ||
1546 | sat_equality_negate_to_literal(b(equal(ID,Pol),pred,_), _-NegPol-_-Name) :- | |
1547 | ID = b(identifier(Name),_,_), | |
1548 | Pol = b(Value,boolean,_), | |
1549 | ( b_pred_or_bool_true(Value) | |
1550 | -> NegPol = pred_false | |
1551 | ; NegPol = pred_true | |
1552 | ). | |
1553 | ||
1554 | %%%%% Solver State | |
1555 | create_solver_state(StateMutable) :- | |
1556 | State = [cur_level:0,current_stack_size:0], | |
1557 | create_mutable(solver_state(State), StateMutable). | |
1558 | ||
1559 | %% get_full_state(+StateMutable, +Key, -Datum). | |
1560 | % We assume an order of the SolverState to prevent using member. | |
1561 | get_full_state(StateMutable, Key, Datum) :- | |
1562 | get_mutable(solver_state(SolverState), StateMutable), | |
1563 | get_full_state_ordered(Key, SolverState, Datum), !. | |
1564 | ||
1565 | get_full_state_ordered(cur_level, [cur_level:CurLevel,_], CurLevel). | |
1566 | get_full_state_ordered(current_stack_size, [_,current_stack_size:Size], Size). | |
1567 | ||
1568 | %% delete_from_heuristic(+SatVarName). | |
1569 | delete_from_heuristic(SatVarName) :- | |
1570 | ( fibonacci_heap:elm_exists(SatVarName) | |
1571 | ? | -> fibonacci_heap:delete_elm_bt(SatVarName) |
1572 | ; % it can be the case that SatVarName has already been removed | |
1573 | % from the mutable due to coroutines etc.; succeed in this case | |
1574 | true | |
1575 | ). | |
1576 | ||
1577 | %% update_full_state(+StateMutable, +Key, +Datum). | |
1578 | % We assume an order of the SolverState to prevent using member. | |
1579 | update_full_state(StateMutable, Key, Datum) :- | |
1580 | get_mutable(solver_state(SolverState), StateMutable), | |
1581 | update_full_state_ordered(Key, Datum, SolverState, NewSolverState), !, | |
1582 | update_mutable(solver_state(NewSolverState), StateMutable). | |
1583 | ||
1584 | update_full_state_ordered(cur_level, NewDatum, [cur_level:_,B], [cur_level:NewDatum,B]). | |
1585 | update_full_state_ordered(current_stack_size, NewDatum, [A,current_stack_size:_], [A,current_stack_size:NewDatum]). | |
1586 | ||
1587 | %% Initialize the dynamic solver state for a specific solver. | |
1588 | init_dynamic_solver_state(SolverName) :- | |
1589 | fibonacci_heap:init, | |
1590 | clean_dynamic_solver_state, | |
1591 | clear_pending_theory_propagations, | |
1592 | asserta(solver_name(SolverName)), | |
1593 | asserta(restarts(0)), | |
1594 | asserta(glue_clauses(0)), | |
1595 | %asserta(amount_clause_reductions(0)), | |
1596 | asserta(assignment_count_on_cur_level(0)), | |
1597 | asserta(amount_learned_clauses(0)), | |
1598 | asserta(conflict_stats(total(0), since_restart(0), since_reduction(0))), | |
1599 | asserta(recent_lbds_dl(Diff1-Diff1, 0)), | |
1600 | asserta(recent_stack_sizes_dl(Diff2-Diff2, 0)), | |
1601 | asserta(total_lbd_sum(0)), | |
1602 | init_luby_sequence. | |
1603 | ||
1604 | clean_dynamic_solver_state :- | |
1605 | retractall(assignment_timeout_occurred), | |
1606 | retractall(allow_partial_model), | |
1607 | retractall(unfixed_deferred_set_error), | |
1608 | retractall(assignment_count_on_cur_level(_)), | |
1609 | retractall(pending_theory_prop(_,_)), | |
1610 | retractall(glue_clauses(_)), | |
1611 | retractall(glue_level(_,_,_)), | |
1612 | retractall(solver_name(_)), | |
1613 | retractall(restarts(_)), | |
1614 | retractall(is_restart), | |
1615 | retractall(bt_from_smt_solution), | |
1616 | retractall(recent_lbds_dl(_, _)), | |
1617 | retractall(recent_stack_sizes_dl(_, _)), | |
1618 | retractall(saved_phase(_, _)), | |
1619 | %retractall(amount_clause_reductions(_)), | |
1620 | retractall(amount_learned_clauses(_)), | |
1621 | retractall(luby_counter(_)), | |
1622 | %retractall(exclude_sat_solution_clause(_)), | |
1623 | retractall(total_lbd_sum(_)), | |
1624 | retractall(conflict_stats(_, _, _)), | |
1625 | retractall(idl_unsat_core(_)), | |
1626 | retractall(backjump_level(_)), | |
1627 | retractall(backjump_clause(_, _, _, _, _, _)). | |
1628 | ||
1629 | %% Remove dynamically stored unsat core found by the IDL solver. | |
1630 | remove_idl_unsat_core :- | |
1631 | retractall_once(idl_unsat_core(_)). | |
1632 | ||
1633 | %% Store an unsat core found by the IDL solver in the SMT solver's dynamic state. | |
1634 | store_idl_unsat_core(Core) :- | |
1635 | assignment_count_on_cur_level(ACount), | |
1636 | ACount > 1, % at least one unit propagation on this level, otherwise just backtrack | |
1637 | retractall_once(idl_unsat_core(_)), | |
1638 | asserta(idl_unsat_core(Core)). | |
1639 | ||
1640 | %% Announce backtracking after a solution has been found in order to backtrack to search for another solution. | |
1641 | %% We have to be able to distinguish between backtracking due to not finding a solution or backtracking | |
1642 | %% triggered by the user to find another solution. | |
1643 | announce_bt_from_smt_solution :- | |
1644 | asserta(bt_from_smt_solution). | |
1645 | %%%%% | |
1646 | ||
1647 | %% b_to_cnf_safe(+In, +State, -Out). | |
1648 | b_to_cnf_safe(In, State, Out) :- | |
1649 | b_to_cnf(In, State, TOut), | |
1650 | !, | |
1651 | Out = TOut. | |
1652 | b_to_cnf_safe(_, _, _) :- | |
1653 | add_internal_error('B to CNF conversion failed ', cdclt), | |
1654 | fail. | |
1655 | ||
1656 | %% b_to_cnf(+In, +State, -Out). | |
1657 | % Accepts predicates with conjunction, disjunction, and equality of SAT variables. No negations. | |
1658 | b_to_cnf(In, State, Out) :- | |
1659 | get_texpr_expr(In, Expr), | |
1660 | ? | b_to_cnf_aux(Expr, State, Res, []), |
1661 | !, | |
1662 | Res = Out. | |
1663 | b_to_cnf(In, _, _) :- | |
1664 | translate_bexpression(In, PPIn), | |
1665 | !, | |
1666 | add_error_fail(b_to_cnf, 'CNF conversion failed', PPIn). | |
1667 | ||
1668 | b_to_cnf(b(Expr,_,_Info), State) --> | |
1669 | !, | |
1670 | ? | b_to_cnf_aux(Expr, State). |
1671 | b_to_cnf(In, _, _, _) :- | |
1672 | add_error_fail(b_to_cnf, 'Not properly wrapped:', In). | |
1673 | ||
1674 | b_to_cnf_aux(X, _) --> | |
1675 | {X == truth}, !, | |
1676 | []. | |
1677 | b_to_cnf_aux(X, _) --> | |
1678 | {X == falsity}, !, | |
1679 | [[]]. | |
1680 | b_to_cnf_aux(equal(A,B), State) --> | |
1681 | {get_texpr_expr(B, Expr), | |
1682 | Expr == boolean_true, | |
1683 | get_texpr_expr(A, identifier(Name))}, | |
1684 | !, | |
1685 | ? | {member(bind(Name,Res)-StackInfo, State)}, |
1686 | [[StackInfo-pred_true-Res-Name]]. | |
1687 | b_to_cnf_aux(equal(A,B), State) --> | |
1688 | {get_texpr_expr(B, Expr), | |
1689 | Expr == boolean_false, | |
1690 | get_texpr_expr(A, identifier(Name)), | |
1691 | ? | member(bind(Name,Res)-StackInfo, State)}, |
1692 | [[StackInfo-pred_false-Res-Name]]. | |
1693 | b_to_cnf_aux(disjunct(D1,D2), State) --> | |
1694 | b_to_cnf_disj_aux(D1, D2, State). | |
1695 | b_to_cnf_aux(conjunct(A,B), State) --> | |
1696 | ? | b_to_cnf(A, State), |
1697 | ? | b_to_cnf(B, State). |
1698 | ||
1699 | b_to_cnf_disj_aux(D1, D2, State) --> | |
1700 | {get_texpr_expr(D1, conjunct(A,B))}, !, | |
1701 | {create_texpr(disjunct(A,D2), pred, [], DJ1), | |
1702 | create_texpr(disjunct(B,D2), pred, [], DJ2)}, | |
1703 | b_to_cnf_aux(conjunct(DJ1,DJ2), State). | |
1704 | b_to_cnf_disj_aux(D1, D2, State) --> | |
1705 | {get_texpr_expr(D2, conjunct(A,B))}, !, | |
1706 | {create_texpr(disjunct(D1,A), pred, [], DJ1), | |
1707 | create_texpr(disjunct(D1,B), pred, [], DJ2)}, | |
1708 | b_to_cnf_aux(conjunct(DJ1,DJ2), State). | |
1709 | b_to_cnf_disj_aux(D1, D2, State, Res, Acc) :- | |
1710 | b_to_cnf(D1, State, Res1), | |
1711 | b_to_cnf(D2, State, Res2), | |
1712 | !, | |
1713 | ( Res1 = [] | |
1714 | -> Res = Acc | |
1715 | ; Res1 = [[]] | |
1716 | -> append(Res2,Acc,Res) | |
1717 | ; Res2 = [] | |
1718 | -> Res = Acc | |
1719 | ; Res2 = [[]] | |
1720 | -> append(Res1,Acc,Res) | |
1721 | ; ( Res1 = [ResD1], | |
1722 | Res2 = [ResD2] | |
1723 | ) | |
1724 | -> Res = [Res12|Acc], | |
1725 | append(ResD1, ResD2, Res12) | |
1726 | ? | ; join_clauses(Res1,Res2,Res,Acc) |
1727 | -> true | |
1728 | ; add_error_fail(b_to_cnf_disj, 'Cannot join clauses: ', Res1:Res2) | |
1729 | ). | |
1730 | ||
1731 | join_clauses([], _) --> []. | |
1732 | join_clauses([Clause1|T], Clauses2) --> | |
1733 | ? | join_clauses_aux(Clause1,Clauses2), |
1734 | ? | join_clauses(T,Clauses2). |
1735 | ||
1736 | join_clauses_aux(_, []) --> []. | |
1737 | join_clauses_aux(Clause1, [Clause2|T]) --> | |
1738 | {append(Clause1, Clause2, NewClause)}, | |
1739 | [NewClause], | |
1740 | ? | join_clauses_aux(Clause1, T). |
1741 | ||
1742 | ||
1743 | % Used for random restarts. | |
1744 | % First restart is after 32nd conflict, second after additional 32 conflicts, | |
1745 | % third after additional 64 conflicts etc. | |
1746 | init_luby_sequence :- | |
1747 | retractall(luby_counter(_)), | |
1748 | % unit length of 32 | |
1749 | % 1,1,2,1,1,2,4,1,1,2,1,1,2,4,8,.. | |
1750 | assertz(luby_counter(1)), assertz(luby_counter(1)), assertz(luby_counter(2)), assertz(luby_counter(1)), assertz(luby_counter(1)), | |
1751 | assertz(luby_counter(2)), assertz(luby_counter(4)), assertz(luby_counter(1)), assertz(luby_counter(1)), assertz(luby_counter(2)), | |
1752 | assertz(luby_counter(1)), assertz(luby_counter(1)), assertz(luby_counter(2)), assertz(luby_counter(4)), assertz(luby_counter(8)), | |
1753 | assertz(luby_counter(1)), assertz(luby_counter(1)), assertz(luby_counter(2)), assertz(luby_counter(1)), assertz(luby_counter(1)), | |
1754 | assertz(luby_counter(2)), assertz(luby_counter(4)), assertz(luby_counter(8)), assertz(luby_counter(16)), assertz(luby_counter(1)), | |
1755 | assertz(luby_counter(1)), assertz(luby_counter(2)), assertz(luby_counter(1)), assertz(luby_counter(1)), assertz(luby_counter(2)), | |
1756 | assertz(luby_counter(4)), assertz(luby_counter(8)), assertz(luby_counter(16)), assertz(luby_counter(32)), assertz(luby_counter(1)), | |
1757 | assertz(luby_counter(1)), assertz(luby_counter(2)), assertz(luby_counter(1)), assertz(luby_counter(1)), assertz(luby_counter(2)), | |
1758 | assertz(luby_counter(4)), assertz(luby_counter(8)), assertz(luby_counter(16)), assertz(luby_counter(32)), assertz(luby_counter(64)), | |
1759 | assertz(luby_counter(1)), assertz(luby_counter(1)), assertz(luby_counter(2)), assertz(luby_counter(1)), assertz(luby_counter(1)), | |
1760 | assertz(luby_counter(2)), assertz(luby_counter(4)), assertz(luby_counter(8)), assertz(luby_counter(16)), assertz(luby_counter(32)), | |
1761 | assertz(luby_counter(64)), assertz(luby_counter(128)). | |
1762 | ||
1763 | % ---------------- | |
1764 | ||
1765 | %% simplify_cnf(+CNF, -Simplified). | |
1766 | % Boolean resolution. | |
1767 | simplify_cnf([], []). | |
1768 | simplify_cnf([Clause|T], NewCnf) :- | |
1769 | simplify_clause(Clause, _, Simplified, IsTrue), !, | |
1770 | Simplified \== [], % contradiction if a clause is empty | |
1771 | ( IsTrue == true | |
1772 | -> NewCnf = NT % remove true clauses | |
1773 | ; NewCnf = [Simplified|NT] | |
1774 | ), | |
1775 | simplify_cnf(T, NT). | |
1776 | ||
1777 | simplify_clause([], IsTrue, [], IsTrue). | |
1778 | simplify_clause([_-Pol-Var-_|T], IsTrueAcc, NT, IsTrue) :- | |
1779 | ground(Var), | |
1780 | Pol \== Var, | |
1781 | !, | |
1782 | simplify_clause(T, IsTrueAcc, NT, IsTrue). | |
1783 | simplify_clause([StackInfo-Pol-Var-SatVarName|T], IsTrueAcc, [StackInfo-Pol-Var-SatVarName|NT], IsTrue) :- | |
1784 | ( Pol == Var | |
1785 | -> IsTrueAcc = true | |
1786 | ; true | |
1787 | ), | |
1788 | simplify_clause(T, IsTrueAcc, NT, IsTrue). | |
1789 | ||
1790 | clause_order(_-_-_-A3, _-_-_-B3) :- A3 @< B3. | |
1791 | ||
1792 | %% unit_propagate_cnf(+SolverEnv, +StateMutable, +Clauses, -NewClauses). | |
1793 | % A simple unit propagation, useful to run before reification. | |
1794 | % Removes duplicates from each clause. | |
1795 | % Important to identify all unit clauses, b_to_cnf does not check for unique sat variables in clauses. | |
1796 | % An exhaustive unit-propagation prior to the reification is not beneficial | |
1797 | % since simplifying a CNF is slow compared to using watched literals in sat/4. | |
1798 | % Note: It is important to remove duplicates, e.g., using sort/2. Otherwise, a conflict clause with duplicates | |
1799 | % would lead to failure for first UIP CDCL (first UIP not recognized due to duplicate decision level). | |
1800 | unit_propagate_cnf(SolverEnv, StateMutable, Clauses, NewClauses) :- | |
1801 | ? | unit_prop_clause_sort(true, SolverEnv, StateMutable, Clauses, _, _, TNewClauses), !, |
1802 | simplify_cnf(TNewClauses, NewClauses). | |
1803 | ||
1804 | propagate_unit_clause([StackInfo-Pol-PrologVar-SatVarName], StateMutable, RAcc) :- | |
1805 | ( PrologVar == Pol | |
1806 | -> % duplicate unit clause already propagated | |
1807 | true | |
1808 | ; PrologVar = Pol, | |
1809 | RAcc = true, | |
1810 | debug_format_sat("deterministic unit propagation of ~w with polarity ~w before reification", [SatVarName,Pol]), | |
1811 | ? | get_next_assignment_count_on_level(ACount), |
1812 | StackInfo = (unit,(0,ACount),Pol,[_-Pol-PrologVar-SatVarName]), | |
1813 | ? | bt_log_sat_stack(StateMutable, SatVarName, Pol), |
1814 | log_unit_propagation | |
1815 | ). | |
1816 | ||
1817 | %% unit_prop_clause_sort(+Sort, +SolverEnv, +StateMutable, +CNF, +RAcc, -Resolved, -NewClauses). | |
1818 | % Removes duplicates from each clause if +Sort is true. | |
1819 | % Logs if a variable has been unit propagated in -Resolved using +RAcc. | |
1820 | unit_prop_clause_sort(_, _, _, [], RAcc, RAcc, []). | |
1821 | unit_prop_clause_sort(Sort, SolverEnv, StateMutable, [[StackInfo-Pol-PrologVar-SatVarName]|T], RAcc, Resolved, NT) :- | |
1822 | ? | propagate_unit_clause([StackInfo-Pol-PrologVar-SatVarName], StateMutable, RAcc), |
1823 | !, | |
1824 | ? | unit_prop_clause_sort(Sort, SolverEnv, StateMutable, T, RAcc, Resolved, NT). |
1825 | unit_prop_clause_sort(Sort, SolverEnv, StateMutable, [Clause|T], RAcc, Resolved, NewClauses) :- | |
1826 | ( Sort = true | |
1827 | -> remove_dups(Clause, TNewClause), | |
1828 | % clause_order ensures that watched literals are initially set to the same variables for stronger propagation | |
1829 | samsort(clause_order, TNewClause, NewClause) | |
1830 | ; NewClause = Clause | |
1831 | ), | |
1832 | ( NewClause = [_-_-_-_] | |
1833 | -> propagate_unit_clause(NewClause, StateMutable, RAcc), | |
1834 | NewClauses = NT | |
1835 | ; NewClauses = [NewClause|NT] | |
1836 | ), !, | |
1837 | ? | unit_prop_clause_sort(Sort, SolverEnv, StateMutable, T, RAcc, Resolved, NT). |
1838 | ||
1839 | % ---------------- | |
1840 | ||
1841 | portray_cnf(Clauses) :- length(Clauses,Len), format('CNF with ~w clauses:~n',[Len]), | |
1842 | maplist(portray_sat_clause,Clauses). | |
1843 | ||
1844 | portray_sat_clause(Clause) :- write(' '),maplist(portray_literal,Clause),nl. | |
1845 | ||
1846 | portray_literal(pred_false-PrologVar-ID) :- !, format('- ~w(~w) ',[ID,PrologVar]). | |
1847 | portray_literal(pred_true-PrologVar-ID) :- !, format(' ~w(~w) ',[ID,PrologVar]). | |
1848 | portray_literal(Lit) :- format(' *** UNKNOWN: ~w ',[Lit]). | |
1849 | ||
1850 | % ---------------- | |
1851 | ||
1852 | /* | |
1853 | %% static_sat_symmetry_breaking(+Clauses, +SolverEnv, +CurLevelMut, -NewSolverEnv). | |
1854 | % Static SAT symmetry breaking after unit propagation of problem_setup/3 but only once, e.g., not after a restart or bj to level 0 | |
1855 | % Can only be used for pure SAT solving. | |
1856 | static_sat_symmetry_breaking(_, SolverEnv, _, NewSolverEnv) :- | |
1857 | static_sat_symmetry_breaking(false), | |
1858 | !, | |
1859 | NewSolverEnv = SolverEnv. | |
1860 | static_sat_symmetry_breaking(Clauses, SolverEnv, CurLevelMut, NewSolverEnv) :- | |
1861 | \+ symmetry_breaking_pred(_, _), | |
1862 | !, | |
1863 | get_symmetry_breaking_predicates(Clauses, SBPsConjNoRef, NewSatVars), | |
1864 | asserta(symmetry_breaking_pred(SBPsConjNoRef,NewSatVars)), | |
1865 | static_sat_symmetry_breaking(Clauses, SolverEnv, CurLevelMut, NewSolverEnv). | |
1866 | static_sat_symmetry_breaking(_, SolverEnv, CurLevelMut, NewSolverEnv) :- | |
1867 | get_asserted_symmetry_breaking_pred(SolverEnv, SBPsConj, NewSolverEnv), | |
1868 | problem_setup(NewSolverEnv, CurLevelMut, SBPsConj). | |
1869 | ||
1870 | get_asserted_symmetry_breaking_pred(SolverEnv, SBPsConj, NewSolverEnv) :- | |
1871 | symmetry_breaking_pred(SBPsConjNoRef, NewSatVars), | |
1872 | add_symmetry_breaking_eqs_to_solver_env(NewSatVars, SolverEnv, NewSolverEnv), | |
1873 | get_from_solver_env(NewSolverEnv, pl_vars, PlVars), | |
1874 | set_variable_references_in_clauses(PlVars, SBPsConjNoRef, SBPsConj), | |
1875 | findall(Var, (member(Var, NewSatVars), bt_asserta(heuristic_tuple(Var,1))), _). | |
1876 | ||
1877 | %% add_symmetry_breaking_eqs_to_solver_env(+NewSatVars, +SolverEnv, -NewSolverEnv). | |
1878 | % Symmetry breaking might introduce new SAT variables for equalities inbetween cycles of permutations. | |
1879 | % We update the solver environment and create the corresponding SMT formulas for equalities here. | |
1880 | % This is necessary, e.g., if a SAT variable corresponding to an equality introduced | |
1881 | % from symmetry breaking is involved in a conflict. | |
1882 | add_symmetry_breaking_eqs_to_solver_env(NewSatVars, SolverEnv, NewSolverEnv) :- | |
1883 | SolverEnv = [sat_vars:SatVars,sat_varnames:SatVarNames,sat_bindings:SatBindings,t2b_env:Env,pl_vars:PrologSatVarTriple], | |
1884 | add_symmetry_breaking_eqs_to_solver_env(NewSatVars, SatVars, SatVarNames, SatBindings, Env, PrologSatVarTriple, NSatVars, NSatVarNames, NSatBindings, NEnv, NPrologSatVarTriple), | |
1885 | NewSolverEnv = [sat_vars:NSatVars,sat_varnames:NSatVarNames,sat_bindings:NSatBindings,t2b_env:NEnv,pl_vars:NPrologSatVarTriple]. | |
1886 | ||
1887 | add_symmetry_breaking_eqs_to_solver_env([], SatVars, SatVarNames, SatBindings, Env, PrologSatVarTriple, SatVars, SatVarNames, SatBindings, Env, PrologSatVarTriple). | |
1888 | add_symmetry_breaking_eqs_to_solver_env([NewSatVarName-EqClauses|T], SatVars, SatVarNames, SatBindings, Env, PrologSatVarTriple, NSatVars, NSatVarNames, NSatBindings, NEnv, NPrologSatVarTriple) :- | |
1889 | maplist(clause_to_smt_disjunction(SatVars), EqClauses, EqSmtClauses), | |
1890 | conjunct_predicates(EqSmtClauses, EqSmt1), % all true | |
1891 | maplist(negate_smt_formula, EqSmtClauses, NegEqSmtClauses), | |
1892 | conjunct_predicates(NegEqSmtClauses, EqSmt2), % or all false | |
1893 | EqSmt = b(disjunct(EqSmt1,EqSmt2),pred,[]), | |
1894 | SatVars1 = [b(identifier(NewSatVarName),boolean,[smt_formula(EqSmt),eq_symmetry_break])|SatVars], | |
1895 | SatVarNames1 = [NewSatVarName|SatVarNames], | |
1896 | SatBindings1 = [bind(NewSatVarName,Var)|SatBindings], | |
1897 | PrologSatVarTriple1 = [Var-NewSatVarName-EqSmt|PrologSatVarTriple], | |
1898 | Env1 = [(EqSmt,b(identifier(NewSatVarName),boolean,[]))|Env], | |
1899 | add_symmetry_breaking_eqs_to_solver_env(T, SatVars1, SatVarNames1, SatBindings1, Env1, PrologSatVarTriple1, NSatVars, NSatVarNames, NSatBindings, NEnv, NPrologSatVarTriple). | |
1900 | ||
1901 | %clause_to_smt_disjunction(_, [], b(truth,pred,[])). | |
1902 | clause_to_smt_disjunction(SatVars, [Pol-_-SatVarName|T], SmtDisj) :- | |
1903 | get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula), | |
1904 | clause_to_smt_disjunction(SatVars, T, SmtFormula, SmtDisj). | |
1905 | ||
1906 | clause_to_smt_disjunction(_, [], Acc, Acc). | |
1907 | clause_to_smt_disjunction(SatVars, [Pol-_-SatVarName|T], Acc, SmtDisj) :- | |
1908 | get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula), | |
1909 | NAcc = b(disjunct(SmtFormula,Acc),pred,[]), | |
1910 | clause_to_smt_disjunction(SatVars, T, NAcc, SmtDisj). | |
1911 | */ | |
1912 | ||
1913 | /* | |
1914 | % Remove half of the clauses every "frequency_constant + constant_factor * x" conflicts, | |
1915 | % where x is the amount of clause reductions so far. We keep clauses with a small LBD forever. | |
1916 | possibly_discard_learned_clauses :- | |
1917 | conflict_stats(_, _, since_reduction(SRed)), | |
1918 | cdclt_settings:discard_learned_clauses_frequency_constant(Frequency), | |
1919 | SRed >= Frequency, % first check to improve performance | |
1920 | amount_clause_reductions(Reductions), | |
1921 | cdclt_settings:discard_learned_clauses_constant_factor(Factor), | |
1922 | Threshold is Frequency + Factor * Reductions, | |
1923 | SRed == Threshold, | |
1924 | !, | |
1925 | log_set_of_learned_clauses_reduction, | |
1926 | debug_format_sat("~nDiscard half of learned clauses..", []), | |
1927 | cdclt_settings:discard_clause_greater_lbd(LbdLimit), | |
1928 | amount_learned_clauses(ALC), | |
1929 | Half is ALC // 2, | |
1930 | NReductions is Reductions + 1, | |
1931 | retract(amount_clause_reductions(_)), | |
1932 | asserta(amount_clause_reductions(NReductions)), | |
1933 | discard_half_of_learned_clauses_greater_lbd(0, Half, LbdLimit, Removed), | |
1934 | log_forgotten_clauses(Removed), | |
1935 | retract(amount_learned_clauses(Old)), | |
1936 | New is Old - Removed, | |
1937 | asserta(amount_learned_clauses(New)), | |
1938 | retract(conflict_stats(total(Total), since_restart(SRRed), _)), | |
1939 | asserta(conflict_stats(total(Total), since_restart(SRRed), since_reduction(0))), !. | |
1940 | possibly_discard_learned_clauses. | |
1941 | % Remove half of the clauses learned so far. | |
1942 | % We keep clauses with an LBD smaller than cdclt_settings:discard_clause_greater_lbd/1 | |
1943 | % forever. Thus it is not guaranteed that exactly half of the clauses are deleted if | |
1944 | % a lot of high quality clauses have been learned. | |
1945 | discard_half_of_learned_clauses_greater_lbd(C, Half, LbdLimit, Removed) :- | |
1946 | C =< Half, | |
1947 | retract(backjump_clause(BjLevel, BjClause, LbdScore, BjSatVars, UsedVars, AC)), | |
1948 | !, | |
1949 | ( LbdScore > LbdLimit | |
1950 | -> C1 is C + 1, | |
1951 | discard_half_of_learned_clauses_greater_lbd(C1, Half, LbdLimit, Removed) | |
1952 | ; discard_half_of_learned_clauses_greater_lbd(C, Half, LbdLimit, Removed), | |
1953 | asserta(backjump_clause(BjLevel, BjClause, LbdScore, BjSatVars, UsedVars, AC)) | |
1954 | ). | |
1955 | discard_half_of_learned_clauses_greater_lbd(C, _, _, C). | |
1956 | */ |