1 | % (c) 2019-2022 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(dpllt_sat_solver, [b_to_cnf/3, | |
6 | create_solver_state/1, | |
7 | sat/3, | |
8 | sat/4, | |
9 | restarts/1, | |
10 | is_backjumping/0, | |
11 | is_last_propagated_sat_var/2, | |
12 | announce_bt_from_smt_solution/0, | |
13 | store_idl_unsat_core/1, | |
14 | log_theory_propagation_sat_stack/3, | |
15 | set_variable_references_in_clauses/3, | |
16 | remove_idl_unsat_core/0, | |
17 | exhaustive_unit_propagate_cnf/4, | |
18 | unit_propagate_cnf/4, | |
19 | init_dynamic_solver_state/1, | |
20 | get_bindings_from_ids/5, | |
21 | portray_cnf/1, | |
22 | portray_sat_stack/1, | |
23 | cnf_to_smt/2]). | |
24 | ||
25 | :- meta_predicate(asserta_once(0)). | |
26 | :- meta_predicate(bt_retract_if_exists(0)). | |
27 | ||
28 | :- use_module(library(lists)). | |
29 | :- use_module(library(avl)). | |
30 | :- use_module(library(heaps)). | |
31 | :- use_module(library(ordsets)). | |
32 | :- use_module(library(timeout)). | |
33 | :- use_module(library(samsort)). | |
34 | :- use_module(library(aggregate),[forall/2]). | |
35 | ||
36 | :- use_module(smt_solvers_interface(ast_optimizer_for_smt)). | |
37 | :- use_module(dpllt_solver('dpllt_pred_to_sat')). | |
38 | :- use_module(dpllt_solver('dpllt_settings')). | |
39 | :- use_module(dpllt_solver('symmetry_check/sat_symmetry_breaking')). | |
40 | :- use_module(wdsrc(well_def_hyps), [empty_hyps/1]). | |
41 | :- use_module(wdsrc(well_def_analyser), [compute_wd/4]). | |
42 | :- use_module(probsrc(tools_portability), [exists_source/1]). | |
43 | :- use_module(probsrc(bsyntaxtree),[get_texpr_expr/2, | |
44 | safe_create_texpr/4, | |
45 | disjunct_predicates/2, | |
46 | conjunct_predicates/2, | |
47 | conjunction_to_list/2]). | |
48 | :- use_module(probsrc(debug)). | |
49 | :- use_module(probsrc(error_manager), [add_error_fail/3,add_internal_error/2]). | |
50 | :- use_module(probsrc(translate), [translate_bexpression/2]). | |
51 | :- use_module(extrasrc(unsat_cores), [unsat_core_with_fixed_conjuncts/3,unsat_chr_core_list_with_auto_time_limit/5]). | |
52 | :- use_module(probsrc(module_information), [module_info/2]). | |
53 | ||
54 | :- module_info(group, dpllt). | |
55 | :- module_info(description,'This module provides the SAT solver for DPLL(T) implementing CDCL with backjumping.'). | |
56 | ||
57 | :- dynamic backjump_wd_level/1, backjump_wd_clause/3, solver_name/1, incremental_mode/0, memoize_backjump_clause/3, backjump_clause/4, backjump_level/1, conflict_stats/3, saved_phase/2, bt_from_smt_solution/0, is_restart/0, exclude_sat_solution_clause/1, total_lbd_sum/1, recent_lbds_dl/2, recent_stack_sizes_dl/2, amount_clause_reductions/1, amount_learned_clauses/1, idl_unsat_core/1. | |
58 | :- volatile backjump_wd_level/1, backjump_wd_clause/3, solver_name/1, incremental_mode/0, memoize_backjump_clause/3, backjump_clause/4, backjump_level/1, conflict_stats/3, saved_phase/2, bt_from_smt_solution/0, is_restart/0, exclude_sat_solution_clause/1, total_lbd_sum/1, recent_lbds_dl/2, recent_stack_sizes_dl/2, amount_clause_reductions/1, amount_learned_clauses/1, idl_unsat_core/1. | |
59 | ||
60 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
61 | % A sat solver utilising delay declaration to implement watched literals. | |
62 | % Authors: Jacob Howe and Andy King | |
63 | % | |
64 | % Extended for DPLL(T) with first UIP conflict-driven clause learning, | |
65 | % theory propagation, branching heuristics, phase saving for rapid restarts, | |
66 | % learned clause reduction, random restarts, and static SMT symmetry breaking. | |
67 | % We implement a variant of VSIDS as follows: | |
68 | % - one score for each variable initialized with the number of occurrences in all clauses | |
69 | % - increase score by one for each variable occuring in a learned clause | |
70 | % - divide all scores by 2 after each dpllt_settings:vsids_decay_frequency/1 conflict (favor recently learned clauses) | |
71 | % Random restarts: | |
72 | % restarts using either the Luby sequence or Glucose restarts | |
73 | % Phase saving: | |
74 | % - if backjump level is 0 because of learning a unit clause or a random restart, | |
75 | % cache phases/polarities of variable assignments (see saved_phase/2) | |
76 | % - when the decision heuristic decides to branch on a variable, pick the cached phase first if one exists | |
77 | % Reducing learned clauses: | |
78 | % - remove half of the learned clauses every "frequency_constant + constant_factor * x" conflicts, where x is the amount of clause reductions so far | |
79 | % - keep clauses with small LBD (dpllt_settings:discard_clause_greater_lbd/1) forever | |
80 | % incremental_mode/0 memoizes learned clauses and reuses them for the following calls. | |
81 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
82 | ||
83 | % TO DO: | |
84 | % [] ANRFA, VMTF, (ACIDS) branching heuristics | |
85 | % -> empirical results by Biere and Fröhlich in "Evaluating CDCL Variable Scoring Schemes" have shown that EVSIDS is as good as the other heuristics | |
86 | % [] polarity for heuristic scores (no branching when selecting max heuristic value?) | |
87 | % -> first tests inidicated that this is slower | |
88 | % (- FirstNewCutscheme (cf. https://www.aaai.org/Papers/JAIR/Vol22/JAIR-2210.pdf)) | |
89 | % [] improve implying constraint detection (e.g., :dpllt x > y & gt : {x+1} & y > gt) | |
90 | % [] clause minimization (cf. Definition 9, "Towards Understanding and Harnessing the Potential of Clause Learning") | |
91 | % [] use profiler | |
92 | % [] check out "Advances in Symmetry Breaking for SAT Modulo Theories" by Dinliwal et al. for static SMT symmetry breaking | |
93 | ||
94 | :- if(exists_source(library(mutdict))). | |
95 | :- use_module(library(mutdict)). | |
96 | :- else. | |
97 | new_mutdict(Dict) :- | |
98 | empty_avl(Avl), | |
99 | create_mutable(Avl, Dict). | |
100 | ||
101 | mutdict_put(Dict, Key, Value) :- | |
102 | get_mutable(Avl, Dict), | |
103 | avl_store(Key, Avl, Value, NewAvl), | |
104 | update_mutable(NewAvl, Dict). | |
105 | ||
106 | mutdict_get(Dict, Key, Value) :- | |
107 | get_mutable(Avl, Dict), | |
108 | avl_fetch(Key, Avl, Value). | |
109 | ||
110 | mutdict_keys(Dict, Keys) :- | |
111 | get_mutable(Avl, Dict), | |
112 | avl_domain(Avl, Keys). | |
113 | ||
114 | :- endif. | |
115 | ||
116 | debug_format_sat(_, _) :- | |
117 | debug_mode(off), | |
118 | !. | |
119 | debug_format_sat(Msg, Vars) :- | |
120 | append(Msg, " (DPLL(T) SAT Solver)~n", NCodes), | |
121 | atom_codes(NMsg, NCodes), | |
122 | format(NMsg, Vars), !. | |
123 | ||
124 | debug_format_sat(_, _, _) :- | |
125 | debug_mode(off), | |
126 | !. | |
127 | debug_format_sat(Msg, Vars, Pred) :- | |
128 | format(Msg, Vars), | |
129 | translate:print_bexpr(Pred), nl, !. | |
130 | ||
131 | %log_propagated_wd_pred(SatId) :- | |
132 | % bt_asserta(propagated_wd_pred(SatId)). | |
133 | ||
134 | clauses_to_sat_assert([], SatVars, T2BEnv, SatVars, T2BEnv, []). | |
135 | clauses_to_sat_assert([SmtClause-LbdScore|T], SatVars, T2BEnv, NewSatVars, NewT2BEnv, [SatClause|NT]) :- | |
136 | predicate_to_sat(normal, [], SatVars, T2BEnv, SmtClause, TT2BEnv, _, SatClause, TSatVars), | |
137 | !, | |
138 | asserta(backjump_clause(0, SatClause, LbdScore, [])), | |
139 | debug_format_sat("Learn clause from prior run ~w~n", [SatClause]), | |
140 | clauses_to_sat_assert(T, TSatVars, TT2BEnv, NewSatVars, NewT2BEnv, NT). | |
141 | clauses_to_sat_assert([_|T], SatVars, T2BEnv, NewSatVars, NewT2BEnv, NT) :- | |
142 | clauses_to_sat_assert(T, SatVars, T2BEnv, NewSatVars, NewT2BEnv, NT). | |
143 | ||
144 | assert_memoized_clauses(SolverName, SolverEnv, NewSolverEnv) :- | |
145 | findall(C-LbdScore, memoize_backjump_clause(SolverName, C, LbdScore), SmtClauses), | |
146 | SmtClauses \== [], | |
147 | !, | |
148 | % learned clauses can be applied to all variables which are equal to new ids (see id_equality/3) | |
149 | %findall(CPrime-LbdScore, (memoize_backjump_clause(SolverName, C, LbdScore), replace_ids_with_eq_ids_top_level(C, CPrime)), PrimedSmtClauses), | |
150 | %append(SmtClauses, PrimedSmtClauses, FullClauses), | |
151 | get_from_solver_env(SolverEnv, sat_vars, SatVars), | |
152 | get_from_solver_env(SolverEnv, t2b_env, T2BEnv), | |
153 | clauses_to_sat_assert(SmtClauses, SatVars, T2BEnv, NewSatVars, NewT2BEnv, _SatClauses), | |
154 | get_bindings_from_ids(NewSatVars, NewSatBindings, NewSatVarNames, _, PrologSatVarTriple), | |
155 | NewSolverEnv = [sat_vars:NewSatVars,sat_varnames:NewSatVarNames,sat_bindings:NewSatBindings,t2b_env:NewT2BEnv,pl_vars:PrologSatVarTriple]. | |
156 | ||
157 | learn_clauses_if_incremental(SolverName, StateMutable, SolverEnv, Clauses, NewSolverEnv, NewClauses) :- | |
158 | incremental_mode, | |
159 | format("INCREMENTAL MODE: Learn clauses from prior run", []), | |
160 | assert_memoized_clauses(SolverName, SolverEnv, NewSolverEnv), | |
161 | learn_asserted_clauses(StateMutable, 0, SolverEnv, Clauses, NewClauses), !. | |
162 | learn_clauses_if_incremental(_, _, SolverEnv, Clauses, SolverEnv, Clauses). | |
163 | ||
164 | % Given a set of boolean B identifiers. Create a list of bindings containing terms bind/2 | |
165 | % and a list of tuples of B identifier and corresponding Prolog variable used for sat solving. | |
166 | get_bindings_from_ids(SatVars, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple) :- | |
167 | get_bindings_from_ids_acc(SatVars, [], [], [], [], SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple), !. | |
168 | ||
169 | get_bindings_from_ids_acc([], AccBindings, AccNames, AccTuples, AccPlVars, AccBindings, AccNames, AccTuples, AccPlVars). | |
170 | get_bindings_from_ids_acc([b(identifier(Name),IdType,IdInfo)|T], AccBindings, AccNames, AccTuples, AccPlVars, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple) :- | |
171 | NewAccBindings = [bind(Name,PrologVar)|AccBindings], | |
172 | NewAccTuples = [(b(identifier(Name),IdType,IdInfo),PrologVar)|AccTuples], | |
173 | !, | |
174 | ? | ( member(smt_formula(SmtFormula), IdInfo) |
175 | -> NewAccPlVars = [PrologVar-Name-SmtFormula|AccPlVars] | |
176 | ; % plain SAT variable which is not reified with a theory solver, e.g., introduced by CNF optimization rewriting | |
177 | OptEq = b(equal(b(identifier(Name),boolean,[]),b(boolean_true,boolean,[])),pred,[]), | |
178 | NewAccPlVars = [PrologVar-Name-OptEq|AccPlVars] | |
179 | ), | |
180 | get_bindings_from_ids_acc(T, NewAccBindings, [Name|AccNames], NewAccTuples, NewAccPlVars, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple). | |
181 | get_bindings_from_ids_acc([_|T], AccBindings, AccNames, AccTuples, AccPlVars, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple) :- | |
182 | get_bindings_from_ids_acc(T, AccBindings, AccNames, AccTuples, AccPlVars, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple). | |
183 | ||
184 | %% sat(+SolverName, +SolverEnv, +Clauses). | |
185 | % SolverEnv is a list [sat_vars:_, sat_bindings:_, t2b_env:_, pl_vars:_]. | |
186 | % sat_vars are boolean b/3 identifier ASTs for corresponding SAT variables in Clauses. | |
187 | % sat_bindings is a list of terms bind/2 as used by the ProB constraint solver. | |
188 | % t2b_env is the environment mapping SAT variable names and theory formulae used to | |
189 | % translate B predicates to SAT. | |
190 | % pl_vars is a list of triples PrologVar-SatVarName-SmtFormula. | |
191 | % Note: init_dynamic_solver_state/1 has to be called before the call to sat/3 | |
192 | sat(SolverName, SolverEnv, Clauses) :- | |
193 | debug_format_sat("Start SAT solving with solver ~w ", [SolverName]), | |
194 | create_solver_state(StateMutable), | |
195 | learn_clauses_if_incremental(SolverName, StateMutable, SolverEnv, Clauses, NewSolverEnv, NewClauses), | |
196 | %init_heuristic(SolverEnv), | |
197 | init_decision_heuristic(StateMutable, NewClauses), | |
198 | sat_stateful_pre(NewSolverEnv, StateMutable, NewClauses). | |
199 | ||
200 | %% sat(+SolverName, +SolverEnv, +StateMutable, +Clauses). | |
201 | % Note: init_dynamic_solver_state/1 has to be called before the call to sat/4 | |
202 | sat(SolverName, SolverEnv, StateMutable, Clauses) :- | |
203 | debug_format_sat("Start SAT solving with solver ~w ", [SolverName]), | |
204 | learn_clauses_if_incremental(SolverName, StateMutable, SolverEnv, Clauses, NewSolverEnv, NewClauses), | |
205 | ? | init_decision_heuristic(StateMutable, NewClauses), |
206 | ? | sat_stateful_pre(NewSolverEnv, StateMutable, NewClauses). |
207 | ||
208 | % Wrapper for sat_stateful_restart_cp/3 to enable backjumping to level 0 several times. | |
209 | sat_stateful_pre(SolverEnv, StateMutable, Clauses) :- | |
210 | ? | sat_stateful_restart_cp(SolverEnv, StateMutable, Clauses). |
211 | ||
212 | sat_stateful_restart_cp(SolverEnv, StateMutable, Clauses) :- | |
213 | ? | ( sat_stateful(SolverEnv, StateMutable, Clauses) |
214 | ; % we either learned a unit-clause from conflict analysis or randomly restart | |
215 | % in both cases, we learn all asserted backjump clauses | |
216 | retract(backjump_level(0)), | |
217 | ( retract(is_restart) | |
218 | -> debug_format_sat("backjump to level 0 random restart", []) | |
219 | ; debug_format_sat("backjump to level 0", []) | |
220 | ), | |
221 | learn_asserted_clauses(StateMutable, 0, SolverEnv, Clauses, NewClauses), | |
222 | ? | sat_stateful_pre(SolverEnv, StateMutable, NewClauses) |
223 | ). | |
224 | ||
225 | %% sat_stateful(+Clauses, +StateMutable, +Clauses). | |
226 | % DPLL with first UIP conflict-driven clause learning, two-watched literals, VSIDS branching heuristic, | |
227 | % random restarts (Luby sequence with unit length 32), and phase saving for rapid restarts. | |
228 | % See create_solver_state/1 for variable StateMutable. | |
229 | sat_stateful(SolverEnv, StateMutable, Clauses) :- | |
230 | ? | problem_setup(SolverEnv, StateMutable, Clauses), |
231 | update_full_state(StateMutable, cur_level, 1), | |
232 | get_from_solver_env(SolverEnv, pl_vars, PlVars), % TO DO: enable constant access by assuming an order of SolverEnv | |
233 | %static_sat_symmetry_breaking(Clauses, SolverEnv, CurLevelMut, NewSolverEnv), | |
234 | ? | elim_vars(SolverEnv, StateMutable, PlVars). |
235 | ||
236 | %% elim_vars(+SolverEnv, +StateMutable, +PlVars). | |
237 | elim_vars(SolverEnv, StateMutable, PlVars) :- | |
238 | get_full_state(StateMutable, cur_level, CurLevel), | |
239 | ( % solution found | |
240 | get_full_state(StateMutable, heuristic_avl, AVL), | |
241 | empty_avl(AVL) | |
242 | ; update_full_state(StateMutable, decision_level, CurLevel), | |
243 | %possibly_decay_heuristic_values, % only for vsids; remove for now | |
244 | ? | ( elim_vars_from_asserted_heuristic_rapid_restart(SolverEnv, StateMutable, CurLevel, PlVars) |
245 | ; % backjumping | |
246 | backjump_level(C), | |
247 | debug_format_sat("Current level is ~w", [CurLevel]), | |
248 | C == CurLevel, | |
249 | retract(backjump_level(C)), | |
250 | debug_format_sat("~nbackjump branch prop level ~w", [CurLevel]), | |
251 | ? | get_clauses_to_learn_bump_scores(StateMutable, C, SolverEnv, ClausesToLearn), |
252 | ? | problem_setup(SolverEnv, StateMutable, ClausesToLearn), |
253 | ? | elim_vars(SolverEnv, StateMutable, PlVars) |
254 | ) | |
255 | ). | |
256 | ||
257 | %% handle_backjump_wd_clauses(+BjClausesNoRef, +LbdScore, +CurLevel, +StateMutable, +SolverEnv). | |
258 | % Learn and convert to common backjump clause. | |
259 | handle_backjump_wd_clauses(BjClausesNoRef, LbdScore, CurLevel, StateMutable, SolverEnv) :- | |
260 | ? | set_references_and_bump_scores(BjClausesNoRef, [], StateMutable, SolverEnv, ClausesToLearn), |
261 | !, | |
262 | ? | problem_setup(SolverEnv, StateMutable, ClausesToLearn), |
263 | ? | bt_asserta(backjump_clause(CurLevel, BjClausesNoRef, LbdScore, [])). |
264 | ||
265 | %% elim_vars_from_asserted_heuristic_rapid_restart(+SolverEnv, +StateMutable, +CurLevel, +PlVars). | |
266 | % Variable State Independent Decaying Sum (VSIDS) branching heuristic. | |
267 | % Initially, each variable is assigned the number of its occurrences in all clauses as its score. | |
268 | % Afterwards, for each conflict clause, the scores of the variables occuring in the clause are increased by bump_heuristic_score_for_type. | |
269 | % Periodically divides all scores by a constant for vsids (see possibly_decay_heuristic_values/0). | |
270 | % Possibly choose the polarity to assign first using saved_phase/2 for rapid restarts. | |
271 | % Note: Assert state before propagation because Var is bound to coroutines. | |
272 | % OriginalClause not necessary for decision variables in the stack because | |
273 | % they are not expanded during conflict analysis. | |
274 | elim_vars_from_asserted_heuristic_rapid_restart(SolverEnv, StateMutable, CurLevel, PlVars) :- | |
275 | \+ backjump_level(_), | |
276 | \+ backjump_wd_level(_), | |
277 | \+ idl_unsat_core(_), | |
278 | max_heuristic_values(StateMutable, MaxScore, SatVarNames), | |
279 | debug_format_sat("Max heuristic values with score ~w are ~w", [MaxScore,SatVarNames]), | |
280 | get_decision_variable_from_list(SatVarNames, SatVarName), | |
281 | delete_state_instance(StateMutable, heuristic_avl, (SatVarName, MaxScore)), | |
282 | get_pl_var_for_sat_id(SatVarName, PlVars, Var), | |
283 | NextLevel is CurLevel + 1, | |
284 | ? | ( saved_phase(SatVarName, SavedPol) |
285 | -> elim_var_from_saved_phase(SatVarName, SavedPol, Var, SolverEnv, StateMutable, CurLevel, PlVars) | |
286 | ; % uninformed phase/polarity selection | |
287 | ? | ( bt_log_sat_stack(StateMutable, SatVarName, branch, CurLevel, pred_true, _OriginalClause), |
288 | debug_format_sat("Decide variable ~w with polarity ~w on level ~w", [SatVarName,pred_true,CurLevel]), | |
289 | %get_theory_formula_for_satvar(SolverEnv, SatVarName, TheoryFormula), | |
290 | %translate:print_bexpr(TheoryFormula),nl, | |
291 | Var = pred_true, | |
292 | ? | update_full_state(StateMutable, cur_level, NextLevel), |
293 | ? | elim_vars(SolverEnv, StateMutable, PlVars) |
294 | ; ( \+ backjump_level(_), | |
295 | \+ backjump_wd_level(_) | |
296 | ; retract(backjump_wd_level(CurLevel)), % backjump to wd decision without CDCL (custom backjumping) | |
297 | retract(backjump_wd_clause(_, BjClauseNoRef, LbdScore)), | |
298 | ? | handle_backjump_wd_clauses([BjClauseNoRef], LbdScore, CurLevel, StateMutable, SolverEnv) |
299 | ), | |
300 | %( learn_idl_core(StateMutable, CurLevel, SolverEnv) | |
301 | %; true | |
302 | %), | |
303 | ( ground(Var) | |
304 | -> true | |
305 | ? | ; bt_log_sat_stack(StateMutable, SatVarName, branch, CurLevel, pred_false, _OriginalClause), |
306 | debug_format_sat("Decide variable ~w with polarity ~w on level ~w", [SatVarName,pred_false,CurLevel]), | |
307 | %get_theory_formula_for_satvar(SolverEnv, SatVarName, TheoryFormula), | |
308 | %translate:print_bexpr(TheoryFormula),nl, | |
309 | Var = pred_false | |
310 | ), | |
311 | update_full_state(StateMutable, cur_level, NextLevel), | |
312 | ? | elim_vars(SolverEnv, StateMutable, PlVars) |
313 | ) | |
314 | ). | |
315 | ||
316 | %% elim_var_from_saved_phase(+SatVarName, +SavedPol, +Var, +SolverEnv, +StateMutable, +CurLevel, +PlVars). | |
317 | % Restore phase/polarity for +SatVarName from cache for rapid restart. | |
318 | elim_var_from_saved_phase(SatVarName, SavedPol, Var, SolverEnv, StateMutable, CurLevel, PlVars) :- | |
319 | get_pl_var_for_sat_id(SatVarName, PlVars, Var), | |
320 | NextLevel is CurLevel + 1, | |
321 | ? | ( bt_log_sat_stack(StateMutable, SatVarName, branch, CurLevel, SavedPol, _OriginalClause), |
322 | debug_format_sat("Phase Restore: Decide variable ~w with polarity ~w on level ~w", [SatVarName,SavedPol,CurLevel]), | |
323 | Var = SavedPol, | |
324 | ? | update_full_state(StateMutable, cur_level, NextLevel), |
325 | bt_retract(saved_phase(SatVarName, SavedPol)), | |
326 | elim_vars(SolverEnv, StateMutable, PlVars) | |
327 | ; ( \+ backjump_level(_), | |
328 | \+ backjump_wd_level(_) | |
329 | ; retract(backjump_wd_level(CurLevel)), % backjump to wd decision without CDCL (custom backjumping) | |
330 | retract(backjump_wd_clause(_, BjClauseNoRef, LbdScore)), | |
331 | ? | handle_backjump_wd_clauses([BjClauseNoRef], LbdScore, CurLevel, StateMutable, SolverEnv) |
332 | ), | |
333 | %( learn_idl_core(StateMutable, CurLevel, SolverEnv) | |
334 | %; true | |
335 | %), | |
336 | ( ground(Var) | |
337 | -> true | |
338 | ; negate_polarity(SavedPol, NegSavedPol), | |
339 | ? | bt_log_sat_stack(StateMutable, SatVarName, branch, CurLevel, NegSavedPol, _OriginalClause), |
340 | debug_format_sat("Phase Restore Failed: Decide variable ~w with polarity ~w on level ~w", [SatVarName,NegSavedPol,CurLevel]), | |
341 | % remove saved phase permanently once it has failed to evaluate to true | |
342 | %retract(saved_phase(SatVarName, SavedPol)), | |
343 | Var = NegSavedPol | |
344 | ), | |
345 | ? | update_full_state(StateMutable, cur_level, NextLevel), |
346 | elim_vars(SolverEnv, StateMutable, PlVars) | |
347 | ). | |
348 | ||
349 | problem_setup(_, _, []). | |
350 | problem_setup(SolverEnv, StateMutable, [Clause|Clauses]) :- | |
351 | ? | clause_setup(SolverEnv, StateMutable, Clause), |
352 | ? | problem_setup(SolverEnv, StateMutable, Clauses). |
353 | ||
354 | clause_setup(SolverEnv, StateMutable, Clause) :- | |
355 | Clause = [Pol-Var-SatVarName|Triples], | |
356 | ? | set_watch(SolverEnv, StateMutable, Clause, Triples, Var, Pol, SatVarName). |
357 | ||
358 | % Enforce well-definedness before cdcl if unit propagation of predicate that entails the well-definedness condition caused a theory conflict. | |
359 | /*enforce_well_definedness(SolverEnv, StateMutable, SatVarName, Var) :- | |
360 | get_top_level_wd_condition(SolverEnv, SatVarName, TopLevelWdPred, PredWithWdCondition), | |
361 | !, | |
362 | debug_format_sat("Enforce well-definedness for ~w ", [SatVarName]), | |
363 | get_from_solver_env(SolverEnv, t2b_env, T2BEnv), | |
364 | get_from_solver_env(SolverEnv, sat_vars, SatVars), | |
365 | debug_format_sat("Top level wd pred ", [], TopLevelWdPred), | |
366 | debug_format_sat("Pred with wd condition ", [], PredWithWdCondition), | |
367 | predicate_to_sat(only_reuse, [], SatVars, T2BEnv, TopLevelWdPred, _NewEnv1, _, TopLevelWdBool, _NewSatVars1), | |
368 | predicate_to_sat(only_reuse, [], SatVars, T2BEnv, PredWithWdCondition, _NewEnv2, _, PredWithWdConditionBool, _NewSatVars2), | |
369 | TopLevelWdBool = b(equal(b(identifier(WdSatVarName),_,_),_),pred,[]), | |
370 | PredWithWdConditionBool = b(equal(b(identifier(PredWithWdSatVarName),_,_),_),pred,[]), | |
371 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
372 | memberchk(Var-WdSatVarName-_, PlVars), | |
373 | get_full_state(StateMutable, cur_level, CurLevel), | |
374 | set_variable_references_in_clause(PlVars, [pred_false-_-PredWithWdSatVarName,pred_true-_-WdSatVarName], OriginalClause), | |
375 | debug_format_sat("OriginalClause for well-definedness is ~w ", [OriginalClause]), | |
376 | worsen_scores_for_vars_in_clause(StateMutable, OriginalClause), | |
377 | bt_log_sat_stack(StateMutable, WdSatVarName, branch, CurLevel, pred_true, OriginalClause), | |
378 | Var = pred_true. | |
379 | %; bt_log_sat_stack(StateMutable, WdSatVarName, branch, CurLevel, pred_false, OriginalClause), | |
380 | % Var = pred_false | |
381 | %). | |
382 | enforce_well_definedness(_, _, _, _).*/ | |
383 | ||
384 | clause_contains_decided_pred(_, _, [], _, Acc, Acc). | |
385 | clause_contains_decided_pred(SolverEnv, StateMutable, [_-_-SatVarName|T], SatStack, Acc, WdDecisionLevels) :- | |
386 | get_from_sat_stack_or_explain_theory_propagation(SolverEnv, StateMutable, SatVarName, PropType, Level, AssignedPol, _), | |
387 | AssignedPol == pred_true, % assuming that we first assign true when deciding for a polarity | |
388 | PropType == branch, | |
389 | !, | |
390 | ? | clause_contains_decided_pred(SolverEnv, StateMutable, T, SatStack, [Level|Acc], WdDecisionLevels). |
391 | clause_contains_decided_pred(SolverEnv, StateMutable, [_|T], SatStack, Acc, WdDecisionLevels) :- | |
392 | ? | clause_contains_decided_pred(SolverEnv, StateMutable, T, SatStack, Acc, WdDecisionLevels). |
393 | ||
394 | assert_backjump_wd_clause(SatStack, BjLevel, BjClause) :- | |
395 | ? | compute_lbd_score(SatStack, BjClause, LbdScore), |
396 | asserta(backjump_wd_clause(BjLevel, BjClause, LbdScore)). | |
397 | ||
398 | set_polarity_of_var_explicitly(_, _, [], []). | |
399 | set_polarity_of_var_explicitly(SatVarName, Pol, [CPol-CVar-CName|T], ConflictClause) :- | |
400 | var(CVar), | |
401 | SatVarName == CName, | |
402 | !, | |
403 | ConflictClause = [CPol-Pol-CName|T]. | |
404 | set_polarity_of_var_explicitly(SatVarName, Pol, [Triple|T], [Triple|NT]) :- | |
405 | ? | set_polarity_of_var_explicitly(SatVarName, Pol, T, NT). |
406 | ||
407 | ||
408 | set_watch(_, StateMutable, OriginalClause, [], Var, Pol, SatVarName) :- | |
409 | Var == Pol, | |
410 | delete_state_instance(StateMutable, heuristic_avl, (SatVarName, _)), | |
411 | bt_retract_if_exists(saved_phase(SatVarName, _)), | |
412 | ? | worsen_scores_for_vars_in_clause(StateMutable, OriginalClause). |
413 | set_watch(SolverEnv, StateMutable, OriginalClause, [], Var, Pol, _) :- | |
414 | ground(Var), | |
415 | Var \== Pol, | |
416 | debug_format_sat("sat conflict", []), | |
417 | get_complete_theory_lemma(SolverEnv, TheoryLemmaClause), | |
418 | possibly_bt_from_smt_solution(StateMutable, TheoryLemmaClause), | |
419 | get_full_state(StateMutable, current_stack_size, StackSize), | |
420 | get_full_state(StateMutable, cur_level, CurLevel), | |
421 | compute_and_assert_backjump_clause(SolverEnv, StateMutable, StackSize, CurLevel, OriginalClause), | |
422 | fail. | |
423 | set_watch(SolverEnv, StateMutable, OriginalClause, [], Var, Pol, SatVarName) :- | |
424 | var(Var), | |
425 | get_full_state(StateMutable, cur_level, CurLevel), | |
426 | debug_format_sat("unit propagation of ~w with polarity ~w on level ~w due to clause ~w", [SatVarName,Pol,CurLevel,OriginalClause]), | |
427 | %translate:print_bexpr(TheoryFormula),nl, | |
428 | ? | bt_log_sat_stack(StateMutable, SatVarName, unit, CurLevel, Pol, OriginalClause), |
429 | ( Var = Pol, | |
430 | %( Pol == pred_true | |
431 | %-> enforce_well_definedness(SolverEnv, StateMutable, SatVarName, Var) | |
432 | %; true | |
433 | %), | |
434 | ? | delete_state_instance(StateMutable, heuristic_avl, (SatVarName, _)), |
435 | ? | bt_retract_if_exists(saved_phase(SatVarName, _)), |
436 | ? | worsen_scores_for_vars_in_clause(StateMutable, OriginalClause), |
437 | ( true | |
438 | ; % remove idl unsat core from higher decision level on backtracking | |
439 | remove_idl_unsat_core, | |
440 | fail | |
441 | ) | |
442 | ; % theory conflict: if Var = Pol triggered a SAT conflict instead, | |
443 | % a backjump clause has been computed and backjump_level/1 is asserted | |
444 | \+ backjump_level(_), % skip when backjumping | |
445 | \+ backjump_wd_level(_), | |
446 | get_last_decision_level(StateMutable, LastDLevel), % skip if no decision so far | |
447 | LastDLevel \== 1, % just backtrack if last decision level is 1 | |
448 | get_complete_theory_lemma(SolverEnv, TheoryLemmaClause), | |
449 | possibly_bt_from_smt_solution(StateMutable, TheoryLemmaClause), | |
450 | ( learn_idl_core(StateMutable, CurLevel, SolverEnv) | |
451 | -> true | |
452 | ; debug_format_sat("theory conflict on level ~w", [CurLevel]), | |
453 | get_conflict_clause_for_theory_conflict(SatVarName, Pol, SolverEnv, TConflictClause), | |
454 | get_full_state(StateMutable, sat_stack, SatStack), | |
455 | % explicitly set the polarity which failed to be assigned above in line 414 for conflict analysis (possibly part of the unsat core) | |
456 | ? | set_polarity_of_var_explicitly(SatVarName, Pol, TConflictClause, ConflictClause), |
457 | get_maximum_decision_level_other_than_current(ConflictClause, SatStack, 0, 0, ConflictLevel), | |
458 | % it can be the case that ProB first recognizes unsatisfiable after grounding waitflags; the last decision level is then not necessarily the conflict level | |
459 | ( ConflictLevel =< CurLevel, | |
460 | ? | clause_contains_decided_pred(SolverEnv, StateMutable, ConflictClause, SatStack, [], WdDecisionLevels), |
461 | WdDecisionLevels \== [] | |
462 | -> min_member(BjLevel, WdDecisionLevels), | |
463 | negate_polarities(ConflictClause, BjClause), | |
464 | asserta(backjump_wd_level(BjLevel)), | |
465 | ? | assert_backjump_wd_clause(SatStack, BjLevel, BjClause), |
466 | debug_format_sat("theory conflict on level ~w due to pred with wd", [BjLevel]) | |
467 | ; debug_format_sat("theory conflict on level ~w after unsat core computation", [ConflictLevel]), | |
468 | %ConflictLevel \== 0, | |
469 | get_full_state(StateMutable, current_stack_size, StackSize), | |
470 | %portray_sat_stack(StateMutable), | |
471 | compute_and_assert_backjump_clause_get_level(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause, _BjLevel) | |
472 | ) | |
473 | ), | |
474 | fail | |
475 | ). | |
476 | set_watch(SolverEnv, StateMutable, OriginalClause, [Pol2-Var2-Name2|Triples], Var1, Pol1, Name1):- | |
477 | ? | watch(SolverEnv, StateMutable, OriginalClause, Var1, Pol1, Name1, Var2, Pol2, Name2, Triples). |
478 | ||
479 | :- block watch(?, ?, ?, -, ?, ?, -, ?, ?, ?). | |
480 | watch(SolverEnv, StateMutable, OriginalClause, Var1, Pol1, Name1, Var2, Pol2, Name2, Triples) :- | |
481 | ( nonvar(Var1) | |
482 | ? | -> update_watch(SolverEnv, StateMutable, OriginalClause, Var1, Pol1, Name1, Var2, Pol2, Name2, Triples) |
483 | ? | ; update_watch(SolverEnv, StateMutable, OriginalClause, Var2, Pol2, Name2, Var1, Pol1, Name1, Triples) |
484 | ). | |
485 | ||
486 | update_watch(SolverEnv, StateMutable, OriginalClause, Var1, Pol1, Name1, Var2, Pol2, Name2, Triples) :- | |
487 | ( Var1 == Pol1 | |
488 | -> delete_state_instance(StateMutable, heuristic_avl, (Name1, _)), | |
489 | ? | bt_retract_if_exists(saved_phase(Name1, _)), |
490 | ? | worsen_scores_for_vars_in_clause(StateMutable, OriginalClause) |
491 | ? | ; set_watch(SolverEnv, StateMutable, OriginalClause, Triples, Var2, Pol2, Name2) |
492 | ). | |
493 | ||
494 | retract_once(Assertion) :- | |
495 | retract(Assertion), | |
496 | !. | |
497 | ||
498 | /*get_top_level_wd_condition(SolverEnv, SatVarName, TopLevelWdPred, PredWithWdCondition) :- | |
499 | get_from_solver_env(SolverEnv, sat_vars, SatVars), | |
500 | member(b(identifier(SatVarName),_,Info), SatVars), | |
501 | member(contains_top_level_wd_condition(TopLevelWdPred,PredWithWdCondition), Info).*/ | |
502 | ||
503 | %% is_backjumping. | |
504 | is_backjumping :- | |
505 | backjump_level(_). | |
506 | is_backjumping :- | |
507 | backjump_wd_level(_). | |
508 | ||
509 | %% is_last_propagated_sat_var(+StateMutable, +SatVarName). | |
510 | is_last_propagated_sat_var(StateMutable, SatVarName) :- | |
511 | get_full_state(StateMutable, sat_stack, Stack), | |
512 | % TO DO: improve, can be mutable dict | |
513 | avl_fetch(SatVarName, Stack, _). | |
514 | ||
515 | log_theory_propagation_sat_stack(StateMutable, SatVarName, SatPrologVar) :- | |
516 | get_full_state(StateMutable, cur_level, CurLevel), | |
517 | !, | |
518 | debug_format_sat("Theory propagation of ~w with polarity ~w", [SatVarName,SatPrologVar]), | |
519 | % explanation (OriginalClause) is computed lazily for conflict analysis if necessary, see explain_theory_propagation/5 | |
520 | ? | bt_log_sat_stack(StateMutable, SatVarName, theory, CurLevel, SatPrologVar, _). |
521 | ||
522 | % Calculating the unsat core in the idl solver is no overhead so it might be worthwhile to learn | |
523 | % unsat cores on the decision level as well. | |
524 | learn_idl_core(StateMutable, _CurLevel, SolverEnv) :- | |
525 | retract(idl_unsat_core(Core)), | |
526 | remove_idl_unsat_core, | |
527 | !, | |
528 | get_conflict_clause_from_unsat_core(Core, SolverEnv, ConflictClause), | |
529 | get_full_state(StateMutable, current_stack_size, StackSize), | |
530 | get_full_state(StateMutable, cur_level, CurLevel), | |
531 | compute_and_assert_backjump_clause(SolverEnv, StateMutable, StackSize, CurLevel, ConflictClause). | |
532 | ||
533 | % Log variable assignments. | |
534 | % Effect is undone on backtracking. If backjump level is zero on backtracking, i.e., | |
535 | % a random restart occured or a unit-clause has been learned, save the phase to restore | |
536 | % assignments afterwards for a rapid restart. | |
537 | bt_log_sat_stack(StateMutable, SatVarName, PropType, CurLevel, Pol, OriginalClause) :- | |
538 | add_state_instance(StateMutable, sat_stack, (SatVarName, PropType, CurLevel, Pol, OriginalClause)), | |
539 | ( increase_stack_size(StateMutable) | |
540 | ; is_restart, | |
541 | asserta_once(saved_phase(SatVarName, Pol)), | |
542 | fail | |
543 | ). | |
544 | ||
545 | increase_stack_size(StateMutable) :- | |
546 | get_full_state(StateMutable, current_stack_size, Old), | |
547 | New is Old + 1, !, | |
548 | update_full_state(StateMutable, current_stack_size, New). | |
549 | ||
550 | %% possibly_bt_from_smt_solution(+StateMutable, +TheoryLemmaClause). | |
551 | % Backtracking from an SMT solution which should not be handled as a theory conflict. | |
552 | possibly_bt_from_smt_solution(StateMutable, TheoryLemmaClause) :- | |
553 | retract(bt_from_smt_solution), | |
554 | !, | |
555 | % backjump to the last decision level without computing a conflict clause | |
556 | % but excluding the last SAT solution when backtracking after finding an SMT solution | |
557 | get_last_decision_level(StateMutable, Level), | |
558 | asserta(exclude_sat_solution_clause(TheoryLemmaClause)), | |
559 | asserta(backjump_level(Level)), | |
560 | fail. | |
561 | possibly_bt_from_smt_solution(_, _). | |
562 | ||
563 | negate_smt_formula(b(negation(Smt),pred,[]), NegSmt) :- | |
564 | !, | |
565 | NegSmt = Smt. | |
566 | negate_smt_formula(Smt, b(negation(Smt),pred,[])). | |
567 | ||
568 | %% explain_theory_propagation(+SolverEnv, +SatStack, +TheoryPropSatVar, +TheoryPropLevel, +TheoryPropPol, -ExplainingClause). | |
569 | explain_theory_propagation(SolverEnv, SatStack, TheoryPropSatVar, TheoryPropLevel, TheoryPropPol, ExplainingClause) :- | |
570 | debug_format_sat("Explain theory propagation", []), | |
571 | avl_to_list(SatStack, SatStackList), | |
572 | findall((SatVarName-Pol), (member(SatVarName-(_,Level,Pol,_), SatStackList), Level<TheoryPropLevel), SatVarNameTuples), | |
573 | get_from_solver_env(SolverEnv, sat_vars, SatVars), | |
574 | get_smt_formula_from_vars_for_sat_pol(SatVars, TheoryPropSatVar, TheoryPropPol, SmtFormula), | |
575 | negate_smt_formula(SmtFormula, NegSmt), | |
576 | get_explanation_candidate_formula(SatVars, SatVarNameTuples, CandidateFormula), | |
577 | ( SatVarNameTuples = [_] | |
578 | -> UnsatCore = b(conjunct(CandidateFormula,NegSmt),pred,[]) | |
579 | ; temporary_set_unsat_core_timeout, | |
580 | unsat_core_with_fixed_conjuncts(CandidateFormula, NegSmt, TUnsatCore), | |
581 | UnsatCore = b(conjunct(TUnsatCore,NegSmt),pred,[]), | |
582 | preferences:reset_temporary_preference(time_out) | |
583 | ), | |
584 | %nl, write('Explanation Core: '), nl,translate:print_bexpr(UnsatCore),nl, | |
585 | get_from_solver_env(SolverEnv, t2b_env, T2BEnv), | |
586 | predicate_to_sat(only_reuse, [], SatVars, T2BEnv, UnsatCore, _NewEnv, _, UnsatCoreSat, _NewSatVars), | |
587 | sat_conj_negate_to_clause(UnsatCoreSat, TExplainingClause), | |
588 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
589 | set_variable_references_in_clause(PlVars, TExplainingClause, ExplainingClause).% TO DO: learn theory lemma? | |
590 | ||
591 | get_explanation_candidate_formula(SatVars, [SatVarName-Pol|T], CandidateFormula) :- | |
592 | get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula), | |
593 | !, | |
594 | get_explanation_candidate_formula_acc(SatVars, T, SmtFormula, CandidateFormula). | |
595 | get_explanation_candidate_formula(SatVars, [_|T], CandidateFormula) :- | |
596 | % can be artificial SAT variable introduced by cnf rewriting | |
597 | get_explanation_candidate_formula(SatVars, T, CandidateFormula). | |
598 | ||
599 | get_explanation_candidate_formula_acc(_, [], Acc, Acc). | |
600 | get_explanation_candidate_formula_acc(SatVars, [SatVarName-Pol|T], Acc, CandidateFormula) :- | |
601 | get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula), | |
602 | !, | |
603 | NAcc = b(conjunct(SmtFormula,Acc),pred,[]), | |
604 | get_explanation_candidate_formula_acc(SatVars, T, NAcc, CandidateFormula). | |
605 | get_explanation_candidate_formula_acc(SatVars, [_|T], Acc, CandidateFormula) :- | |
606 | get_explanation_candidate_formula_acc(SatVars, T, Acc, CandidateFormula). | |
607 | ||
608 | get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula) :- | |
609 | memberchk(b(identifier(SatVarName),_,Info), SatVars), | |
610 | member(smt_formula(TSmtFormula), Info), | |
611 | get_smt_formula_for_sat_pol(TSmtFormula, Pol, SmtFormula). | |
612 | ||
613 | get_smt_formula_for_sat_pol(TSmtFormula, Pol, SmtFormula) :- | |
614 | ( Pol == pred_true | |
615 | -> SmtFormula = TSmtFormula | |
616 | ; TSmtFormula = b(negation(SmtFormula),pred,[]) | |
617 | -> true | |
618 | ; TSmtFormula = b(_,_,Info), | |
619 | SmtFormula = b(negation(TSmtFormula),pred,Info) | |
620 | ). | |
621 | ||
622 | %% max_heuristic_values(+StateMutable, -MaxScore, -SatVarNames). | |
623 | % Fails if there are no heuristic scores. | |
624 | max_heuristic_values(StateMutable, MaxScore, SatVarNames) :- | |
625 | get_full_state(StateMutable, heuristic_avl, AVL), | |
626 | avl_range(AVL, Range), % TO DO: improve datastructure, e.g. max heap | |
627 | max_member(MaxScore, Range), | |
628 | !, | |
629 | findall(SatVarName, (avl_member(SatVarName, AVL, S), S == MaxScore), SatVarNames). | |
630 | ||
631 | %get_heuristic_values_for_score(Heap, Score, [SatVarName|NT]) :- | |
632 | % get_from_heap(Heap, MinScore, SatVarName, NewHeap), | |
633 | % MinScore == Score, | |
634 | % !, | |
635 | % get_heuristic_values_for_score(NewHeap, Score, NT). | |
636 | %get_heuristic_values_for_score(_, _, []). | |
637 | ||
638 | % Skip on backjumping. | |
639 | get_decision_variable_from_list(SatVarNames, SatVarName) :- | |
640 | memberchk(SatVarName, SatVarNames), % important for performance to get only one member | |
641 | \+ backjump_level(_), | |
642 | \+ backjump_wd_level(_), | |
643 | \+ idl_unsat_core(_). | |
644 | ||
645 | bt_retract_if_exists(Assertion) :- | |
646 | ? | ( dpllt_sat_solver:Assertion |
647 | ? | -> bt_retract(Assertion) |
648 | ; true | |
649 | ). | |
650 | ||
651 | % Not undone on backtracking. | |
652 | /* | |
653 | If this is used we need to store the mutable since operations are undone on backtracking. | |
654 | possibly_decay_heuristic_values(StateMutable) :- | |
655 | decision_heuristic(Heuristic), | |
656 | Heuristic == vsids, | |
657 | conflict_stats(total(AC), _, _), | |
658 | AC \== 0, | |
659 | vsids_decay_frequency(I), | |
660 | C is AC mod I, | |
661 | C == 0, | |
662 | debug_format_sat("~nDecay heuristic scores", []), | |
663 | !, | |
664 | vsids_decay_value(Val), | |
665 | decay_heuristic_values(StateMutable, Val). | |
666 | possibly_decay_heuristic_values(_). | |
667 | ||
668 | % Not undone on backtracking. | |
669 | decay_heuristic_values(StateMutable, DecayValue) :- | |
670 | retract(heuristic_tuple(SatVarName, Score)), | |
671 | !, | |
672 | NewScore is Score / DecayValue, | |
673 | decay_heuristic_values(DecayValue), | |
674 | asserta(heuristic_tuple(SatVarName, NewScore)). | |
675 | decay_heuristic_values(_, _).*/ | |
676 | ||
677 | % Each variable in each polarity has a counter, initialized to 0. | |
678 | /*init_heuristic(SolverEnv) :- | |
679 | get_from_solver_env(SolverEnv, sat_varnames, SatVarNames), | |
680 | init_heuristic_tuples_from_vars(SatVarNames). | |
681 | ||
682 | init_heuristic_tuples_from_vars([]). | |
683 | init_heuristic_tuples_from_vars([SatVarName|T]) :- | |
684 | asserta(heuristic_tuple(SatVarName, 0)), | |
685 | %asserta(heuristic_tuple(SatVarName, pred_true, 0)), | |
686 | %asserta(heuristic_tuple(SatVarName, pred_false, 0)), | |
687 | init_heuristic_tuples_from_vars(T).*/ | |
688 | ||
689 | % Each variable is initially assigned the number of its occurrences in all clauses as its score. | |
690 | % Variable scores are not split for polarities. | |
691 | init_decision_heuristic(StateMutable, Clauses) :- | |
692 | count_occurrences_in_clauses(Clauses, VarScoreTuples), | |
693 | ? | add_heuristic_tuples(StateMutable, VarScoreTuples). |
694 | ||
695 | add_heuristic_tuples(_, []). | |
696 | add_heuristic_tuples(StateMutable, [(SatVarName,Score)|T]) :- | |
697 | add_state_instance(StateMutable, heuristic_avl, (SatVarName,Score)), | |
698 | ? | add_heuristic_tuples(StateMutable, T). |
699 | ||
700 | :- dynamic occurrences/2. | |
701 | :- volatile occurrences/2. | |
702 | ||
703 | count_occurrences_in_clauses(Clauses, VarScoreTuples) :- | |
704 | retractall(occurrences(_, _)), | |
705 | assert_count_occurrences(Clauses), | |
706 | findall((SatVarName,Score), retract(occurrences(SatVarName, Score)), VarScoreTuples), !. | |
707 | ||
708 | assert_count_occurrences([]). | |
709 | assert_count_occurrences([Clause|T]) :- | |
710 | assert_count_occurrences_from_clause(Clause), | |
711 | assert_count_occurrences(T). | |
712 | ||
713 | % TO DO: use avl tree instead of assert | |
714 | assert_count_occurrences_from_clause([]). | |
715 | assert_count_occurrences_from_clause([_-_-SatVarName|T]) :- | |
716 | ( retract(occurrences(SatVarName, Score)) | |
717 | -> Score1 is Score + 1, | |
718 | asserta(occurrences(SatVarName, Score1)) | |
719 | ; asserta(occurrences(SatVarName, 1)) | |
720 | ), | |
721 | assert_count_occurrences_from_clause(T). | |
722 | ||
723 | get_unassigned_vars([], _, []). | |
724 | get_unassigned_vars([SatVarName|T], PlVars, UnassignedVars) :- | |
725 | get_pl_var_for_sat_id(SatVarName, PlVars, PlVar), | |
726 | var(PlVar), | |
727 | !, | |
728 | get_unassigned_vars(T, PlVars, NT), | |
729 | UnassignedVars = [SatVarName|NT]. | |
730 | get_unassigned_vars([_|T], PlVars, UnassignedVars) :- | |
731 | get_unassigned_vars(T, PlVars, UnassignedVars). | |
732 | ||
733 | update_heuristic_scores_for_vars(StateMutable, UsedVars, PlVars) :- | |
734 | get_unassigned_vars(UsedVars, PlVars, UnassignedVars), | |
735 | decision_heuristic(Type), | |
736 | update_heuristic_scores(StateMutable, Type, UnassignedVars). | |
737 | ||
738 | % Update heuristic scores from learned clauses for VSIDS branching heuristic. | |
739 | update_heuristic_scores_for_clauses(StateMutable, ClausesToLearn) :- | |
740 | % we don't want to bump scores for already assigned variables, i.e., don't add them to the heuristic again | |
741 | get_non_ground_varnames_occurring_in_clauses(ClausesToLearn, SatVarNames), | |
742 | decision_heuristic(Type), | |
743 | ? | update_heuristic_scores(StateMutable, Type, SatVarNames). |
744 | ||
745 | get_non_ground_varnames_occurring_in_clauses(ClausesToLearn, SatVarNames) :- | |
746 | get_non_ground_varnames_occurring_in_clauses(ClausesToLearn, [], SatVarNames). | |
747 | ||
748 | get_non_ground_varnames_occurring_in_clauses([], Acc, Acc). | |
749 | get_non_ground_varnames_occurring_in_clauses([Clause|T], Acc, SatVarNames) :- | |
750 | get_non_ground_varnames_occurring_in_clause(Clause, Acc, NewAcc), | |
751 | get_non_ground_varnames_occurring_in_clauses(T, NewAcc, SatVarNames). | |
752 | ||
753 | get_non_ground_varnames_occurring_in_clause([], Acc, Acc). | |
754 | get_non_ground_varnames_occurring_in_clause([_-Var-SatVarName|T], Acc, SatVarNames) :- | |
755 | var(Var), | |
756 | !, | |
757 | ord_add_element(Acc, SatVarName, NewAcc), | |
758 | get_non_ground_varnames_occurring_in_clause(T, NewAcc, SatVarNames). | |
759 | get_non_ground_varnames_occurring_in_clause([_|T], Acc, SatVarNames) :- | |
760 | get_non_ground_varnames_occurring_in_clause(T, Acc, SatVarNames). | |
761 | ||
762 | %% update_heuristic_scores(+StateMutable, +Type, +SatVarNames). | |
763 | % Type is either vsids or evsids. | |
764 | % SatVarNames are the variable names occurring in learned clauses. | |
765 | % Effect is undone on backtracking. | |
766 | update_heuristic_scores(StateMutable, Type, SatVarNames) :- | |
767 | conflict_stats(total(TotalConflicts), _, _), | |
768 | get_full_state(StateMutable, heuristic_avl, Avl), | |
769 | ? | update_heuristic_scores(Avl, TotalConflicts, Type, NAvl, SatVarNames), |
770 | update_full_state(StateMutable, heuristic_avl, NAvl). | |
771 | ||
772 | update_heuristic_scores(AvlAcc, _, _, AvlAcc, []). | |
773 | update_heuristic_scores(AvlAcc, TotalConflicts, Type, NAvl, [SatVarName|T]) :- | |
774 | avl_fetch(SatVarName, AvlAcc, OldScore), | |
775 | !, | |
776 | bump_heuristic_score_for_type(Type, TotalConflicts, OldScore, NewScore), | |
777 | avl_change(SatVarName, AvlAcc, _, NAvlAcc, NewScore), | |
778 | ? | update_heuristic_scores(NAvlAcc, TotalConflicts, Type, NAvl, T). |
779 | update_heuristic_scores(AvlAcc, TotalConflicts, Type, NAvl, [_|T]) :- | |
780 | % guided backjump to decision due to wd, not all vars necessarily propagated | |
781 | ? | update_heuristic_scores(AvlAcc, TotalConflicts, Type, NAvl, T). |
782 | ||
783 | % v_s + 1 | |
784 | bump_heuristic_score_for_type(vsids, _, OldScore, NewScore) :- | |
785 | NewScore is OldScore + 1. | |
786 | % v_s + f^(-k), where f is evsids_f_value/1 and it is the k-th conflict | |
787 | bump_heuristic_score_for_type(evsids, TotalConflicts, OldScore, NewScore) :- | |
788 | evsids_f_value(FVal), | |
789 | NewScore is ceiling(OldScore + FVal**(-TotalConflicts)). | |
790 | ||
791 | get_pl_var_for_sat_id(SatVarName, PlVars, Var) :- | |
792 | ? | member((Var-SatVarName-_), PlVars), !. % TO DO: improve? |
793 | ||
794 | % We have positive scores, maximum value is best. Remove if zero. | |
795 | % Effect is undone on backtracking. | |
796 | worsen_scores_for_vars_in_clause(_, []). | |
797 | worsen_scores_for_vars_in_clause(StateMutable, [_-_-SatVarName|T]) :- | |
798 | get_full_state(StateMutable, heuristic_avl, Avl), | |
799 | ( avl_fetch(SatVarName, Avl, Score) | |
800 | -> ( Score \== 1, | |
801 | NScore is Score - 1, | |
802 | avl_change(SatVarName, Avl, _, NAvl, NScore), | |
803 | update_full_state(StateMutable, heuristic_avl, NAvl) | |
804 | ; Score == 1, | |
805 | delete_state_instance(StateMutable, heuristic_avl, (SatVarName, Score)) | |
806 | ), | |
807 | ? | worsen_scores_for_vars_in_clause(StateMutable, T) |
808 | ? | ; worsen_scores_for_vars_in_clause(StateMutable, T) |
809 | ). | |
810 | ||
811 | % Literal Block Distance (LBD) as defined in "Predicting Learnt Clauses Quality in Modern SAT Solvers", | |
812 | % i.e., the amount of different decision levels in a clause. | |
813 | compute_lbd_score(SatStack, BjClause, LbdScore) :- | |
814 | ? | compute_lbd_score(SatStack, BjClause, [], LbdScore). |
815 | ||
816 | compute_lbd_score(_, [], Acc, LbdScore) :- | |
817 | length(Acc, LbdScore). | |
818 | compute_lbd_score(SatStack, [_-_-SatVarName|T], Acc, LbdScore) :- | |
819 | avl_fetch(SatVarName, SatStack, (_,Level,_,_)), | |
820 | !, | |
821 | ord_add_element(Acc, Level, NewAcc), | |
822 | ? | compute_lbd_score(SatStack, T, NewAcc, LbdScore). |
823 | compute_lbd_score(SatStack, [_|T], Acc, LbdScore) :- % TO DO: check this, happens when using idl solver unsat core? | |
824 | compute_lbd_score(SatStack, T, Acc, LbdScore). | |
825 | ||
826 | % Remove half of the clauses every "frequency_constant + constant_factor * x" conflicts, | |
827 | % where x is the amount of clause reductions so far. We keep clauses with a small LBD forever. | |
828 | possibly_discard_learned_clauses :- | |
829 | conflict_stats(_, _, since_reduction(SRed)), | |
830 | dpllt_settings:discard_learned_clauses_frequency_constant(Frequency), | |
831 | SRed >= Frequency, % first check to improve performance | |
832 | amount_clause_reductions(Reductions), | |
833 | dpllt_settings:discard_learned_clauses_constant_factor(Factor), | |
834 | Threshold is Frequency + Factor * Reductions, | |
835 | SRed == Threshold, | |
836 | !, | |
837 | debug_format_sat("~nDiscard half of learned clauses..", []), | |
838 | dpllt_settings:discard_clause_greater_lbd(LbdLimit), | |
839 | amount_learned_clauses(ALC), | |
840 | Half is ALC // 2, | |
841 | discard_half_of_learned_clauses_greater_lbd(0, Half, LbdLimit, Removed), | |
842 | retract(amount_learned_clauses(Old)), | |
843 | New is Old - Removed, | |
844 | asserta(amount_learned_clauses(New)), | |
845 | retract(conflict_stats(total(Total), since_restart(SRed), _)), | |
846 | asserta(conflict_stats(total(Total), since_restart(SRed), since_reduction(0))), !. | |
847 | possibly_discard_learned_clauses. | |
848 | ||
849 | % Remove half of the clauses learned so far. | |
850 | % We keep clauses with an LBD smaller than dpllt_settings:discard_clause_greater_lbd/1 | |
851 | % forever. Thus it is not guaranteed that exactly half of the clauses are deleted if | |
852 | % a lot of high quality clauses have been learned. | |
853 | discard_half_of_learned_clauses_greater_lbd(C, Half, LbdLimit, Removed) :- | |
854 | C =< Half, | |
855 | backjump_clause(BjLevel, BjClause, LbdScore, UsedVars), | |
856 | !, | |
857 | retract(backjump_clause(BjLevel, BjClause, LbdScore, UsedVars)), | |
858 | ( LbdScore > LbdLimit | |
859 | -> C1 is C + 1, | |
860 | discard_half_of_learned_clauses_greater_lbd(C1, Half, LbdLimit, Removed) | |
861 | ; discard_half_of_learned_clauses_greater_lbd(C, Half, LbdLimit, Removed), | |
862 | asserta(backjump_clause(BjLevel, BjClause, LbdScore, UsedVars)) | |
863 | ). | |
864 | discard_half_of_learned_clauses_greater_lbd(C, _, _, C). | |
865 | ||
866 | %% count_found_conflict(-NewTotal, -NewSinceRestart, -NewSinceReduction). | |
867 | count_found_conflict(Total1, SRes1, SRed1) :- | |
868 | retract(conflict_stats(total(Total), since_restart(SRes), since_reduction(SRed))), | |
869 | Total1 is Total + 1, | |
870 | SRes1 is SRes + 1, | |
871 | SRed1 is SRed + 1, | |
872 | asserta(conflict_stats(total(Total1), since_restart(SRes1), since_reduction(SRed1))). | |
873 | ||
874 | %% compute_and_assert_backjump_clause(+SolverEnv, +StateMutable, +StackSize, +ConflictClause). | |
875 | compute_and_assert_backjump_clause(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause) :- | |
876 | compute_and_assert_backjump_clause_get_level(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause, _). | |
877 | ||
878 | cnf_to_smt(BoolPred, Smt) :- | |
879 | BoolPred = b(Expr,_,_), | |
880 | ? | cnf_to_smt_e(Expr, Smt). |
881 | ||
882 | cnf_to_smt_e(falsity, b(falsity,pred,[])). | |
883 | cnf_to_smt_e(truth, b(truth,pred,[])). | |
884 | cnf_to_smt_e(conjunct(A,B), Smt) :- | |
885 | ? | cnf_to_smt(A, NA), |
886 | ? | cnf_to_smt(B, NB), |
887 | safe_create_texpr(conjunct(NA,NB), pred, [], Smt). | |
888 | cnf_to_smt_e(disjunct(A,B), Smt) :- | |
889 | ? | cnf_to_smt(A, NA), |
890 | ? | cnf_to_smt(B, NB), |
891 | safe_create_texpr(disjunct(NA,NB), pred, [], Smt). | |
892 | cnf_to_smt_e(equal(b(identifier(_),_,Info),b(BoolExpr,boolean,_)), Smt) :- | |
893 | ? | member(smt_formula(TSmt), Info), |
894 | ( BoolExpr == boolean_true | |
895 | -> Smt = TSmt | |
896 | ; safe_create_texpr(negation(TSmt), pred, [], Smt) | |
897 | ). | |
898 | ||
899 | /*cnf_to_smt([], _, Acc, SmtFromCnf) :- | |
900 | conjunct_predicates(Acc, SmtFromCnf). | |
901 | cnf_to_smt([Clause|T], PrologSatVarTriple, Acc, SmtFromCnf) :- | |
902 | clause_to_smt(PrologSatVarTriple, Clause, SmtClause), | |
903 | cnf_to_smt(T, PrologSatVarTriple, [SmtClause|Acc], SmtFromCnf).*/ | |
904 | ||
905 | clause_to_smt(PlVars, Clause, SmtFormula) :- | |
906 | clause_to_smt(PlVars, Clause, [], SmtFormula). | |
907 | ||
908 | clause_to_smt(_, [], Acc, SmtFormula) :- | |
909 | disjunct_predicates(Acc, SmtFormula). | |
910 | clause_to_smt(PlVars, [Pol-_-SatVarName|T], Acc, SmtClause) :- | |
911 | member(_-SatVarName-TSmtFormula, PlVars), | |
912 | get_smt_formula_for_sat_pol(TSmtFormula, Pol, SmtFormula), | |
913 | clause_to_smt(PlVars, T, [SmtFormula|Acc], SmtClause). | |
914 | ||
915 | %% compute_and_assert_backjump_clause_get_level(+SolverEnv, +StateMutable, +StackSize, +ConflictLevel, +ConflictClause, -BjLevel). | |
916 | /*compute_and_assert_backjump_clause_get_level(_SolverEnv, StateMutable, _StackSize, ConflictLevel, ConflictClause, BjLevel) :- | |
917 | % Theory conflict in unsat core can be on level zero while the SMT actually found the contradiction on a higher level | |
918 | % after the grounding phase of ProB's constraint solver. | |
919 | % In this case, we learn the negated unsat core and backjump to level 0. | |
920 | get_last_decision_level(StateMutable, _), | |
921 | ConflictLevel == 0, | |
922 | !, | |
923 | BjLevel = 0, | |
924 | negate_assignments_to_polarities(ConflictClause, BjClause), | |
925 | debug_format_sat("Found theory conflict in unsat core on level 0.", []), | |
926 | debug_format_sat("Backjump clause is ~w", [BjClause]), | |
927 | debug_format_sat("Backjump level is ~w", [BjLevel]), | |
928 | get_full_state(StateMutable, sat_stack, SatStack), | |
929 | compute_lbd_score(SatStack, BjClause, LbdScore), | |
930 | asserta(backjump_clause(BjLevel, BjClause, LbdScore, [])), | |
931 | asserta(backjump_level(BjLevel)).*/ | |
932 | compute_and_assert_backjump_clause_get_level(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause, BjLevel) :- | |
933 | get_last_decision_level(StateMutable, _), | |
934 | possibly_discard_learned_clauses, | |
935 | debug_format_sat("~nConflict clause is ~w", [ConflictClause]), | |
936 | debug_format_sat("~nStart CDCL..", []), | |
937 | ? | ( (get_backjump_clause_conflict_resolution(SolverEnv, StateMutable, ConflictLevel, ConflictClause, BjClause, BjLevel, UsedVars), BjLevel \== -1) |
938 | ; add_error_fail(compute_and_assert_backjump_clause_get_level, 'SMT solver\'s conflict resolution failed', []) | |
939 | ),%trace,get_backjump_clause_conflict_resolution(SolverEnv, StateMutable, ConflictLevel, ConflictClause, BjClause, BjLevel, UsedVars)), | |
940 | debug_format_sat("done.", []), | |
941 | debug_format_sat("Backjump clause is ~w", [BjClause]), | |
942 | debug_format_sat("Backjump level is ~w", [BjLevel]), | |
943 | get_full_state(StateMutable, sat_stack, SatStack), | |
944 | ? | compute_lbd_score(SatStack, BjClause, LbdScore), |
945 | asserta(backjump_clause(BjLevel, BjClause, LbdScore, UsedVars)), | |
946 | asserta(backjump_level(BjLevel)), | |
947 | ( incremental_mode, | |
948 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
949 | clause_to_smt(PlVars, BjClause, SmtFormula), | |
950 | SmtFormula \= b(negation(b(truth,pred,_)),pred,_), | |
951 | SmtFormula \= b(truth,pred,_) % uses _cnf_opt variable, don't store those | |
952 | -> solver_name(SolverName), | |
953 | asserta(memoize_backjump_clause(SolverName, SmtFormula, LbdScore)) | |
954 | ; true | |
955 | ), | |
956 | count_found_conflict(NewTotal, NewSinceRestart, _), | |
957 | store_recent_stack_size(StackSize), | |
958 | count_learned_clause, | |
959 | ( \+ clear_lbd_values_or_fail(StateMutable), | |
960 | BjLevel \== 0 | |
961 | -> store_recent_lbd_score(LbdScore), | |
962 | update_total_lbd_sum(LbdScore), | |
963 | (random_restart(NewTotal, NewSinceRestart), !; true) | |
964 | ; true | |
965 | ), !. | |
966 | ||
967 | count_learned_clause :- | |
968 | retract(amount_learned_clauses(Old)), | |
969 | New is Old + 1, | |
970 | asserta(amount_learned_clauses(New)). | |
971 | ||
972 | %% store_recent_lbd_score(+LbdScore). | |
973 | % The stored list of recent LBDs is a difference list and we insert at the end of list. | |
974 | % The first LBD is thus the oldest one and removed when exceeding the maximum size | |
975 | % defined by recent_lbd_threshold/1. | |
976 | store_recent_lbd_score(LbdScore) :- | |
977 | retract(recent_lbds_dl(Lbds-Diff, Amount)), | |
978 | glucose_restart_recent_lbds_threshold(Thresh), | |
979 | Diff = [LbdScore|NDiff], | |
980 | ( Amount < Thresh | |
981 | -> Amount1 is Amount + 1, | |
982 | asserta(recent_lbds_dl(Lbds-NDiff, Amount1)) | |
983 | ; Lbds = [_|RLbds], | |
984 | asserta(recent_lbds_dl(RLbds-NDiff, Amount)) | |
985 | ). | |
986 | ||
987 | store_recent_stack_size(StackSize) :- | |
988 | retract(recent_stack_sizes_dl(StackSizes-Diff, Amount)), | |
989 | glucose_restart_trail_threshold(Thresh), | |
990 | Diff = [StackSize|NDiff], | |
991 | ( Amount < Thresh | |
992 | -> Amount1 is Amount + 1, | |
993 | asserta(recent_stack_sizes_dl(StackSizes-NDiff, Amount1)) | |
994 | ; StackSizes = [_|RStackSizes], | |
995 | asserta(recent_stack_sizes_dl(RStackSizes-NDiff, Amount)) | |
996 | ). | |
997 | ||
998 | %% update_total_lbd_sum(+LbdScore). | |
999 | update_total_lbd_sum(LbdScore) :- | |
1000 | retract(total_lbd_sum(Old)), | |
1001 | New is Old + LbdScore, | |
1002 | asserta(total_lbd_sum(New)). | |
1003 | ||
1004 | %% random_restart(+AmountOfConflicts, +AmountOfConflictsSinceRestart). | |
1005 | % "Randomly" restart after an amount of conflicts since the last restart. | |
1006 | random_restart(_AC, ACR) :- | |
1007 | restart_policy(luby), | |
1008 | random_luby_restart(ACR), !. | |
1009 | random_restart(AC, _ACR) :- | |
1010 | restart_policy(glucose), | |
1011 | random_glucose_restart(AC), !. | |
1012 | ||
1013 | :- dynamic restarts/1. | |
1014 | ||
1015 | do_random_restart :- | |
1016 | retract(restarts(OldR)), | |
1017 | NewR is OldR + 1, | |
1018 | asserta(restarts(NewR)), | |
1019 | retract(backjump_level(_)), | |
1020 | asserta(backjump_level(0)), | |
1021 | retract(conflict_stats(total(Total), _, since_reduction(SRed))), | |
1022 | asserta(conflict_stats(total(Total), since_restart(0), since_reduction(SRed))), | |
1023 | asserta_once(is_restart), | |
1024 | debug_format_sat("~nRandom restart", []). | |
1025 | ||
1026 | %% random_glucose_restart(+AmountOfConflicts). | |
1027 | % Restart search if recent_lbds_dl/2 contains exactly glucose_restart_recent_lbds_threshold/1 amount | |
1028 | % of most recent LBDs and RecentAvg * Proportion > TotalAvg is satisfied, i.e., the recently learned clauses' | |
1029 | % LBDs got too large. | |
1030 | random_glucose_restart(AC) :- | |
1031 | total_lbd_sum(TotalLbdSum), % TO DO: reset the sum at any time? | |
1032 | TotalAvg is TotalLbdSum / AC, | |
1033 | recent_lbds_dl(RLbds-[], LbdAmount), | |
1034 | glucose_restart_recent_lbds_threshold(LbdThresh), | |
1035 | LbdAmount == LbdThresh, % queue of recent LBDs is full | |
1036 | sumlist(RLbds, RSum), | |
1037 | RecentAvg is RSum / LbdAmount, | |
1038 | glucose_restart_margin_ratio(Proportion), | |
1039 | debug_format_sat("~nTotalAvg: ~w~nRecentAvg: ~w", [TotalAvg,RecentAvg]), | |
1040 | ( RecentAvg * Proportion > TotalAvg | |
1041 | -> do_random_restart, | |
1042 | clear_recent_lbds_state | |
1043 | ; true | |
1044 | ). | |
1045 | ||
1046 | % Favor SAT instances too by possibly clearing the recent LBD queue. | |
1047 | % Assumption: The queue of recent LBDs is full. | |
1048 | clear_lbd_values_or_fail(StateMutable) :- | |
1049 | glucose_restart_trail_threshold(TrailThresh), | |
1050 | glucose_restart_stack_avg_factor(StackSizeFactor), | |
1051 | recent_stack_sizes_dl(StackSizes-[], AmountStackSizes), | |
1052 | AmountStackSizes == TrailThresh, % queue of recent stack sizes on conflict is full | |
1053 | get_full_state(StateMutable, current_stack_size, StackSize), | |
1054 | sumlist(StackSizes, SSum), | |
1055 | StackSizesAvg is SSum / AmountStackSizes, | |
1056 | StackSize > StackSizeFactor * StackSizesAvg, | |
1057 | clear_recent_lbds_state. | |
1058 | ||
1059 | clear_recent_lbds_state :- | |
1060 | retract(recent_lbds_dl(_, _)), | |
1061 | asserta(recent_lbds_dl(Diff-Diff, 0)). | |
1062 | ||
1063 | %% random_luby_restart(+AmountOfConflictsSinceRestart). | |
1064 | % The amount of conflicts when to restart is defined by the Luby sequence, | |
1065 | % 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") | |
1066 | % using a unit length of 32 (see luby_counter/1). | |
1067 | random_luby_restart(ACR) :- | |
1068 | restart_policy(luby), | |
1069 | get_next_luby_value(Luby), | |
1070 | !, | |
1071 | ( ACR == Luby | |
1072 | -> retract_once(luby_counter(_)), | |
1073 | do_random_restart | |
1074 | ; true | |
1075 | ). | |
1076 | random_luby_restart(_) :- | |
1077 | add_error_fail(random_restart, 'No more values in predefined Luby sequence', []). | |
1078 | ||
1079 | get_next_luby_value(LubyValue) :- | |
1080 | luby_counter(Luby), | |
1081 | luby_restart_unit_length(UnitLength), | |
1082 | LubyValue is UnitLength * Luby, % TO DO: faster to precompute once a unit length is fixed | |
1083 | !. | |
1084 | ||
1085 | %% learn_asserted_clauses(+CurrentBjLevel, +SolverEnv, +Clauses, -NewClauses). | |
1086 | learn_asserted_clauses(StateMutable, CurrentBjLevel, SolverEnv, Clauses, NewClauses) :- | |
1087 | ? | get_clauses_to_learn_bump_scores(StateMutable, CurrentBjLevel, SolverEnv, ClausesToLearn), |
1088 | append(ClausesToLearn, Clauses, NewClauses), !. | |
1089 | ||
1090 | %% get_sat_solution_exclusion_clauses(-ExclClausesNoRef). | |
1091 | % We exclude SAT solutions when backtracking from finding an SMT solution to find a different assignment. | |
1092 | get_sat_solution_exclusion_clauses(ExclClausesNoRef) :- | |
1093 | findall(ExclClause, exclude_sat_solution_clause(ExclClause), ExclClausesNoRef), !. | |
1094 | ||
1095 | %% get_clauses_to_learn_bump_scores(+StateMutable, +CurrentBjLevel, +SolverEnv, -ClausesToLearn). | |
1096 | % Note that the Prolog variable references are set correctly in here. | |
1097 | % We thus do not have to take care for correct references when analyzing a conflict | |
1098 | % and creating a backjump clause beforehand. | |
1099 | % We learn all backjump clauses which have been learned on a decision level higher or equal to CurrentBjLevel. | |
1100 | % Note that the clauses learned on a lower level are already included in the set of clauses. | |
1101 | % Yet, when backjumping, we do not want to forget clauses learned on a decision level between the current backjump | |
1102 | % level and the last conflict level. | |
1103 | % -UsedVars are the SAT variables used during all conlict analyses of clauses to learn. | |
1104 | get_clauses_to_learn_bump_scores(StateMutable, CurrentBjLevel, SolverEnv, ClausesToLearn) :- | |
1105 | get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, TempBjClauses, UsedVars), | |
1106 | %length(TempBjClauses, Len), | |
1107 | %debug_format_sat("Learn ~w clauses", [Len]), | |
1108 | get_sat_solution_exclusion_clauses(ExclClauses), | |
1109 | append(ExclClauses, TempBjClauses, BjClausesNoRef), | |
1110 | ? | set_references_and_bump_scores(BjClausesNoRef, UsedVars, StateMutable, SolverEnv, ClausesToLearn). |
1111 | ||
1112 | set_references_and_bump_scores(BjClausesNoRef, UsedVars, StateMutable, SolverEnv, ClausesToLearn) :- | |
1113 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
1114 | ? | set_variable_references_in_clauses(PlVars, BjClausesNoRef, ClausesToLearn), |
1115 | ? | update_heuristic_scores_for_clauses(StateMutable, ClausesToLearn), |
1116 | ( bump_scores_for_bj_clause_only(true) | |
1117 | ; % additionally bump scores for all variables used during conflict analysis | |
1118 | bump_scores_for_bj_clause_only(false), | |
1119 | update_heuristic_scores_for_vars(StateMutable, UsedVars, PlVars) | |
1120 | ). | |
1121 | ||
1122 | %% get_asserted_backjump_clauses_greater_eq_level(+CurrentBjLevel, -BjClauses). | |
1123 | % Get and remove, but undo on backtracking. | |
1124 | get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, BjClauses, UsedVars) :- | |
1125 | get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, [], BjClauses, [], UsedVars). | |
1126 | ||
1127 | get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, BAcc, BjClauses, UAcc, UsedVars) :- | |
1128 | ? | ( backjump_clause(BjLevel, BjClause, _, _) |
1129 | ? | -> bt_retract(backjump_clause(BjLevel, BjClause, _, BUsedVars)), |
1130 | ( BjLevel >= CurrentBjLevel | |
1131 | -> append(BUsedVars, UAcc, NUAcc), | |
1132 | get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, [BjClause|BAcc], BjClauses, NUAcc, UsedVars) | |
1133 | ; get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, BAcc, BjClauses, UAcc, UsedVars), | |
1134 | ? | bt_asserta(backjump_clause(BjLevel, BjClause, _, BUsedVars)) |
1135 | ) | |
1136 | ; BjClauses = BAcc, | |
1137 | UsedVars = UAcc | |
1138 | ), !. | |
1139 | ||
1140 | %% set_variable_references_in_clauses(+PlVars, +Clauses, -RefClauses). | |
1141 | set_variable_references_in_clauses(_, [], []). | |
1142 | set_variable_references_in_clauses(PlVars, [Clause|T], [RefClause|NT]) :- | |
1143 | ? | set_variable_references_in_clause(PlVars, Clause, RefClause), |
1144 | ? | set_variable_references_in_clauses(PlVars, T, NT). |
1145 | ||
1146 | %% set_variable_references_in_clause(+PlVars, +Clause, -RefClauses). | |
1147 | % We need to set the correct variable references in a new learned clause | |
1148 | % to trigger co-routines etc. | |
1149 | set_variable_references_in_clause(_, [], []). | |
1150 | set_variable_references_in_clause(PlVars, [Pol-_-Name|T], [Pol-Var-Name|NT]) :- | |
1151 | ? | member(Var-Name-_, PlVars), |
1152 | !, | |
1153 | ? | set_variable_references_in_clause(PlVars, T, NT). |
1154 | set_variable_references_in_clause(PlVars, [_|T], NT) :- | |
1155 | % symmetry breaking might introduce new SAT variables which are not connected to any SMT variable | |
1156 | set_variable_references_in_clause(PlVars, T, NT). | |
1157 | ||
1158 | get_from_solver_env(SolverEnv, Key, OutValue) :- | |
1159 | ? | member(Key:Value, SolverEnv), |
1160 | !, | |
1161 | OutValue = Value. | |
1162 | get_from_solver_env(SolverEnv, Key, _) :- | |
1163 | add_error_fail(get_from_solver_env, | |
1164 | 'Wrong key or corrupt solver environment in DPLL(T) SAT solver', | |
1165 | [env:SolverEnv,key:Key]). | |
1166 | ||
1167 | bt_asserta(Assertion) :- | |
1168 | asserta(Assertion); (retract(Assertion), fail). | |
1169 | ||
1170 | bt_retract(Assertion) :- | |
1171 | ( retract(Assertion) | |
1172 | -> ( true | |
1173 | ; asserta(Assertion), | |
1174 | fail | |
1175 | ) | |
1176 | ; fail | |
1177 | ). | |
1178 | ||
1179 | %% Assert all list elements as wd_condition/1. | |
1180 | /*register_wd_conditions([]). | |
1181 | register_wd_conditions([WDImpl|T]) :- | |
1182 | WDImpl = b(disjunct(_,Pred),_,_), | |
1183 | norm_pred_check(Pred,NPred), | |
1184 | asserta(wd_condition(NPred)), | |
1185 | register_wd_conditions(T). | |
1186 | ||
1187 | contains_pred_with_wd_or_for_wd(Conj) :- | |
1188 | ground(Conj), | |
1189 | conjunction_to_list(Conj, L), | |
1190 | contains_pred_with_wd_or_for_wd_l(L). | |
1191 | ||
1192 | contains_pred_with_wd_or_for_wd_l([Pred|_]) :- | |
1193 | Pred = b(_,_,I), | |
1194 | ( member(contains_wd_condition, I) | |
1195 | ; member(discharged_wd_po, I) | |
1196 | ; member(discharged(_,_), I) | |
1197 | ), | |
1198 | !. | |
1199 | contains_pred_with_wd_or_for_wd_l([Pred|_]) :- | |
1200 | norm_pred_check(Pred,NPred), | |
1201 | wd_condition(NPred), | |
1202 | !. | |
1203 | contains_pred_with_wd_or_for_wd_l([_|T]) :- | |
1204 | contains_pred_with_wd_or_for_wd_l(T).*/ | |
1205 | ||
1206 | has_wd_condition(_, Pred) :- | |
1207 | empty_hyps(Hyps), | |
1208 | compute_wd(Pred, Hyps, [], _WDPo), !. | |
1209 | %has_wd_condition(_, Pred) :- | |
1210 | % contains_pred_with_wd_or_for_wd(Pred), !. | |
1211 | %has_wd_condition(PredList, _) :- | |
1212 | % member(b(member(_,b(domain(_),_,_)),pred,_), PredList), !. % TO DO: add more | |
1213 | ||
1214 | get_core_for_cdcl(Cores, UnsatCore, RestCores) :- | |
1215 | get_core_for_cdcl_aux(Cores, _, TUnsatCore, TRestCores), | |
1216 | ( ground(TUnsatCore) | |
1217 | -> UnsatCore = TUnsatCore, | |
1218 | RestCores = TRestCores | |
1219 | ; TRestCores = [UnsatCore|RestCores] | |
1220 | ). | |
1221 | ||
1222 | get_core_for_cdcl_aux([], CoreAcc, CoreAcc, []). | |
1223 | get_core_for_cdcl_aux([CoreList|T], CoreAcc, UnsatCore, RestCores) :- | |
1224 | conjunct_predicates(CoreList, Core), | |
1225 | ( var(CoreAcc), | |
1226 | has_wd_condition(CoreList, Core), | |
1227 | CoreList \= [_] % not a single WD condition, can't learn from that | |
1228 | -> get_core_for_cdcl_aux(T, Core, UnsatCore, RestCores) | |
1229 | ; get_core_for_cdcl_aux(T, CoreAcc, UnsatCore, TRestCores), | |
1230 | RestCores = [Core|TRestCores] | |
1231 | ). | |
1232 | ||
1233 | %% get_conflict_clause_for_theory_conflict(+LastVarName, +LastVarValue, +SolverEnv, -ConflictClause). | |
1234 | % Translate current sat solution, which is a theory conflict, to the theory and compute | |
1235 | % the (minimum) unsat core. Return the negated unsat core as a conflict clause. | |
1236 | % Note that an SMT formula passed to the theory solver is always a conjunction and | |
1237 | % thus the negated unsat core is a disjunction (clause). | |
1238 | % Assumption: unsat core computation only removes constraints and does not deduce new ones. | |
1239 | get_conflict_clause_for_theory_conflict(LastVarName, LastVarValue, SolverEnv, ConflictClause) :- | |
1240 | ( retract(idl_unsat_core(UnsatCore)) | |
1241 | -> true | |
1242 | ; get_from_solver_env(SolverEnv, sat_bindings, SatBindingsNoLast), | |
1243 | get_from_solver_env(SolverEnv, sat_vars, SatVars), | |
1244 | ? | temporary_set_unsat_core_timeout, |
1245 | sat_to_predicate_from_solution(SatBindingsNoLast, SatVars, SmtFormulaNoLast), | |
1246 | sat_to_predicate_from_solution([bind(LastVarName,LastVarValue)], SatVars, FixedConj), | |
1247 | debug_format_sat("Compute unsat core for : ", [], b(conjunct(FixedConj,SmtFormulaNoLast),pred,[])), | |
1248 | tools:start_ms_timer(TT), | |
1249 | conjunct_predicates([FixedConj,SmtFormulaNoLast],FullFormula), | |
1250 | ? | time_out(unsat_chr_core_list_with_auto_time_limit(FullFormula, 30000, |
1251 | [auto_time_out_factor(180), % we add 80 % | |
1252 | ignore_if_sol_found], _Result, CoreList), | |
1253 | 30000, TimeoutResult), | |
1254 | tools:stop_ms_timer_with_msg(TT,'unsat_chr_core_list_with_auto_time_limit'), | |
1255 | ( TimeoutResult == time_out | |
1256 | -> % don't waste too much time in unsat core computation | |
1257 | debug_format_sat("Canceled unsat core computation due to exceeding a timeout" ,[]), | |
1258 | TUnsatCore = FullFormula | |
1259 | ; (CoreList == [] | |
1260 | -> add_internal_error('Conflict clause in SMT solving is not a conflict.', | |
1261 | get_conflict_clause_for_theory_conflict(LastVarName)), | |
1262 | fail | |
1263 | ; conjunct_predicates(CoreList, TUnsatCore) | |
1264 | ) | |
1265 | ), | |
1266 | ? | remove_wd_pos_introduced_for_dpllt_keep_toplevel(TUnsatCore, UnsatCore), |
1267 | debug_format_sat("Computed unsat core: ", [], UnsatCore), | |
1268 | preferences:reset_temporary_preference(time_out) | |
1269 | ), !, | |
1270 | get_conflict_clause_from_unsat_core(UnsatCore, SolverEnv, ConflictClause), | |
1271 | !. | |
1272 | ||
1273 | get_conflict_clause_from_unsat_core_map(SolverEnv, UnsatCore, ConflictClause) :- | |
1274 | get_conflict_clause_from_unsat_core(UnsatCore, SolverEnv, ConflictClause). | |
1275 | ||
1276 | %% get_conflict_clause_from_unsat_core(+UnsatCore, +SolverEnv, -ConflictClause). | |
1277 | get_conflict_clause_from_unsat_core(UnsatCore, SolverEnv, ConflictClause) :- | |
1278 | get_from_solver_env(SolverEnv, sat_vars, SatVars), | |
1279 | get_from_solver_env(SolverEnv, t2b_env, T2BEnv), | |
1280 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
1281 | ? | predicate_to_sat(only_reuse, [], SatVars, T2BEnv, UnsatCore, _NewEnv, _, UnsatCoreSat, _NewSatVars), |
1282 | %nl, write('Core: '), | |
1283 | %translate:print_bexpr(UnsatCore),nl, | |
1284 | %translate:print_bexpr(UnsatCoreSat),nl, | |
1285 | sat_conj_negate_to_clause(UnsatCoreSat, TConflictClause), | |
1286 | ? | set_variable_references_in_clause(PlVars, TConflictClause, ConflictClause), |
1287 | !. | |
1288 | get_conflict_clause_from_unsat_core(_, _, _) :- | |
1289 | add_internal_error('Unsat core to conflict clause failed.', get_conflict_clause_from_unsat_core), | |
1290 | fail. | |
1291 | ||
1292 | %% get_complete_theory_lemma(+SolverEnv, -TheoryLemmaClause) :- | |
1293 | % Return the complete unsatisfiable SMT formula as a conflict clause. | |
1294 | get_complete_theory_lemma(SolverEnv, TheoryLemmaClause) :- | |
1295 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
1296 | get_from_solver_env(SolverEnv, sat_bindings, SatBindings), | |
1297 | get_clause_from_negated_ground_bindings(SatBindings, TTheoryLemmaClause), | |
1298 | ? | set_variable_references_in_clause(PlVars, TTheoryLemmaClause, TheoryLemmaClause), !. |
1299 | ||
1300 | %% get_clause_from_negated_ground_bindings(+SatBindings, -TheoryLemmaClause) :- | |
1301 | get_clause_from_negated_ground_bindings(SatBindings, TheoryLemmaClause) :- | |
1302 | get_clause_from_negated_ground_bindings(SatBindings, [], TheoryLemmaClause). | |
1303 | ||
1304 | get_clause_from_negated_ground_bindings([], Acc, Acc). | |
1305 | get_clause_from_negated_ground_bindings([bind(SatVarName,Pol)|T], Acc, TheoryLemmaClause) :- | |
1306 | ground(Pol), | |
1307 | !, | |
1308 | negate_polarity(Pol, NegPol), | |
1309 | get_clause_from_negated_ground_bindings(T, [NegPol-_-SatVarName|Acc], TheoryLemmaClause). | |
1310 | get_clause_from_negated_ground_bindings([_|T], Acc, TheoryLemmaClause) :- | |
1311 | get_clause_from_negated_ground_bindings(T, Acc, TheoryLemmaClause). | |
1312 | ||
1313 | temporary_set_unsat_core_timeout :- | |
1314 | preferences:temporary_set_preference(time_out, 25). | |
1315 | temporary_set_unsat_core_timeout :- | |
1316 | preferences:reset_temporary_preference(time_out), | |
1317 | fail. | |
1318 | ||
1319 | % In the conflict graph each node corresponds to a variable assignment. | |
1320 | % The predecessors of node x are the antecedent assignments A^w(x) corresponding | |
1321 | % to the unit clause w (in its original form) that led to the propagation of x (logical implications). | |
1322 | % The directed edges from the nodes in A^w(x) to node x are all labeled with w. | |
1323 | % Nodes that have no predecessor correspond to decision/branching assignments | |
1324 | % (cf. GRASP: A Search Algorithm for Propositional Satisfiability, by Marques-Silva and Sakallah). | |
1325 | % As an improvement, we apply first UIP clause learning (cf. Efficient Conflict Driven Learning in a Boolean Satisfiability Solver, Zhang et al.). | |
1326 | %% get_backjump_clause_conflict_resolution(+SolverEnv, +StateMutable, +ConflictLevel, +ConflictClause, -BjClause, -BjLevel, -UsedVars). | |
1327 | % Compute the conflict graph for a conflicting unit-propagation of a variable | |
1328 | % and extract a backjump clause. | |
1329 | % -UsedVars are the SAT variables used during conflict analysis (can be necessary for branching heuristic). | |
1330 | % Notes: | |
1331 | % - the variable references in the returned clause are not yet set (cf. get_clauses_to_learn_bump_scores/4) | |
1332 | % - we do not create an actual graph | |
1333 | get_backjump_clause_conflict_resolution(SolverEnv, StateMutable, ConflictLevel, ConflictClause, BjClause, BjLevel, UsedVars) :- | |
1334 | get_last_decision_level(StateMutable, _), | |
1335 | get_full_state(StateMutable, sat_stack, SatStack), | |
1336 | get_antecedent_assignments_for_clause(ConflictClause, SatStack, Antecedent), | |
1337 | new_mutdict(ResolvedSoFar), | |
1338 | ( Antecedent == [] | |
1339 | -> % special case if there are no antecedents of the conflict clause: occurs if | |
1340 | % antecedent assignments are all deterministic unit propagations (unit clauses in original formula) | |
1341 | % or all decision variables | |
1342 | negate_assignments_to_polarities(ConflictClause, BjClause), | |
1343 | get_variables_used_in_cdcl(ResolvedSoFar, BjClause, UsedVars), | |
1344 | % highest level other than conflict level or 0 | |
1345 | get_maximum_decision_level_other_than_current(BjClause, SatStack, 0, ConflictLevel, BjLevel) | |
1346 | ? | ; get_wo_antecedent_from_conflict_clause(SolverEnv, StateMutable, ConflictClause, DecisionVars), |
1347 | add_used_vars_to_mutdict(DecisionVars, ResolvedSoFar), | |
1348 | ? | get_backjump_clause_and_level(SolverEnv, StateMutable, ConflictLevel, ResolvedSoFar, Antecedent, BjClause, BjLevel, UsedVars) |
1349 | ). | |
1350 | ||
1351 | %% get_wo_antecedent_from_conflict_clause(+SolverEnv, +StateMutable, +Clause, -VarsNoAnt). | |
1352 | % Get variables without antecedent assignments from conflict clause. | |
1353 | get_wo_antecedent_from_conflict_clause(_, _, [], []). | |
1354 | get_wo_antecedent_from_conflict_clause(SolverEnv, StateMutable, [Pol-Var-N|T], VarsNoAnt) :- | |
1355 | get_from_sat_stack_or_explain_theory_propagation(SolverEnv, StateMutable, N, PropType, _, _, _), | |
1356 | PropType == branch, | |
1357 | !, | |
1358 | ? | get_wo_antecedent_from_conflict_clause(SolverEnv, StateMutable, T, NT), |
1359 | VarsNoAnt = [Pol-Var-N|NT]. | |
1360 | get_wo_antecedent_from_conflict_clause(SolverEnv, StateMutable, [Pol-Var-N|T], VarsNoAnt) :- | |
1361 | get_from_sat_stack_or_explain_theory_propagation(SolverEnv, StateMutable, N, _, _, _, OriginalClause), | |
1362 | get_full_state(StateMutable, sat_stack, SatStack), | |
1363 | get_antecedent_assignments_for_clause(OriginalClause, SatStack, Antecedent), | |
1364 | Antecedent == [], | |
1365 | !, | |
1366 | ? | get_wo_antecedent_from_conflict_clause(SolverEnv, StateMutable, T, NT), |
1367 | VarsNoAnt = [Pol-Var-N|NT]. | |
1368 | get_wo_antecedent_from_conflict_clause(SolverEnv, StateMutable, [_|T], NT) :- | |
1369 | ? | get_wo_antecedent_from_conflict_clause(SolverEnv, StateMutable, T, NT). |
1370 | ||
1371 | negate_assignments_to_polarities([], Out) :- | |
1372 | !, | |
1373 | Out = []. | |
1374 | negate_assignments_to_polarities([_-AssignedPol-SatVarName|T], [Pol-_-SatVarName|NT]) :- | |
1375 | ground(AssignedPol), | |
1376 | !, | |
1377 | negate_polarity(AssignedPol, Pol), | |
1378 | negate_assignments_to_polarities(T, NT). | |
1379 | /*negate_assignments_to_polarities([Pol-AssignedPol-SatVarName|T], [NPol-_-SatVarName|NT]) :- | |
1380 | var(AssignedPol), | |
1381 | !, | |
1382 | negate_polarity(Pol, NPol), | |
1383 | negate_assignments_to_polarities(T, NT).*/ | |
1384 | negate_assignments_to_polarities(In, _) :- | |
1385 | add_internal_error('Expected ground polarity.', negate_assignments_to_polarities(In)), | |
1386 | fail. | |
1387 | ||
1388 | % Fail if no decision has been made so far, i.e., the decision level is set to -1. | |
1389 | get_last_decision_level(StateMutable, Level) :- | |
1390 | get_full_state(StateMutable, decision_level, TLevel), | |
1391 | TLevel \== -1, | |
1392 | !, | |
1393 | Level = TLevel. | |
1394 | ||
1395 | negate_polarities([], []). | |
1396 | negate_polarities([Pol-Var-Name|T], [NPol-Var-Name|NT]) :- | |
1397 | negate_polarity(Pol, NPol), | |
1398 | negate_polarities(T, NT). | |
1399 | ||
1400 | get_maximum_decision_level_other_than_current([_], _, _, _, BjLevel) :- | |
1401 | % zero if learning a unit clause | |
1402 | !, | |
1403 | BjLevel = 0. | |
1404 | get_maximum_decision_level_other_than_current(BjClause, SatStack, BjLevelAcc, CurLevel, BjLevel) :- | |
1405 | get_maximum_decision_level_other_than_current_not_unit(BjClause, SatStack, BjLevelAcc, CurLevel, BjLevel). | |
1406 | ||
1407 | get_maximum_decision_level_other_than_current_not_unit([], _, BjLevelAcc, _, BjLevelAcc). | |
1408 | get_maximum_decision_level_other_than_current_not_unit([_-_-Name|T], SatStack, BjLevelAcc, CurLevel, BjLevel) :- | |
1409 | avl_fetch(Name, SatStack, (_,Level,_,_)), | |
1410 | ( (Level \== CurLevel, | |
1411 | Level > BjLevelAcc | |
1412 | ) | |
1413 | -> NBjLevelAcc = Level | |
1414 | ; NBjLevelAcc = BjLevelAcc | |
1415 | ), | |
1416 | get_maximum_decision_level_other_than_current_not_unit(T, SatStack, NBjLevelAcc, CurLevel, BjLevel). | |
1417 | ||
1418 | %% get_antecedent_assignments_for_clause(+ConflictClause, +SatStack, -Antecedent). | |
1419 | % It is important that the resulting list does not contain any duplicates | |
1420 | % to identify the first UIP. | |
1421 | get_antecedent_assignments_for_clause(ConflictClause, SatStack, Antecedent) :- | |
1422 | get_antecedent_assignments_for_clause(ConflictClause, SatStack, [], TAntecedent), | |
1423 | sort(TAntecedent, Antecedent), | |
1424 | !. | |
1425 | ||
1426 | get_antecedent_assignments_for_clause([], _, Acc, Acc). | |
1427 | get_antecedent_assignments_for_clause([_-_-SatVarName|T], SatStack, Acc, Antecedent) :- | |
1428 | get_antecedent_assignments(SatStack, SatVarName, TAntecedent), | |
1429 | append(Acc, TAntecedent, NAcc), | |
1430 | get_antecedent_assignments_for_clause(T, SatStack, NAcc, Antecedent). | |
1431 | ||
1432 | %% get_antecedent_assignments(+SatStack, +SatVarName, -Antecedent). | |
1433 | get_antecedent_assignments(SatStack, SatVarName, Antecedent) :- | |
1434 | avl_fetch(SatVarName, SatStack, (_,_,_,OriginalClause)), | |
1435 | !, | |
1436 | ? | select(_-_-SatVarName, OriginalClause, TAntecedent), |
1437 | ? | negate_polarities(TAntecedent, Antecedent), !. |
1438 | get_antecedent_assignments(_, _, []). % wd po not necessarily assigned, e.g., if the predicate containing the wd condition is false | |
1439 | ||
1440 | %% join_assignments(+A1, +A2, -Joined). | |
1441 | join_assignments([], A, _, A). | |
1442 | join_assignments([Pol-Var-Name|T], A2, ResolvedSoFar, A) :- | |
1443 | ? | ( ( \+ member(Pol-Var-Name, A2), |
1444 | \+ mutdict_get(ResolvedSoFar, Name, _) | |
1445 | ) | |
1446 | -> join_assignments(T, [Pol-Var-Name|A2], ResolvedSoFar, A) | |
1447 | ; join_assignments(T, A2, ResolvedSoFar, A) | |
1448 | ). | |
1449 | ||
1450 | %% resolve(+SatStack, +TBjClause, +ResolvedSoFar, +Resolver, -New). | |
1451 | % +Resolver is a SAT variable name to resolve next (i.e., expand its antecedent assignments). | |
1452 | resolve(SatStack, TBjClause, ResolvedSoFar, Resolver, New) :- | |
1453 | get_antecedent_assignments(SatStack, Resolver, Antecedent), | |
1454 | join_assignments(Antecedent, TBjClause, ResolvedSoFar, TNTBjClause), | |
1455 | ? | select(_-_-Resolver, TNTBjClause, NTBjClause), |
1456 | sort(NTBjClause, New). | |
1457 | ||
1458 | add_used_vars_to_mutdict([], _). | |
1459 | add_used_vars_to_mutdict([_-_-SatVarName|T], VarNamesDict) :- | |
1460 | \+ mutdict_get(VarNamesDict, SatVarName, _), | |
1461 | !, | |
1462 | mutdict_put(VarNamesDict, SatVarName, SatVarName), | |
1463 | add_used_vars_to_mutdict(T, VarNamesDict). | |
1464 | add_used_vars_to_mutdict([_|T], VarNamesDict) :- | |
1465 | add_used_vars_to_mutdict(T, VarNamesDict). | |
1466 | ||
1467 | get_variables_used_in_cdcl(ResolvedSoFar, BjClause, UsedVars) :- | |
1468 | add_used_vars_to_mutdict(BjClause, ResolvedSoFar), | |
1469 | mutdict_keys(ResolvedSoFar, UsedVars). | |
1470 | ||
1471 | %% get_backjump_clause_and_level(+SolverEnv, +StateMutable, +ConflictDLevel, +ResolvedSoFar, +TBjClause, -BjClause, -BjLevel, -UsedVars). | |
1472 | get_backjump_clause_and_level(SolverEnv, StateMutable, ConflictDLevel, ResolvedSoFar, TBjClause, BjClause, BjLevel, UsedVars) :- | |
1473 | ? | get_backjump_clause_and_level_sub(SolverEnv, StateMutable, ConflictDLevel, 0, _, TBjClause, Resolver, ThisLevelCount), |
1474 | get_full_state(StateMutable, sat_stack, SatStack), | |
1475 | ( ThisLevelCount == 1 | |
1476 | -> % break, first UIP | |
1477 | negate_polarities(TBjClause, BjClause), | |
1478 | get_maximum_decision_level_other_than_current(BjClause, SatStack, -1, ConflictDLevel, BjLevel), | |
1479 | get_variables_used_in_cdcl(ResolvedSoFar, BjClause, UsedVars) | |
1480 | ; ( var(Resolver) | |
1481 | -> % nothing to resolve and decision on conflict level not part of temporary backjump clause, | |
1482 | % all sources are backjump clause | |
1483 | negate_polarities(TBjClause, BjClause), | |
1484 | get_maximum_decision_level_other_than_current(BjClause, SatStack, -1, ConflictDLevel, BjLevel), | |
1485 | get_variables_used_in_cdcl(ResolvedSoFar, BjClause, UsedVars) | |
1486 | ? | ; resolve(SatStack, TBjClause, ResolvedSoFar, Resolver, NToExpand), |
1487 | mutdict_put(ResolvedSoFar, Resolver, Resolver), | |
1488 | ? | get_backjump_clause_and_level(SolverEnv, StateMutable, ConflictDLevel, ResolvedSoFar, NToExpand, BjClause, BjLevel, UsedVars) |
1489 | ) | |
1490 | ). | |
1491 | ||
1492 | get_backjump_clause_and_level_sub(_, _, _, ThisLevelCountAcc, ResolverAcc, [], ResolverAcc, ThisLevelCountAcc). | |
1493 | get_backjump_clause_and_level_sub(SolverEnv, StateMutable, ConflictDLevel, ThisLevelCountAcc, ResolverAcc, [_-_-SatVarName|T], Resolver, ThisLevelCount) :- | |
1494 | get_from_sat_stack_or_explain_theory_propagation(SolverEnv, StateMutable, SatVarName, PropType, Level, _, OriginalClause), | |
1495 | ( Level == ConflictDLevel | |
1496 | -> NThisLevelCountAcc is ThisLevelCountAcc + 1 | |
1497 | ; NThisLevelCountAcc = ThisLevelCountAcc | |
1498 | ), | |
1499 | ( (Level == ConflictDLevel, | |
1500 | PropType == unit, | |
1501 | OriginalClause \= [_] % not a deterministic unit propagation | |
1502 | ) | |
1503 | -> NResolverAcc = SatVarName | |
1504 | ; NResolverAcc = ResolverAcc | |
1505 | ), | |
1506 | ? | get_backjump_clause_and_level_sub(SolverEnv, StateMutable, ConflictDLevel, NThisLevelCountAcc, NResolverAcc, T, Resolver, ThisLevelCount). |
1507 | ||
1508 | %% get_from_sat_stack_or_explain_theory_propagation(+SolverEnv, +StateMutable, +SatVarName, -PropType, -Level, -Pol, -OriginalClause). | |
1509 | get_from_sat_stack_or_explain_theory_propagation(SolverEnv, StateMutable, SatVarName, PropType, Level, Pol, OriginalClause) :- | |
1510 | get_full_state(StateMutable, sat_stack, SatStack), | |
1511 | avl_fetch(SatVarName, SatStack, (PropType,Level,Pol,TOriginalClause)), | |
1512 | ( (PropType == theory, var(TOriginalClause)) | |
1513 | -> explain_theory_propagation(SolverEnv, SatStack, SatVarName, Level, Pol, OriginalClause), | |
1514 | avl_change(SatVarName, SatStack, _, NStack, (PropType,Level,Pol,OriginalClause)), | |
1515 | update_full_state(StateMutable, sat_stack, NStack) | |
1516 | ; OriginalClause = TOriginalClause | |
1517 | ). | |
1518 | ||
1519 | negate_polarity(pred_true, pred_false). | |
1520 | negate_polarity(pred_false, pred_true). | |
1521 | ||
1522 | asserta_once(Assertion) :- | |
1523 | call(dpllt_sat_solver:Assertion), | |
1524 | !. | |
1525 | asserta_once(Assertion) :- | |
1526 | asserta(dpllt_sat_solver:Assertion). | |
1527 | ||
1528 | b_pred_or_bool_true(X) :- X == truth; X == boolean_true; X == value(pred_true). | |
1529 | b_pred_or_bool_false(X) :- X == falsity; X == boolean_false; X == value(pred_false). | |
1530 | ||
1531 | sat_conj_negate_to_clause(Pred, Clause) :- | |
1532 | conjunction_to_list(Pred, List), | |
1533 | maplist(sat_equality_negate_to_literal, List, Clause). | |
1534 | ||
1535 | sat_equality_negate_to_literal(b(equal(ID,Pol),pred,_), NegPol-_-Name) :- | |
1536 | ID = b(identifier(Name),_,_), | |
1537 | Pol = b(Value,boolean,_), | |
1538 | ? | ( b_pred_or_bool_true(Value) |
1539 | -> NegPol = pred_false | |
1540 | ; NegPol = pred_true | |
1541 | ). | |
1542 | ||
1543 | %%%%% Solver State | |
1544 | create_solver_state(StateMutable) :- | |
1545 | empty_avl(EmptyAvl), | |
1546 | State = [sat_stack:EmptyAvl,cur_level:0,':'(decision_level,-1),current_stack_size:0,heuristic_avl:EmptyAvl], | |
1547 | create_mutable(solver_state(State), StateMutable). | |
1548 | ||
1549 | %% get_full_state(+StateMutable, +Key, -Datum). | |
1550 | get_full_state(StateMutable, Key, Datum) :- | |
1551 | get_mutable(solver_state(SolverState), StateMutable), | |
1552 | ? | member(Key:Datum, SolverState), !. |
1553 | ||
1554 | %% add_state_instance(+StateMutable, +Key, +Datum). | |
1555 | % Add an instance to iterable data. | |
1556 | add_state_instance(StateMutable, Key, Datum) :- | |
1557 | get_mutable(solver_state(SolverState), StateMutable), | |
1558 | ? | select(Key:Data, SolverState, Rest), |
1559 | ( Key == heuristic_avl | |
1560 | -> Datum = (SatVarName,Score), | |
1561 | avl_store(SatVarName, Data, Score, NewData) | |
1562 | ; Key == sat_stack, | |
1563 | Datum = (SatVarName,A,B,C,D), | |
1564 | avl_store(SatVarName, Data, (A,B,C,D), NewData) | |
1565 | ), !, | |
1566 | update_mutable(solver_state([Key:NewData|Rest]), StateMutable). | |
1567 | ||
1568 | %% delete_state_instance(+StateMutable, +Key, ?Datum). | |
1569 | delete_state_instance(StateMutable, Key, Datum) :- | |
1570 | get_mutable(solver_state(SolverState), StateMutable), | |
1571 | ? | select(Key:Data, SolverState, Rest), |
1572 | ( Key == heuristic_avl | |
1573 | -> Datum = (SatVarName,Score), | |
1574 | ( avl_delete(SatVarName, Data, Score, NewData) | |
1575 | ; NewData = Data | |
1576 | ) | |
1577 | ; Key == sat_stack, | |
1578 | Datum = (SatVarName,A,B,C,D), | |
1579 | ( avl_delete(SatVarName, Data, (A,B,C,D), NewData) | |
1580 | ; NewData = Data | |
1581 | ) | |
1582 | ), | |
1583 | !, | |
1584 | update_mutable(solver_state([Key:NewData|Rest]), StateMutable). | |
1585 | ||
1586 | %% update_full_state(+StateMutable, +Key, +Datum). | |
1587 | update_full_state(StateMutable, Key, Datum) :- | |
1588 | get_mutable(solver_state(SolverState), StateMutable), | |
1589 | ? | select(Key:_, SolverState, Rest), !, |
1590 | update_mutable(solver_state([Key:Datum|Rest]), StateMutable). | |
1591 | ||
1592 | %% Initialize the dynamic solver state for a specific solver. | |
1593 | init_dynamic_solver_state(SolverName) :- | |
1594 | clean_dynamic_solver_state, | |
1595 | asserta(solver_name(SolverName)), | |
1596 | asserta(restarts(0)), | |
1597 | asserta(amount_clause_reductions(0)), | |
1598 | asserta(amount_learned_clauses(0)), | |
1599 | asserta(conflict_stats(total(0), since_restart(0), since_reduction(0))), | |
1600 | asserta(recent_lbds_dl(Diff1-Diff1, 0)), | |
1601 | asserta(recent_stack_sizes_dl(Diff2-Diff2, 0)), | |
1602 | asserta(total_lbd_sum(0)), | |
1603 | init_luby_sequence. | |
1604 | ||
1605 | clean_dynamic_solver_state :- | |
1606 | retractall(solver_name(_)), | |
1607 | retractall(restarts(_)), | |
1608 | retractall(is_restart), | |
1609 | retractall(bt_from_smt_solution), | |
1610 | retractall(recent_lbds_dl(_, _)), | |
1611 | retractall(recent_stack_sizes_dl(_, _)), | |
1612 | retractall(saved_phase(_, _)), | |
1613 | retractall(amount_clause_reductions(_)), | |
1614 | retractall(amount_learned_clauses(_)), | |
1615 | retractall(luby_counter(_)), | |
1616 | retractall(exclude_sat_solution_clause(_)), | |
1617 | retractall(total_lbd_sum(_)), | |
1618 | retractall(conflict_stats(_, _, _)), | |
1619 | retractall(idl_unsat_core(_)), | |
1620 | retractall(backjump_wd_level(_)), | |
1621 | retractall(backjump_wd_clause(_,_,_)), | |
1622 | retractall(backjump_level(_)), | |
1623 | retractall(backjump_clause(_, _, _, _)), | |
1624 | ( incremental_mode | |
1625 | -> true | |
1626 | ; retractall(memoize_backjump_clause(_, _, _)) | |
1627 | ). | |
1628 | ||
1629 | %% Remove dynamically stored unsat core found by the IDL solver. | |
1630 | remove_idl_unsat_core :- | |
1631 | retractall(idl_unsat_core(_)). | |
1632 | ||
1633 | %% Store an unsat core found by the IDL solver in the SMT solvers dynamic state. | |
1634 | store_idl_unsat_core(Core) :- | |
1635 | retractall(idl_unsat_core(_)), | |
1636 | asserta(idl_unsat_core(Core)). | |
1637 | ||
1638 | %% Announce backtracking after a solution has been found in order to backtrack to search for another solution. | |
1639 | %% We have to be able to distinguish between backtracking due to not finding a solution or backtracking | |
1640 | %% triggered by the user to find another solution. | |
1641 | announce_bt_from_smt_solution :- | |
1642 | asserta(bt_from_smt_solution). | |
1643 | %%%%% | |
1644 | ||
1645 | %% b_to_cnf(+In, +State, -Out). | |
1646 | % Accepts predicates with conjunction and disjunction. | |
1647 | b_to_cnf(In, State, Out) :- | |
1648 | get_texpr_expr(In, Expr), | |
1649 | ? | b_to_cnf_aux(Expr, State, Out), |
1650 | !. | |
1651 | b_to_cnf(In, _, _) :- | |
1652 | translate_bexpression(In, PPIn), | |
1653 | !, | |
1654 | add_error_fail(b_to_cnf, 'CNF conversion failed', PPIn). | |
1655 | ||
1656 | b_to_cnf_aux(identifier(Name), State, [[pred_true-Res-Name]]) :- !, | |
1657 | ? | member(bind(Name,Res), State). |
1658 | b_to_cnf_aux(X, _, [Out]) :- | |
1659 | ? | ( b_pred_or_bool_true(X) |
1660 | -> Out = [pred_true-pred_true-nonvar] | |
1661 | ? | ; b_pred_or_bool_false(X) |
1662 | -> Out = [] | |
1663 | ; fail | |
1664 | ), !. | |
1665 | ||
1666 | b_to_cnf_aux(equal(A,B), State, CNF) :- | |
1667 | ground(B), | |
1668 | get_texpr_expr(B, Expr), | |
1669 | ? | ( b_pred_or_bool_true(Expr) |
1670 | -> b_to_cnf(A, State, CNF) | |
1671 | ; %b_pred_or_bool_false(Expr), | |
1672 | safe_create_texpr(value(pred_true), boolean, [], True), | |
1673 | safe_create_texpr(equal(A,True), pred, [], EqualTrue), | |
1674 | b_to_cnf_aux(negation(EqualTrue), State, CNF) | |
1675 | ). | |
1676 | b_to_cnf_aux(negation(A), State, [[Res]]) :- | |
1677 | b_to_cnf(A, State, [[Pol-Var-Name]]), | |
1678 | ( Pol == pred_true | |
1679 | -> Res = pred_false-Var-Name | |
1680 | ; Pol == pred_false, | |
1681 | Res = pred_true-Var-Name | |
1682 | ). | |
1683 | b_to_cnf_aux(disjunct(D1,D2), State, Res) :- | |
1684 | get_texpr_expr(D1, conjunct(A,B)), | |
1685 | !, | |
1686 | b_to_cnf(b(disjunct(A,D2),pred,[]), State, RDJ1), | |
1687 | b_to_cnf(b(disjunct(B,D2),pred,[]), State, RDJ2), | |
1688 | append(RDJ1, RDJ2, Res). | |
1689 | b_to_cnf_aux(disjunct(D1,D2), State, Res) :- | |
1690 | get_texpr_expr(D2, conjunct(A,B)), | |
1691 | !, | |
1692 | b_to_cnf(b(disjunct(D1,A),pred,[]), State, RDJ1), | |
1693 | b_to_cnf(b(disjunct(D1,B),pred,[]), State, RDJ2), | |
1694 | append(RDJ1, RDJ2, Res). | |
1695 | b_to_cnf_aux(disjunct(D1,D2),State,Res) :- | |
1696 | b_to_cnf(D1, State, TResD1), | |
1697 | b_to_cnf(D2, State, TResD2), | |
1698 | ( TResD1 = [ResD1], | |
1699 | TResD2 = [ResD2] | |
1700 | -> append(ResD1, ResD2, DRes), | |
1701 | Res = [DRes] | |
1702 | ; TResD1 = [ClauseResD1], | |
1703 | TResD2 \= [_] | |
1704 | -> maplist(append(ClauseResD1), TResD2, Res) | |
1705 | ; TResD2 = [ClauseResD2], | |
1706 | TResD1 \= [_] | |
1707 | -> maplist(append(ClauseResD2), TResD1, Res) | |
1708 | ; disjunct_non_singleton_cnfs(TResD1, TResD2, Res) | |
1709 | ). | |
1710 | b_to_cnf_aux(conjunct(A,B), State, Res) :- | |
1711 | b_to_cnf(A, State, RA), | |
1712 | b_to_cnf(B, State, RB), | |
1713 | append(RA, RB, Res). | |
1714 | ||
1715 | %% disjunct_non_singleton_cnfs(+Cnf1, +Cnf2, -Cnf). | |
1716 | disjunct_non_singleton_cnfs([], Cnf, Cnf). | |
1717 | disjunct_non_singleton_cnfs([Clause|T], Cnf2, Cnf) :- | |
1718 | maplist(append(Clause), Cnf2, NCnf2), | |
1719 | disjunct_non_singleton_cnfs(T, NCnf2, Cnf). | |
1720 | ||
1721 | :- dynamic luby_counter/1. | |
1722 | :- volatile luby_counter/1. | |
1723 | ||
1724 | % Used for random restarts. | |
1725 | % First restart is after 32nd conflict, second after additional 32 conflicts, | |
1726 | % third after additional 64 conflicts etc. | |
1727 | init_luby_sequence :- | |
1728 | retractall(luby_counter(_)), | |
1729 | % unit length of 32 | |
1730 | % 1,1,2,1,1,2,4,1,1,2,1,1,2,4,8,.. | |
1731 | assertz(luby_counter(1)), | |
1732 | assertz(luby_counter(1)), | |
1733 | assertz(luby_counter(2)), | |
1734 | assertz(luby_counter(1)), | |
1735 | assertz(luby_counter(1)), | |
1736 | assertz(luby_counter(2)), | |
1737 | assertz(luby_counter(4)), | |
1738 | assertz(luby_counter(1)), | |
1739 | assertz(luby_counter(1)), | |
1740 | assertz(luby_counter(2)), | |
1741 | assertz(luby_counter(1)), | |
1742 | assertz(luby_counter(1)), | |
1743 | assertz(luby_counter(2)), | |
1744 | assertz(luby_counter(4)), | |
1745 | assertz(luby_counter(8)), | |
1746 | assertz(luby_counter(1)), | |
1747 | assertz(luby_counter(1)), | |
1748 | assertz(luby_counter(2)), | |
1749 | assertz(luby_counter(1)), | |
1750 | assertz(luby_counter(1)), | |
1751 | assertz(luby_counter(2)), | |
1752 | assertz(luby_counter(4)), | |
1753 | assertz(luby_counter(8)), | |
1754 | assertz(luby_counter(16)), | |
1755 | assertz(luby_counter(1)), | |
1756 | assertz(luby_counter(1)), | |
1757 | assertz(luby_counter(2)), | |
1758 | assertz(luby_counter(1)), | |
1759 | assertz(luby_counter(1)), | |
1760 | assertz(luby_counter(2)), | |
1761 | assertz(luby_counter(4)), | |
1762 | assertz(luby_counter(8)), | |
1763 | assertz(luby_counter(16)), | |
1764 | assertz(luby_counter(32)), | |
1765 | assertz(luby_counter(1)), | |
1766 | assertz(luby_counter(1)), | |
1767 | assertz(luby_counter(2)), | |
1768 | assertz(luby_counter(1)), | |
1769 | assertz(luby_counter(1)), | |
1770 | assertz(luby_counter(2)), | |
1771 | assertz(luby_counter(4)), | |
1772 | assertz(luby_counter(8)), | |
1773 | assertz(luby_counter(16)), | |
1774 | assertz(luby_counter(32)), | |
1775 | assertz(luby_counter(64)), | |
1776 | assertz(luby_counter(1)), | |
1777 | assertz(luby_counter(1)), | |
1778 | assertz(luby_counter(2)), | |
1779 | assertz(luby_counter(1)), | |
1780 | assertz(luby_counter(1)), | |
1781 | assertz(luby_counter(2)), | |
1782 | assertz(luby_counter(4)), | |
1783 | assertz(luby_counter(8)), | |
1784 | assertz(luby_counter(16)), | |
1785 | assertz(luby_counter(32)), | |
1786 | assertz(luby_counter(64)), | |
1787 | assertz(luby_counter(128)). | |
1788 | ||
1789 | % ---------------- | |
1790 | ||
1791 | %% simplify_cnf(+CNF, -Simplified). | |
1792 | % Boolean resolution. | |
1793 | simplify_cnf([], []). | |
1794 | simplify_cnf([Clause|T], NewCnf) :- | |
1795 | simplify_clause(Clause, _, Simplified, IsTrue), !, | |
1796 | Simplified \== [], % contradiction if a clause is empty | |
1797 | ( IsTrue == true | |
1798 | -> NewCnf = NT % remove true clauses | |
1799 | ; NewCnf = [Simplified|NT] | |
1800 | ), | |
1801 | simplify_cnf(T, NT). | |
1802 | ||
1803 | simplify_clause([], IsTrue, [], IsTrue). | |
1804 | simplify_clause([Pol-Var-_|T], IsTrueAcc, NT, IsTrue) :- | |
1805 | ground(Var), | |
1806 | Pol \== Var, | |
1807 | !, | |
1808 | simplify_clause(T, IsTrueAcc, NT, IsTrue). | |
1809 | simplify_clause([Pol-Var-SatVarName|T], IsTrueAcc, [Pol-Var-SatVarName|NT], IsTrue) :- | |
1810 | ( Pol == Var | |
1811 | -> IsTrueAcc = true | |
1812 | ; true | |
1813 | ), | |
1814 | simplify_clause(T, IsTrueAcc, NT, IsTrue). | |
1815 | ||
1816 | clause_order(_-_-A3, _-_-B3) :- A3 @< B3. | |
1817 | ||
1818 | %% unit_propagate_cnf(+StateMutable, +Clauses, -NewClauses). | |
1819 | % A simple unit propagation, useful to run before reification. | |
1820 | % Removes duplicates from each clause. | |
1821 | % Important to identify all unit clauses, b_to_cnf does not check for unique sat variables in clauses. | |
1822 | unit_propagate_cnf(SolverEnv, StateMutable, Clauses, NewClauses) :- | |
1823 | ? | unit_prop_clause_sort(true, SolverEnv, StateMutable, Clauses, _, _, TNewClauses), |
1824 | simplify_cnf(TNewClauses, NewClauses). | |
1825 | ||
1826 | %% exhaustive_unit_propagate_cnf(+SolverEnv, +StateMutable, +Clauses, -NewClauses). | |
1827 | % Exhaustive unit propagation until no more unit clause is present. | |
1828 | % Simplifies CNF after unit propagation and checks for unit clauses again. | |
1829 | % Removes duplicates from each clause once. | |
1830 | exhaustive_unit_propagate_cnf(SolverEnv, StateMutable, Clauses, NewClauses) :- | |
1831 | unit_prop_clause_sort(true, SolverEnv, StateMutable, Clauses, _, Resolved, TNewClauses), | |
1832 | exhaustive_unit_propagate_cnf_loop(SolverEnv, StateMutable, Resolved, TNewClauses, NewClauses). | |
1833 | ||
1834 | exhaustive_unit_propagate_cnf_loop(_, _, false, CAcc, NewClauses) :- | |
1835 | !, | |
1836 | NewClauses = CAcc. | |
1837 | exhaustive_unit_propagate_cnf_loop(SolverEnv, StateMutable, true, Cnf, NewCnf) :- | |
1838 | simplify_cnf(Cnf, SimplifiedCnf), | |
1839 | unit_prop_clause_sort(false, SolverEnv, StateMutable, SimplifiedCnf, _, Resolved, TNewCnf), | |
1840 | exhaustive_unit_propagate_cnf_loop(SolverEnv, StateMutable, Resolved, TNewCnf, NewCnf). | |
1841 | ||
1842 | %% unit_prop_clause_sort(+Sort, +StateMutable, +CNF, +RAcc, -Resolved, -NewClauses). | |
1843 | % Removes duplicates from each clause if +Sort is true. | |
1844 | % Logs if a variable has been unit propagated in -Resolved using +RAcc. | |
1845 | unit_prop_clause_sort(_, _, _, [], RAcc, RAcc, []). | |
1846 | unit_prop_clause_sort(Sort, SolverEnv, StateMutable, [Clause|T], RAcc, Resolved, NewClauses) :- | |
1847 | ( Sort = true | |
1848 | -> sort(Clause, TNewClause), | |
1849 | samsort(clause_order, TNewClause, NewClause) | |
1850 | ; NewClause = Clause | |
1851 | ), | |
1852 | ( NewClause = [pred_false-pred_false-nonvar] | |
1853 | -> % false on the top level conjunction | |
1854 | fail | |
1855 | ; NewClause = [pred_true-pred_true-nonvar] | |
1856 | -> % true on the top level conjunction; remove clause | |
1857 | NewClauses = NT | |
1858 | ; NewClause = [Pol-PrologVar-SatVarName] | |
1859 | -> PrologVar = Pol, | |
1860 | RAcc = true, | |
1861 | debug_format_sat("deterministic unit propagation of ~w with polarity ~w before reification", [SatVarName,Pol]), | |
1862 | ? | bt_log_sat_stack(StateMutable, SatVarName, unit, 0, Pol, [Pol-PrologVar-SatVarName]), |
1863 | NewClauses = NT | |
1864 | ; NewClauses = [NewClause|NT] | |
1865 | ), | |
1866 | ? | unit_prop_clause_sort(Sort, SolverEnv, StateMutable, T, RAcc, Resolved, NT). |
1867 | ||
1868 | % ---------------- | |
1869 | ||
1870 | portray_sat_stack(StateMutable) :- | |
1871 | get_full_state(StateMutable, sat_stack, SatStack), | |
1872 | forall(avl_member(Key, SatStack, Val), format("~w,~w~n", [Key,Val])). | |
1873 | ||
1874 | portray_cnf(Clauses) :- length(Clauses,Len), format('CNF with ~w clauses:~n',[Len]), | |
1875 | maplist(portray_sat_clause,Clauses). | |
1876 | ||
1877 | portray_sat_clause(Clause) :- write(' '),maplist(portray_literal,Clause),nl. | |
1878 | ||
1879 | portray_literal(pred_false-PrologVar-ID) :- !, format('- ~w(~w) ',[ID,PrologVar]). | |
1880 | portray_literal(pred_true-PrologVar-ID) :- !, format(' ~w(~w) ',[ID,PrologVar]). | |
1881 | portray_literal(Lit) :- format(' *** UNKNOWN: ~w ',[Lit]). | |
1882 | ||
1883 | % ---------------- | |
1884 | ||
1885 | ||
1886 | ||
1887 | /* | |
1888 | %% static_sat_symmetry_breaking(+Clauses, +SolverEnv, +CurLevelMut, -NewSolverEnv). | |
1889 | % 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 | |
1890 | % Can only be used for pure SAT solving. | |
1891 | static_sat_symmetry_breaking(_, SolverEnv, _, NewSolverEnv) :- | |
1892 | static_sat_symmetry_breaking(false), | |
1893 | !, | |
1894 | NewSolverEnv = SolverEnv. | |
1895 | static_sat_symmetry_breaking(Clauses, SolverEnv, CurLevelMut, NewSolverEnv) :- | |
1896 | \+ symmetry_breaking_pred(_, _), | |
1897 | !, | |
1898 | get_symmetry_breaking_predicates(Clauses, SBPsConjNoRef, NewSatVars), | |
1899 | asserta(symmetry_breaking_pred(SBPsConjNoRef,NewSatVars)), | |
1900 | static_sat_symmetry_breaking(Clauses, SolverEnv, CurLevelMut, NewSolverEnv). | |
1901 | static_sat_symmetry_breaking(_, SolverEnv, CurLevelMut, NewSolverEnv) :- | |
1902 | get_asserted_symmetry_breaking_pred(SolverEnv, SBPsConj, NewSolverEnv), | |
1903 | problem_setup(NewSolverEnv, CurLevelMut, SBPsConj). | |
1904 | ||
1905 | get_asserted_symmetry_breaking_pred(SolverEnv, SBPsConj, NewSolverEnv) :- | |
1906 | symmetry_breaking_pred(SBPsConjNoRef, NewSatVars), | |
1907 | add_symmetry_breaking_eqs_to_solver_env(NewSatVars, SolverEnv, NewSolverEnv), | |
1908 | get_from_solver_env(NewSolverEnv, pl_vars, PlVars), | |
1909 | set_variable_references_in_clauses(PlVars, SBPsConjNoRef, SBPsConj), | |
1910 | findall(Var, (member(Var, NewSatVars), bt_asserta(heuristic_tuple(Var,1))), _). | |
1911 | ||
1912 | %% add_symmetry_breaking_eqs_to_solver_env(+NewSatVars, +SolverEnv, -NewSolverEnv). | |
1913 | % Symmetry breaking might introduce new SAT variables for equalities inbetween cycles of permutations. | |
1914 | % We update the solver environment and create the corresponding SMT formulas for equalities here. | |
1915 | % This is necessary, e.g., if a SAT variable corresponding to an equality introduced | |
1916 | % from symmetry breaking is involved in a conflict. | |
1917 | add_symmetry_breaking_eqs_to_solver_env(NewSatVars, SolverEnv, NewSolverEnv) :- | |
1918 | SolverEnv = [sat_vars:SatVars,sat_varnames:SatVarNames,sat_bindings:SatBindings,t2b_env:Env,pl_vars:PrologSatVarTriple], | |
1919 | add_symmetry_breaking_eqs_to_solver_env(NewSatVars, SatVars, SatVarNames, SatBindings, Env, PrologSatVarTriple, NSatVars, NSatVarNames, NSatBindings, NEnv, NPrologSatVarTriple), | |
1920 | NewSolverEnv = [sat_vars:NSatVars,sat_varnames:NSatVarNames,sat_bindings:NSatBindings,t2b_env:NEnv,pl_vars:NPrologSatVarTriple]. | |
1921 | ||
1922 | add_symmetry_breaking_eqs_to_solver_env([], SatVars, SatVarNames, SatBindings, Env, PrologSatVarTriple, SatVars, SatVarNames, SatBindings, Env, PrologSatVarTriple). | |
1923 | add_symmetry_breaking_eqs_to_solver_env([NewSatVarName-EqClauses|T], SatVars, SatVarNames, SatBindings, Env, PrologSatVarTriple, NSatVars, NSatVarNames, NSatBindings, NEnv, NPrologSatVarTriple) :- | |
1924 | maplist(clause_to_smt_disjunction(SatVars), EqClauses, EqSmtClauses), | |
1925 | conjunct_predicates(EqSmtClauses, EqSmt1), % all true | |
1926 | maplist(negate_smt_formula, EqSmtClauses, NegEqSmtClauses), | |
1927 | conjunct_predicates(NegEqSmtClauses, EqSmt2), % or all false | |
1928 | EqSmt = b(disjunct(EqSmt1,EqSmt2),pred,[]), | |
1929 | SatVars1 = [b(identifier(NewSatVarName),boolean,[smt_formula(EqSmt),eq_symmetry_break])|SatVars], | |
1930 | SatVarNames1 = [NewSatVarName|SatVarNames], | |
1931 | SatBindings1 = [bind(NewSatVarName,Var)|SatBindings], | |
1932 | PrologSatVarTriple1 = [Var-NewSatVarName-EqSmt|PrologSatVarTriple], | |
1933 | Env1 = [(EqSmt,b(identifier(NewSatVarName),boolean,[]))|Env], | |
1934 | add_symmetry_breaking_eqs_to_solver_env(T, SatVars1, SatVarNames1, SatBindings1, Env1, PrologSatVarTriple1, NSatVars, NSatVarNames, NSatBindings, NEnv, NPrologSatVarTriple). | |
1935 | ||
1936 | %clause_to_smt_disjunction(_, [], b(truth,pred,[])). | |
1937 | clause_to_smt_disjunction(SatVars, [Pol-_-SatVarName|T], SmtDisj) :- | |
1938 | get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula), | |
1939 | clause_to_smt_disjunction(SatVars, T, SmtFormula, SmtDisj). | |
1940 | ||
1941 | clause_to_smt_disjunction(_, [], Acc, Acc). | |
1942 | clause_to_smt_disjunction(SatVars, [Pol-_-SatVarName|T], Acc, SmtDisj) :- | |
1943 | get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula), | |
1944 | NAcc = b(disjunct(SmtFormula,Acc),pred,[]), | |
1945 | clause_to_smt_disjunction(SatVars, T, NAcc, SmtDisj). | |
1946 | */ |