Questions from last week:
paper-1 : "On Computing Minimum Unsatisfiable Cores", Inês Lynce and João Marques-Silva.
Q : Clause recording
On page 4 in Example 3 a new clause is recorded after a solution is found for the current assignment. But even though
For example:
${s_1=0, s_2=0, s_3=1, s_4=1, s_5=0, s_6=1, x_1=1, x_2=0, x_3=0 } \to \omega_8' = s_2 \lor s_5$ -
${s_1=0, s_2=0, s_3=1, s_4=1, s_5=0, s_6=1, x_1=0, x_2=0, x_3=0 } \to \omega_8' = s_1 \lor s_2 \lor s_5$ ? - ...
Questions about paper-2: "Unsatisfiable Core Shrinking for Anytime Answer Set Optimization", Alviano, Dodaro
Q : Symmetry Breakers
How do the Symmetry Breakers that are added to a Program
Q : ONE Algorithm
Related to the Question above, in Example 3 after the first iteration step the set