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 */