MUSes and MCSes

George Katsirelos, Fahiem Bacchus

► To cite this version:

George Katsirelos, Fahiem Bacchus. MUSes and MCSes. AAAI 2016 Workshop on Beyond NP, Feb 2016, Phoenix, United States. hal-01606478

HAL Id: hal-01606478

https://hal.science/hal-01606478

Submitted on 5 Jun 2020

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# MUSes and MCSes

George Katsirelos

February 13, 2016

<figure><img src="image_2.png" /></figure>

<figure><img src="image_3.png" /></figure>

<figure><img src="image_4.png" /></figure>

<figure><img src="image_5.png" /></figure>

<figure><img src="image_6.png" /></figure>

<figure><img src="image_7.png" /></figure>

<figure><img src="image_8.png" /></figure>

<figure><img src="image_9.png" /></figure>

<figure><img src="image_10.png" /></figure>

<figure><img src="image_11.png" /></figure>

<figure><img src="image_12.png" /></figure>

<figure><img src="image_13.png" /></figure>

<figure><img src="image_14.png" /></figure>

<figure><img src="image_15.png" /></figure>
* Boolean satisfiability in Conjunctive Normal Form (CNF)

* True/False variables x, y, z, ...

* Literals x, x̄, ...

* Clauses: disjunctions (sets) of literals x ∨ y ∨ z

* Formulas: conjunctions (sets) of clauses

<figure><img src="image_16.png" /></figure>
Minimal Correction Sets

• $F \setminus C$ is satisfiable, no larger subset of $F$ is

<figure><img src="image_17.png" /></figure>

<figure><img src="image_18.png" /></figure>

<figure><img src="image_19.png" /></figure>

<figure><img src="image_20.png" /></figure>

<figure><img src="image_21.png" /></figure>

<figure><img src="image_22.png" /></figure>

<figure><img src="image_23.png" /></figure>

<figure><img src="image_24.png" /></figure>

<figure><img src="image_25.png" /></figure>

<figure><img src="image_26.png" /></figure>

<figure><img src="image_27.png" /></figure>

<figure><img src="image_28.png" /></figure>

<figure><img src="image_29.png" /></figure>

<figure><img src="image_30.png" /></figure>

<figure><img src="image_31.png" /></figure>

<figure><img src="image_32.png" /></figure>

<figure><img src="image_33.png" /></figure>

<figure><img src="image_34.png" /></figure>
Minimal Correction Sets

• $F \setminus C$ is satisfiable, no larger subset of $F$ is

$$ \begin{array}{ccc} (x_1) & (x_2) & (x_3) \\ (\bar{x}_1 \lor \bar{x}_2) & (\bar{x}_1 \lor \bar{x}_3) & (\bar{x}_2 \lor \bar{x}_3) \end{array} $$

<figure><img src="image_35.png" /></figure>
Minimal Unsatisfiable Sets

* $U \subseteq F$ is unsatisfiable, no smaller subset of $F$ is
  Also called minimal cores

<figure><img src="image_36.png" /></figure>

<figure><img src="image_37.png" /></figure>

<figure><img src="image_38.png" /></figure>

<figure><img src="image_39.png" /></figure>

<figure><img src="image_40.png" /></figure>

<figure><img src="image_41.png" /></figure>

<figure><img src="image_42.png" /></figure>

<figure><img src="image_43.png" /></figure>

<figure><img src="image_44.png" /></figure>

<figure><img src="image_45.png" /></figure>

<figure><img src="image_46.png" /></figure>

<figure><img src="image_47.png" /></figure>

<figure><img src="image_48.png" /></figure>

<figure><img src="image_49.png" /></figure>
Minimal Unsatisfiable Sets

* $U \subseteq F$ is unsatisfiable, no smaller subset of $F$ is Also called minimal cores

$$ \begin{array}{ccc} (x_1) & (x_2) & (x_3) \\ (\bar{x}_1 \lor \bar{x}_2) & (\bar{x}_1 \lor \bar{x}_3) & (\bar{x}_2 \lor \bar{x}_3) \end{array} $$

<figure><img src="image_50.png" /></figure>
MUS applications

* Analysis of over-constrained systems [Junker, 2004]

* Diagnosis [Han and Lee, 1999]

* Type error Debugging [Stuckey et al, 2003]

* Function Decomposition [Belov et al, 2012]

* Approximate model counting [Ivrli et al, 2016]

* MaxSAT [Morgado et al, 2013; Davies and Bacchus, 2011]

<figure><img src="image_51.png" /></figure>
# MUS applications – over-constrained systems

* Help user find the bug in their model

<figure><img src="image_52.png" /></figure>
# MUS applications – over-constrained systems

* Help user find the bug in their model

* Also for indirectly generated models

* Compiler-generated model for type-checking

<figure><img src="image_53.png" /></figure>
# MUS applications – Approximate model counting

* Add a system of large XOR constraints and do complete model counting

* But SAT solvers generally poor at handling large XOR constraints

<figure><img src="image_54.png" /></figure>

<figure><img src="image_55.png" /></figure>

<figure><img src="image_56.png" /></figure>

<figure><img src="image_57.png" /></figure>

<figure><img src="image_58.png" /></figure>

<figure><img src="image_59.png" /></figure>

<figure><img src="image_60.png" /></figure>

<figure><img src="image_61.png" /></figure>

<figure><img src="image_62.png" /></figure>

<figure><img src="image_63.png" /></figure>

<figure><img src="image_64.png" /></figure>

<figure><img src="image_65.png" /></figure>

<figure><img src="image_66.png" /></figure>

<figure><img src="image_67.png" /></figure>

<figure><img src="image_68.png" /></figure>

<figure><img src="image_69.png" /></figure>
# MUS applications – Approximate model counting

* Add a system of large XOR constraints and do complete model counting

* But SAT solvers generally poor at handling large XOR constraints

* Find “input” variables, restrict XORs to these

<figure><img src="image_70.png" /></figure>
MUS applications – Approximate model counting

* Add a system of large XOR constraints and do complete model counting

* But SAT solvers generally poor at handling large XOR constraints

* Find “input” variables, restrict XORs to these

* MUSes of

$$F(\mathbf{X}) \wedge F(\mathbf{Y}) \wedge \mathbf{\wedge}(x_i = y_i) \wedge \mathbf{\vee}(x_i \neq y_i)$$

<figure><img src="image_71.png" /></figure>
MCS applications

* MaxSAT [Mencía et al, 2015; Bjorner and Narodytska, 2015]

* Finding MUSes! [Bacchus and K, 2015]

<figure><img src="image_72.png" /></figure>
Hitting set duality

$$ (x_1) \qquad (x_2) \qquad (x_3) \\ (\bar{x}_1 \lor \bar{x}_2) \qquad (\bar{x}_1 \lor \bar{x}_3) \qquad (\bar{x}_2 \lor \bar{x}_3) $$

$$ (x_1) \qquad (x_2) \qquad (x_3) \\ (\bar{x}_1 \lor \bar{x}_2) \qquad (\bar{x}_1 \lor \bar{x}_3) \qquad (\bar{x}_2 \lor \bar{x}_3) $$

$$ (x_1) \qquad (x_2) \qquad (x_3) \\ (\bar{x}_1 \lor \bar{x}_2) \qquad (\bar{x}_1 \lor \bar{x}_3) \qquad (\bar{x}_2 \lor \bar{x}_3) $$

<figure><img src="image_73.png" /></figure>
Hitting set duality

* Every (minimal) CS is a hitting set of all (minimal) USes

* Every (minimal) US is a hitting set of all (minimal) CSes

[Reiter, 1987]

<figure><img src="image_74.png" /></figure>
Interesting Queries

* Discover a single MCS/MCS

• $D^P$-complete [Liberatore, 2005]

* Enumerate all MCSes/MUSes

• Hypergraph transversal

* Find minimum MCS/MUS

• MUS: $\Sigma_2^P$-complete [Gupta, 2006]

• MCS: $D^P$-complete (MaxSAT)

<figure><img src="image_75.png" /></figure>
Discovering MUSes

<figure><img src="image_76.png" /></figure>

<figure><img src="image_77.png" /></figure>

<figure><img src="image_78.png" /></figure>

<figure><img src="image_79.png" /></figure>

<figure><img src="image_80.png" /></figure>

<figure><img src="image_81.png" /></figure>

<figure><img src="image_82.png" /></figure>

<figure><img src="image_83.png" /></figure>

<figure><img src="image_84.png" /></figure>

<figure><img src="image_85.png" /></figure>

<figure><img src="image_86.png" /></figure>

<figure><img src="image_87.png" /></figure>

<figure><img src="image_88.png" /></figure>

<figure><img src="image_89.png" /></figure>
* Algorithm

* Incremental solver technology

* Avoiding calling the SAT solver

* Trimming [Belov et al, 2014]

* Model Rotation [Belov and Marques-Silva, 2011]

* Clause set refinement [Nadel et al, 2014]

<figure><img src="image_90.png" /></figure>

<figure><img src="image_91.png" /></figure>

<figure><img src="image_92.png" /></figure>

<figure><img src="image_93.png" /></figure>

<figure><img src="image_94.png" /></figure>

<figure><img src="image_95.png" /></figure>

<figure><img src="image_96.png" /></figure>

<figure><img src="image_97.png" /></figure>

<figure><img src="image_98.png" /></figure>

<figure><img src="image_99.png" /></figure>

<figure><img src="image_100.png" /></figure>

<figure><img src="image_101.png" /></figure>

<figure><img src="image_102.png" /></figure>

<figure><img src="image_103.png" /></figure>

<figure><img src="image_104.png" /></figure>

<figure><img src="image_105.png" /></figure>
Impact of incremental solver
technology

<figure><img src="image_106.png" /></figure>

<figure><img src="image_107.png" /></figure>
Impact of fewer SAT calls

<figure><img src="image_108.png" /></figure>

<figure><img src="image_109.png" /></figure>

<figure><img src="image_110.png" /></figure>

<figure><img src="image_111.png" /></figure>

<figure><img src="image_112.png" /></figure>

<figure><img src="image_113.png" /></figure>

<figure><img src="image_114.png" /></figure>

<figure><img src="image_115.png" /></figure>

<figure><img src="image_116.png" /></figure>

<figure><img src="image_117.png" /></figure>

<figure><img src="image_118.png" /></figure>

<figure><img src="image_119.png" /></figure>

<figure><img src="image_120.png" /></figure>

<figure><img src="image_121.png" /></figure>

<figure><img src="image_122.png" /></figure>
Impact of algorithm

<figure><img src="image_123.png" /></figure>

<figure><img src="image_124.png" /></figure>

<figure><img src="image_125.png" /></figure>

<figure><img src="image_126.png" /></figure>

<figure><img src="image_127.png" /></figure>

<figure><img src="image_128.png" /></figure>

<figure><img src="image_129.png" /></figure>

<figure><img src="image_130.png" /></figure>

<figure><img src="image_131.png" /></figure>

<figure><img src="image_132.png" /></figure>

<figure><img src="image_133.png" /></figure>

<figure><img src="image_134.png" /></figure>

<figure><img src="image_135.png" /></figure>

<figure><img src="image_136.png" /></figure>
Algorithms

* Deletion-based [Belov and Marques-Silva, 2012]

* Addition-based [Gregoire et al, 2008; van Maaren and Wieringa, 2008]

* Dichotomic [Junker, 2004]

* Exploit duality [Bacchus and K, 2015]

<figure><img src="image_137.png" /></figure>
Algorithms

* Deletion-based [Belov and Marques-Silva, 2012]

* Addition-based [Gregoire et al, 2008; van Maaren and Wieringa, 2008]

* Dichotomic [Junker, 2004]

* Exploit duality [Bacchus and K, 2015]

⇒ All applicable to any set minimization problem

<figure><img src="image_138.png" /></figure>
Deletion based

$(x_1)$

$(x_2)$

$(x_3)$

$(\bar{x}_1, \bar{x}_2)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

<figure><img src="image_139.png" /></figure>

<figure><img src="image_140.png" /></figure>

<figure><img src="image_141.png" /></figure>

<figure><img src="image_142.png" /></figure>

<figure><img src="image_143.png" /></figure>

<figure><img src="image_144.png" /></figure>

<figure><img src="image_145.png" /></figure>

<figure><img src="image_146.png" /></figure>

<figure><img src="image_147.png" /></figure>

<figure><img src="image_148.png" /></figure>

<figure><img src="image_149.png" /></figure>

<figure><img src="image_150.png" /></figure>

<figure><img src="image_151.png" /></figure>

<figure><img src="image_152.png" /></figure>

<figure><img src="image_153.png" /></figure>

<figure><img src="image_154.png" /></figure>

<figure><img src="image_155.png" /></figure>

<figure><img src="image_156.png" /></figure>

<figure><img src="image_157.png" /></figure>
Deletion based

$$ (\bar{x}_2, \bar{x}_3) $$

$(x_1)$

$(x_2)$

$(x_3)$

$(\bar{x}_1, \bar{x}_2)$

$(\bar{x}_1, \bar{x}_3)$

<figure><img src="image_158.png" /></figure>

<figure><img src="image_159.png" /></figure>

<figure><img src="image_160.png" /></figure>

<figure><img src="image_161.png" /></figure>

<figure><img src="image_162.png" /></figure>

<figure><img src="image_163.png" /></figure>

<figure><img src="image_164.png" /></figure>

<figure><img src="image_165.png" /></figure>

<figure><img src="image_166.png" /></figure>

<figure><img src="image_167.png" /></figure>

<figure><img src="image_168.png" /></figure>

<figure><img src="image_169.png" /></figure>

<figure><img src="image_170.png" /></figure>

<figure><img src="image_171.png" /></figure>

<figure><img src="image_172.png" /></figure>

<figure><img src="image_173.png" /></figure>

<figure><img src="image_174.png" /></figure>
$$ (\bar{x}_2, \bar{x}_3) $$

$(x_1)$

$(x_2)$

$(x_3)$

$(\bar{x}_1, \bar{x}_2)$

$(\bar{x}_1, \bar{x}_3)$

✓ UNSAT

<figure><img src="image_175.png" /></figure>

<figure><img src="image_176.png" /></figure>

<figure><img src="image_177.png" /></figure>

<figure><img src="image_178.png" /></figure>

<figure><img src="image_179.png" /></figure>

<figure><img src="image_180.png" /></figure>

<figure><img src="image_181.png" /></figure>

<figure><img src="image_182.png" /></figure>

<figure><img src="image_183.png" /></figure>

<figure><img src="image_184.png" /></figure>

<figure><img src="image_185.png" /></figure>

<figure><img src="image_186.png" /></figure>

<figure><img src="image_187.png" /></figure>

<figure><img src="image_188.png" /></figure>

<figure><img src="image_189.png" /></figure>
Deletion based

$$ (\bar{x}_2, \bar{x}_3) $$

$(x_1)$

$(x_2)$

$(x_3)$

$(\bar{x}_1, \bar{x}_2)$

$(\bar{x}_1, \bar{x}_3)$

<figure><img src="image_190.png" /></figure>

<figure><img src="image_191.png" /></figure>

<figure><img src="image_192.png" /></figure>

<figure><img src="image_193.png" /></figure>

<figure><img src="image_194.png" /></figure>

<figure><img src="image_195.png" /></figure>

<figure><img src="image_196.png" /></figure>

<figure><img src="image_197.png" /></figure>

<figure><img src="image_198.png" /></figure>

<figure><img src="image_199.png" /></figure>

<figure><img src="image_200.png" /></figure>

<figure><img src="image_201.png" /></figure>

<figure><img src="image_202.png" /></figure>

<figure><img src="image_203.png" /></figure>

<figure><img src="image_204.png" /></figure>

<figure><img src="image_205.png" /></figure>

<figure><img src="image_206.png" /></figure>
Deletion based

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(x_1)$

$(x_2)$

$(x_3)$

$(\bar{x}_1, \bar{x}_2)$

<figure><img src="image_207.png" /></figure>

<figure><img src="image_208.png" /></figure>

<figure><img src="image_209.png" /></figure>

<figure><img src="image_210.png" /></figure>

<figure><img src="image_211.png" /></figure>

<figure><img src="image_212.png" /></figure>

<figure><img src="image_213.png" /></figure>

<figure><img src="image_214.png" /></figure>

<figure><img src="image_215.png" /></figure>

<figure><img src="image_216.png" /></figure>

<figure><img src="image_217.png" /></figure>

<figure><img src="image_218.png" /></figure>

<figure><img src="image_219.png" /></figure>

<figure><img src="image_220.png" /></figure>
$(x_1)$

$(x_2)$

$(x_3)$

$(\bar{x}_1, \bar{x}_2)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

✓ UNSAT

<figure><img src="image_221.png" /></figure>

<figure><img src="image_222.png" /></figure>

<figure><img src="image_223.png" /></figure>

<figure><img src="image_224.png" /></figure>

<figure><img src="image_225.png" /></figure>

<figure><img src="image_226.png" /></figure>

<figure><img src="image_227.png" /></figure>

<figure><img src="image_228.png" /></figure>

<figure><img src="image_229.png" /></figure>

<figure><img src="image_230.png" /></figure>

<figure><img src="image_231.png" /></figure>

<figure><img src="image_232.png" /></figure>

<figure><img src="image_233.png" /></figure>
Deletion based

$$ (\bar{x}_1, \bar{x}_3) $$

$$ (\bar{x}_2, \bar{x}_3) $$

$(x_1)$

$(x_2)$

$(x_3)$

$(\bar{x}_1, \bar{x}_2)$

<figure><img src="image_234.png" /></figure>

<figure><img src="image_235.png" /></figure>

<figure><img src="image_236.png" /></figure>

<figure><img src="image_237.png" /></figure>

<figure><img src="image_238.png" /></figure>

<figure><img src="image_239.png" /></figure>

<figure><img src="image_240.png" /></figure>

<figure><img src="image_241.png" /></figure>

<figure><img src="image_242.png" /></figure>

<figure><img src="image_243.png" /></figure>

<figure><img src="image_244.png" /></figure>

<figure><img src="image_245.png" /></figure>

<figure><img src="image_246.png" /></figure>

<figure><img src="image_247.png" /></figure>
Deletion based

$(\bar{x}_1, \bar{x}_2)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(x_1)$

$(x_2)$

$(x_3)$
Deletion based

$(\bar{x}_1, \bar{x}_2)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

X SAT

$(x_1)$

$(x_2)$

$(x_3)$

<figure><img src="image_248.png" /></figure>

<figure><img src="image_249.png" /></figure>

<figure><img src="image_250.png" /></figure>

<figure><img src="image_251.png" /></figure>

<figure><img src="image_252.png" /></figure>

<figure><img src="image_253.png" /></figure>

<figure><img src="image_254.png" /></figure>

<figure><img src="image_255.png" /></figure>

<figure><img src="image_256.png" /></figure>

<figure><img src="image_257.png" /></figure>

<figure><img src="image_258.png" /></figure>

<figure><img src="image_259.png" /></figure>

<figure><img src="image_260.png" /></figure>

<figure><img src="image_261.png" /></figure>
Deletion based

$$ (\bar{x}_1, \bar{x}_3) $$

$$ (\bar{x}_2, \bar{x}_3) $$

$(x_1)$

$(x_2)$

$(x_3)$

$(\bar{x}_1, \bar{x}_2)$

<figure><img src="image_262.png" /></figure>

<figure><img src="image_263.png" /></figure>

<figure><img src="image_264.png" /></figure>

<figure><img src="image_265.png" /></figure>

<figure><img src="image_266.png" /></figure>

<figure><img src="image_267.png" /></figure>

<figure><img src="image_268.png" /></figure>

<figure><img src="image_269.png" /></figure>

<figure><img src="image_270.png" /></figure>

<figure><img src="image_271.png" /></figure>

<figure><img src="image_272.png" /></figure>

<figure><img src="image_273.png" /></figure>

<figure><img src="image_274.png" /></figure>
Deletion based

$(x_3)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(x_1)$

$(x_2)$

$(\bar{x}_1, \bar{x}_2)$

<figure><img src="image_275.png" /></figure>

<figure><img src="image_276.png" /></figure>

<figure><img src="image_277.png" /></figure>

<figure><img src="image_278.png" /></figure>

<figure><img src="image_279.png" /></figure>

<figure><img src="image_280.png" /></figure>

<figure><img src="image_281.png" /></figure>

<figure><img src="image_282.png" /></figure>

<figure><img src="image_283.png" /></figure>

<figure><img src="image_284.png" /></figure>

<figure><img src="image_285.png" /></figure>

<figure><img src="image_286.png" /></figure>

<figure><img src="image_287.png" /></figure>

<figure><img src="image_288.png" /></figure>
$(x_3)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(x_1)$

$(x_2)$

$(\bar{x}_1, \bar{x}_2)$

✓ UNSAT

<figure><img src="image_289.png" /></figure>

<figure><img src="image_290.png" /></figure>

<figure><img src="image_291.png" /></figure>

<figure><img src="image_292.png" /></figure>

<figure><img src="image_293.png" /></figure>

<figure><img src="image_294.png" /></figure>

<figure><img src="image_295.png" /></figure>

<figure><img src="image_296.png" /></figure>

<figure><img src="image_297.png" /></figure>

<figure><img src="image_298.png" /></figure>

<figure><img src="image_299.png" /></figure>

<figure><img src="image_300.png" /></figure>

<figure><img src="image_301.png" /></figure>

<figure><img src="image_302.png" /></figure>
Deletion based

$(x_1)$

$(x_3)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(x_2)$

$(\bar{x}_1, \bar{x}_2)$

<figure><img src="image_303.png" /></figure>

<figure><img src="image_304.png" /></figure>

<figure><img src="image_305.png" /></figure>

<figure><img src="image_306.png" /></figure>

<figure><img src="image_307.png" /></figure>

<figure><img src="image_308.png" /></figure>

<figure><img src="image_309.png" /></figure>

<figure><img src="image_310.png" /></figure>

<figure><img src="image_311.png" /></figure>

<figure><img src="image_312.png" /></figure>

<figure><img src="image_313.png" /></figure>

<figure><img src="image_314.png" /></figure>

<figure><img src="image_315.png" /></figure>

<figure><img src="image_316.png" /></figure>
Deletion based

$(x_1)$

$(x_2)$

$(x_3)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(\bar{x}_1, \bar{x}_2)$

<figure><img src="image_317.png" /></figure>

<figure><img src="image_318.png" /></figure>

<figure><img src="image_319.png" /></figure>

<figure><img src="image_320.png" /></figure>

<figure><img src="image_321.png" /></figure>

<figure><img src="image_322.png" /></figure>

<figure><img src="image_323.png" /></figure>

<figure><img src="image_324.png" /></figure>

<figure><img src="image_325.png" /></figure>

<figure><img src="image_326.png" /></figure>

<figure><img src="image_327.png" /></figure>

<figure><img src="image_328.png" /></figure>

<figure><img src="image_329.png" /></figure>

<figure><img src="image_330.png" /></figure>
Deletion based

$(x_1)$

$(x_2)$

$(x_3)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(\bar{x}_1, \bar{x}_2)$

x SAT

<figure><img src="image_331.png" /></figure>

<figure><img src="image_332.png" /></figure>

<figure><img src="image_333.png" /></figure>

<figure><img src="image_334.png" /></figure>

<figure><img src="image_335.png" /></figure>

<figure><img src="image_336.png" /></figure>

<figure><img src="image_337.png" /></figure>

<figure><img src="image_338.png" /></figure>

<figure><img src="image_339.png" /></figure>

<figure><img src="image_340.png" /></figure>

<figure><img src="image_341.png" /></figure>

<figure><img src="image_342.png" /></figure>

<figure><img src="image_343.png" /></figure>

<figure><img src="image_344.png" /></figure>
Deletion based

$(x_1)$

$(x_3)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(x_2)$

$(\bar{x}_1, \bar{x}_2)$

<figure><img src="image_345.png" /></figure>

<figure><img src="image_346.png" /></figure>

<figure><img src="image_347.png" /></figure>

<figure><img src="image_348.png" /></figure>

<figure><img src="image_349.png" /></figure>

<figure><img src="image_350.png" /></figure>

<figure><img src="image_351.png" /></figure>

<figure><img src="image_352.png" /></figure>

<figure><img src="image_353.png" /></figure>

<figure><img src="image_354.png" /></figure>

<figure><img src="image_355.png" /></figure>

<figure><img src="image_356.png" /></figure>

<figure><img src="image_357.png" /></figure>

<figure><img src="image_358.png" /></figure>
Deletion based

$(x_1)$

$(x_3)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(x_2)$

$(\bar{x}_1, \bar{x}_2)$

<figure><img src="image_359.png" /></figure>

<figure><img src="image_360.png" /></figure>

<figure><img src="image_361.png" /></figure>

<figure><img src="image_362.png" /></figure>

<figure><img src="image_363.png" /></figure>

<figure><img src="image_364.png" /></figure>

<figure><img src="image_365.png" /></figure>

<figure><img src="image_366.png" /></figure>

<figure><img src="image_367.png" /></figure>

<figure><img src="image_368.png" /></figure>

<figure><img src="image_369.png" /></figure>

<figure><img src="image_370.png" /></figure>

<figure><img src="image_371.png" /></figure>

<figure><img src="image_372.png" /></figure>
Deletion based

$(x_1)$

$(x_3)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(x_2)$

$(\bar{x}_1, \bar{x}_2)$

x SAT

<figure><img src="image_373.png" /></figure>

<figure><img src="image_374.png" /></figure>

<figure><img src="image_375.png" /></figure>

<figure><img src="image_376.png" /></figure>

<figure><img src="image_377.png" /></figure>

<figure><img src="image_378.png" /></figure>

<figure><img src="image_379.png" /></figure>

<figure><img src="image_380.png" /></figure>

<figure><img src="image_381.png" /></figure>

<figure><img src="image_382.png" /></figure>

<figure><img src="image_383.png" /></figure>

<figure><img src="image_384.png" /></figure>

<figure><img src="image_385.png" /></figure>

<figure><img src="image_386.png" /></figure>
Deletion based

$(x_3)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(x_1)$

$(x_2)$

$(\bar{x}_1, \bar{x}_2)$

<figure><img src="image_387.png" /></figure>

<figure><img src="image_388.png" /></figure>

<figure><img src="image_389.png" /></figure>

<figure><img src="image_390.png" /></figure>

<figure><img src="image_391.png" /></figure>

<figure><img src="image_392.png" /></figure>

<figure><img src="image_393.png" /></figure>

<figure><img src="image_394.png" /></figure>

<figure><img src="image_395.png" /></figure>

<figure><img src="image_396.png" /></figure>

<figure><img src="image_397.png" /></figure>

<figure><img src="image_398.png" /></figure>

<figure><img src="image_399.png" /></figure>

<figure><img src="image_400.png" /></figure>
Deletion based

$(x_1)$

$(x_2)$

$(x_3)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(\bar{x}_1, \bar{x}_2)$

MUS!

<figure><img src="image_401.png" /></figure>

<figure><img src="image_402.png" /></figure>

<figure><img src="image_403.png" /></figure>

<figure><img src="image_404.png" /></figure>

<figure><img src="image_405.png" /></figure>

<figure><img src="image_406.png" /></figure>

<figure><img src="image_407.png" /></figure>

<figure><img src="image_408.png" /></figure>

<figure><img src="image_409.png" /></figure>

<figure><img src="image_410.png" /></figure>

<figure><img src="image_411.png" /></figure>

<figure><img src="image_412.png" /></figure>

<figure><img src="image_413.png" /></figure>
Exploiting Hitting Set duality

$$ (\bar{x}_1, \bar{x}_2) $$

$$ (\bar{x}_1, \bar{x}_3) $$

$$ (\bar{x}_2, \bar{x}_3) $$

$$ (x_1) $$

$$ (x_2) $$

$$ (x_3) $$

<figure><img src="image_414.png" /></figure>

<figure><img src="image_415.png" /></figure>

<figure><img src="image_416.png" /></figure>

<figure><img src="image_417.png" /></figure>

<figure><img src="image_418.png" /></figure>

<figure><img src="image_419.png" /></figure>

<figure><img src="image_420.png" /></figure>

<figure><img src="image_421.png" /></figure>

<figure><img src="image_422.png" /></figure>

<figure><img src="image_423.png" /></figure>
Exploiting Hitting Set duality

$(\bar{x}_1, \bar{x}_2)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(x_1)$

$(x_2)$

$(x_3)$

<figure><img src="image_424.png" /></figure>
Exploiting Hitting Set duality

$$ (\bar{x}_1, \bar{x}_2) $$

$$ (\bar{x}_1, \bar{x}_3) $$

$$ (\bar{x}_2, \bar{x}_3) $$

$$ (x_1) $$

$$ (x_2) $$

$$ (x_3) $$

<figure><img src="image_425.png" /></figure>

<figure><img src="image_426.png" /></figure>

<figure><img src="image_427.png" /></figure>

<figure><img src="image_428.png" /></figure>

<figure><img src="image_429.png" /></figure>

<figure><img src="image_430.png" /></figure>

<figure><img src="image_431.png" /></figure>

<figure><img src="image_432.png" /></figure>

<figure><img src="image_433.png" /></figure>

<figure><img src="image_434.png" /></figure>

<figure><img src="image_435.png" /></figure>
Exploiting Hitting Set duality

$(\bar{x}_1, \bar{x}_2)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(x_1)$

$(x_2)$

$(x_3)$

<figure><img src="image_436.png" /></figure>

<figure><img src="image_437.png" /></figure>

<figure><img src="image_438.png" /></figure>

<figure><img src="image_439.png" /></figure>

<figure><img src="image_440.png" /></figure>

<figure><img src="image_441.png" /></figure>

<figure><img src="image_442.png" /></figure>

<figure><img src="image_443.png" /></figure>

<figure><img src="image_444.png" /></figure>

<figure><img src="image_445.png" /></figure>

<figure><img src="image_446.png" /></figure>
Exploiting Hitting Set duality

$(\bar{x}_1, \bar{x}_2)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(x_1)$

$(x_2)$

$(x_3)$

<figure><img src="image_447.png" /></figure>
Exploiting Hitting Set duality

$$ (\bar{x}_1, \bar{x}_2) $$

$$ (\bar{x}_1, \bar{x}_3) $$

$$ (\bar{x}_2, \bar{x}_3) $$

$$ (x_1) $$

$$ (x_2) $$

$$ (x_3) $$
Exploiting Hitting Set duality

$(\bar{x}_1, \bar{x}_2)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(x_1)$

$(x_2)$

$(x_3)$

<figure><img src="image_448.png" /></figure>

<figure><img src="image_449.png" /></figure>

<figure><img src="image_450.png" /></figure>

<figure><img src="image_451.png" /></figure>

<figure><img src="image_452.png" /></figure>

<figure><img src="image_453.png" /></figure>

<figure><img src="image_454.png" /></figure>

<figure><img src="image_455.png" /></figure>

<figure><img src="image_456.png" /></figure>

<figure><img src="image_457.png" /></figure>

<figure><img src="image_458.png" /></figure>

<figure><img src="image_459.png" /></figure>

<figure><img src="image_460.png" /></figure>

<figure><img src="image_461.png" /></figure>

<figure><img src="image_462.png" /></figure>

<figure><img src="image_463.png" /></figure>

<figure><img src="image_464.png" /></figure>
Exploiting Hitting Set duality

$(\bar{x}_1, \bar{x}_2)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(x_1)$

$(x_2)$

$(x_3)$

No MCS

<figure><img src="image_465.png" /></figure>
Exploiting Hitting Set duality

$(\bar{x}_1, \bar{x}_2)$

$(\bar{x}_1, \bar{x}_3)$

$(\bar{x}_2, \bar{x}_3)$

$(x_1)$

$(x_2)$

$(x_3)$

MUS

<figure><img src="image_466.png" /></figure>

<figure><img src="image_467.png" /></figure>

<figure><img src="image_468.png" /></figure>

<figure><img src="image_469.png" /></figure>

<figure><img src="image_470.png" /></figure>

<figure><img src="image_471.png" /></figure>

<figure><img src="image_472.png" /></figure>

<figure><img src="image_473.png" /></figure>

<figure><img src="image_474.png" /></figure>

<figure><img src="image_475.png" /></figure>
Is it faster to

* do *m* SAT checks?
  - or -

* discover *k* MCSes?

<figure><img src="image_476.png" /></figure>

<figure><img src="image_477.png" /></figure>

<figure><img src="image_478.png" /></figure>

<figure><img src="image_479.png" /></figure>

<figure><img src="image_480.png" /></figure>

<figure><img src="image_481.png" /></figure>

<figure><img src="image_482.png" /></figure>

<figure><img src="image_483.png" /></figure>

<figure><img src="image_484.png" /></figure>

<figure><img src="image_485.png" /></figure>

<figure><img src="image_486.png" /></figure>

<figure><img src="image_487.png" /></figure>

<figure><img src="image_488.png" /></figure>

<figure><img src="image_489.png" /></figure>

<figure><img src="image_490.png" /></figure>
<figure><img src="image_491.png" /></figure>

<figure><img src="image_492.png" /></figure>
The way forward

* Faster SAT solving 😊

* Better use of existing SAT solvers

* Extract more information from the solver

* Improved MCS extraction

* A new algorithm?

<figure><img src="image_493.png" /></figure>
More problems

* Enumeration [Liffiton and Sakallah, 2008; Liffiton et al, 2015; Bacchus and K, 2016]

* Minimization [Ignatiev et al, 2013; Ignatiev et al, 2015; Liffiton et al, 2009; Marques-Silva and Previti, 2014]

* MCS extraction and enumeration [O'Callaghan et al, 2005; Bailey and Stuckey, 2005; Felfernig et al, 2014; Nöhrer et al, 2012; Marques-Silva et al, 2013; Bacchus et al, 2014; Bacchus and K, 2015; Mencía et al, 2015]

<figure><img src="image_494.png" /></figure>

<figure><img src="image_495.png" /></figure>

<figure><img src="image_496.png" /></figure>

<figure><img src="image_497.png" /></figure>

<figure><img src="image_498.png" /></figure>

<figure><img src="image_499.png" /></figure>

<figure><img src="image_500.png" /></figure>

<figure><img src="image_501.png" /></figure>

<figure><img src="image_502.png" /></figure>

<figure><img src="image_503.png" /></figure>

<figure><img src="image_504.png" /></figure>

<figure><img src="image_505.png" /></figure>

<figure><img src="image_506.png" /></figure>

<figure><img src="image_507.png" /></figure>

<figure><img src="image_508.png" /></figure>
Q?

<figure><img src="image_509.png" /></figure>

<figure><img src="image_510.png" /></figure>

<figure><img src="image_511.png" /></figure>

<figure><img src="image_512.png" /></figure>

<figure><img src="image_513.png" /></figure>

<figure><img src="image_514.png" /></figure>

<figure><img src="image_515.png" /></figure>

<figure><img src="image_516.png" /></figure>

<figure><img src="image_517.png" /></figure>

<figure><img src="image_518.png" /></figure>

<figure><img src="image_519.png" /></figure>

<figure><img src="image_520.png" /></figure>

<figure><img src="image_521.png" /></figure>

<figure><img src="image_522.png" /></figure>