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

HAL
open science

# How Computers Break (Serious) Puzzles with logic and (a different breed of) learning

Thomas Schiex

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

## To cite this version:

Thomas Schiex. How Computers Break (Serious) Puzzles with logic and (a different breed of) learning. French Académie des sciences Symposium on “Machine Learning for Artificial Intelligence”, Feb 2018, Paris, France. hal-02786911

HAL Id: hal-02786911

https://hal.inrae.fr/hal-02786911

Submitted on 5 Jun 2020

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published 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_3.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# How Computers Break (Serious) Puzzles
with logic and (a different breed of) learning

Thomas Schiex

département
MA INRA
TOULOUSE SCIENCE & IMPACT

February 2018

Académie des sciences, Paris, France
<figure><img src="image_4.png" /></figure>

Human beings

* Easily rely on quick “intuitions” (ill-defined problems)

* Extreme rigor is painful and slow (logic/arithmetic)

Als (computers)

* Accessible to some “intuition” (problems defined by data)

* Fast and extreme rigor is the default (1 billion op./sec)

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

Human beings

* Easily rely on quick “intuitions” (ill-defined problems)

* Extreme rigor is painful and slow (logic/arithmetic)

Als (computers)

* Accessible to some “intuition” (problems defined by data)

* Fast and extreme rigor is the default (1 billion op./sec)

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

It was expected that machines would show superhuman “logical reasoning” performances
<figure><img src="image_8.png" /></figure>

Human beings

* Easily rely on quick “intuitions” (ill-defined problems)

* Extreme rigor is painful and slow (logic/arithmetic)

Als (computers)

* Accessible to some “intuition” (problems defined by data)

* Fast and extreme rigor is the default (1 billion op./sec)

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

It was expected that machines would show superhuman "logical reasoning" performances

1955: Newell & Simon "Logic Theorist" proved 38 of the 52 theorems in the *Principia Mathematica* (Russel and Whitehead), and even corrected a proof in it.
NP-hard problems (Cook-Levin, 1970s)

* Some problems seem intrisically hard (for AIs at least)

* Worst case asymptotic exponential time ($P \neq NP$)
NP-hard problems

(Cook-Levin, 1970s)

* Some problems seem intrisically hard (for AIs at least)

* Worst case asymptotic exponential time ($P \neq NP$)

$n^2 \times n^2$ Sudoku

* NP-complete, $9 \times 9$: $10^{80}$ cases

* $10^{51}$ ages of the universe to examine them all

* Fast brute force will fail

<figure><img src="image_10.png" /></figure>
NP-hard problems

(Cook-Levin, 1970s)

* Some problems seem intrisically hard (for AIs at least)

* Worst case asymptotic exponential time ($P \neq NP$)

$n^2 \times n^2$ Sudoku

* NP-complete, 9 × 9: $10^{80}$ cases

* $10^{51}$ ages of the universe to examine them all

* Fast brute force will fail

<figure><img src="image_11.png" /></figure>
NP-hard problems

(Cook-Levin, 1970s)

* Some problems seem intrisically hard (for AIs at least)

* Worst case asymptotic exponential time ($P \neq NP$)

$n^2 \times n^2$ Sudoku

* NP-complete, $9 \times 9$: $10^{80}$ cases

* $10^{51}$ ages of the universe to examine them all

* Fast brute force will fail

<figure><img src="image_12.png" /></figure>
NP-hard problems

(Cook-Levin, 1970s)

* Some problems seem intrisically hard (for AIs at least)

* Worst case asymptotic exponential time ($P \neq NP$)

$n^2 \times n^2$ Sudoku

* NP-complete, $9 \times 9$: $10^{80}$ cases

* $10^{51}$ ages of the universe to examine them all

* Fast brute force will fail

* Can be solved in milliseconds

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

Logic

From a well defined problem to a solution

* We have a set of variables

(Sudoku cells contain a number from 1 to 9)

$X_1$

$X_2$

$X_3$

$X_4$

$X_5$

$X_6$
<figure><img src="image_15.png" /></figure>

Logic

From a well defined problem to a solution

* We have a set of variables

(Sudoku cells contain a number from 1 to 9)

* We have a set of properties on these variables

(all different rows, columns, super-cells)

<figure><img src="image_16.png" /></figure>
Logic

From a well defined problem to a solution

* We have a set of variables

(Sudoku cells contain a number from 1 to 9)

* We have a set of properties on these variables

(all different rows, columns, super-cells)

* We want to find an input that satisfies all properties (or prove none exists: refutation).

<figure><img src="image_17.png" /></figure>
## Intuition (DL)

From examples to a classifier

* We have a set of digital inputs (in $B^n$) and output (class: one bit).

* We want a function that best predicts seen (and unseen) data in most cases.

<figure><img src="image_18.png" /></figure>
Intuition (DL)

From examples to a classifier

* We have a set of digital inputs (in $\mathbb{B}^n$) and output (class: one bit).

* We want a function that best predicts seen (and unseen) data in most cases.

<figure><img src="image_19.png" /></figure>
## Technological progress

* Increasingly complex useful objects planes, computers, software, cars, Als

* That must be highly reliable (lives at stake)

* We cannot fully get them under control anymore

## Increasing system complexity

* Hardware: Pentium FDIV bug (1994, 3.1 million transistors)

* Software: the Therac-25 (radiation-therapy) kills 6 patients

* Tesla cars: said to carry 100 millions lines of codes

* Convolutional NN: may have billions of parameters
<figure><img src="image_20.png" /></figure>

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

Exponential complexity

[Credit: Kumar, DARPA, cited in Computer World magazine]

Note: *rough estimates, for propositional reasoning*

**Variables**

**Rules (Constraints)**
## SAT

* A set of Boolean variables $x_i$

* A set of clauses (disjunction of variables or negation of) $(-x_1 \lor x_7)$

* Must satisfy all clauses (or prove impossible)

* Semantics: defines a function from $\mathbb{B}^n$ to $\mathbb{B}$
# Propositional logic as an example (SAT)

## SAT

A set of Boolean variables $x_i$

A set of clauses (disjunction of variables or negation of) ($\neg x_1 \lor x_7$)

Must satisfy all clauses (or prove impossible)

Semantics: defines a function from $\mathbb{B}^n$ to $\mathbb{B}$

## Sudoku

A cell $(i, j)$ contains $k$ $x_{ijk}$ true

At least one number per cell $i, j$ $(x_{ij1} \lor \dots \lor x_{ij9})$

At most one number per cell $i, j$ ($\forall k > k' \neg x_{ijk} \lor \neg x_{ijk'}$)

Cell $(i, j)$ and $(i, j')$ must be different ($\neg x_{ijk} \lor \neg x_{ij'k}$)
More sophisticated/practical function description

* propositions over theories SAT Modulo Theory⁹

* non Boolean variables Constraint Satisfaction, Constraint Programming³⁰

* numerical output Weighted MaxSAT²⁵/CSP,⁵ Graphical models¹⁸
More sophisticated/practical function description

* propositions over theories

SAT Modulo Theory⁹

* non Boolean variables

Constraint Satisfaction, Constraint Programming³⁰

* numerical output

Weighted MaxSAT²⁵/CSP,⁵ Graphical models¹⁸

<figure><img src="image_22.png" /></figure>
NP-complete: can express all NP-complete problems

* the logical puzzles you like (Sudoku, Nonograms...)

* or not (configuration, scheduling, test pattern generation...)

* robot planning

* digital circuit verification (Bounded Model Checking)

* or software verification (FOL, grounding, abstraction)
NP-complete: can express all NP-complete problems

* the logical puzzles you like (Sudoku, Nonograms...)

* or not (configuration, scheduling, test pattern generation...)

* robot planning

* digital circuit verification (Bounded Model Checking)

* or software verification (FOL, grounding, abstraction)

NP-complete, so intractable

Standard argument for less realistic problem reformulation, heuristics or stochastic search
NP-complete: can express all NP-complete problems

* the logical puzzles you like (Sudoku, Nonograms...)

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

* or not (configuration, scheduling, test pattern generation...)

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

SIEMENS THALES

* robot planning

(Rosetta-Philae probe plan, CP, LAAS/Toulouse)

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

* digital circuit verification (Bounded Model Checking)

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

IBM

* or software verification (FOL, grounding, abstraction)

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

G

cādence

NP-complete, so intractable

Standard argument for less realistic problem reformulation, heuristics or stochastic search

Real SAT instances with millions of variables/clauses can be solved (with a proof)
p cnf 51639 368352
-1 7 0
-1 6 0
-1 5 0
-1 -4 0
-1 3 0
-1 2 0
-1 -8 0
-9 15 0
-9 14 0
-9 13 0
-9 -12 0
-9 11 0
-9 10 0
-9 -16 0

51, 639 variables, 368, 352

constraints

$$ \neg x_1 \lor x_7 $$

$$ \neg x_1 \lor x_6 $$

...
185 -9 0

185 -1 0

177 169 161 153 145 137 129

121 113 105 97 89 81 73 65 57

49 41 33 25 17 9 1 -185 0

186 -187 0

186 -188 0

...

$(x_{177} \lor x_{169} \lor x_{161} \lor x_{153} \lor \cdots \lor x_{17} \lor x_9 \lor x_1 \lor \neg x_{185})$
<figure><img src="image_28.png" /></figure>

10236 -10050 0

10236 -10051 0

10236 -10235 0

10008 10009 10010 10011 10012 10013 10014 10015 10016 10017 10018

10019 10020 10021 10022 10023 10024 10025 10026 10027 10028 10029

10030 10031 10032 10033 10034 10035 10036 10037 10038 10039 10039

10089 10090 10091 10092 10093 10094 10095 10096 10097 10098 10099

10100 10101 10102 10103 10104 10105 10106 10107 10108 -55 -54 53 -52

-51 50 10047 10048 10049 10050 10051 10235 -10236 0

10237 -10008 0

10237 -10009 0

10237 -10010 0

...
-7 260 0

7 -260 0

1072 1070 0

-15 -14 -13 -12 -11 -10 0

-15 -14 -13 -12 -11 10 0

-15 -14 -13 -12 11 -10 0

-15 -14 -13 -12 11 10 0

-7 -6 -5 -4 -3 -2 0

-7 -6 -5 -4 -3 2 0

-7 -6 -5 -4 3 -2 0

-7 -6 -5 -4 3 2 0

185 0
-7 260 0
7 -260 0
1072 1070 0
-15 -14 -13 -12 -11 -10 0
-15 -14 -13 -12 -11 10 0
-15 -14 -13 -12 11 -10 0
-15 -14 -13 -12 11 10 0
-7 -6 -5 -4 -3 -2 0
-7 -6 -5 -4 -3 2 0
-7 -6 -5 -4 3 -2 0
-7 -6 -5 -4 3 2 0
185 0

Search space

$2^{50,000} \approx 3.1 \ 10^{15,051}$
-7 260 0
7 -260 0
1072 1070 0

-15 -14 -13 -12 -11 -10 0
-15 -14 -13 -12 -11 10 0
-15 -14 -13 -12 11 -10 0
-15 -14 -13 -12 11 10 0

-7 -6 -5 -4 -3 -2 0
-7 -6 -5 -4 -3 2 0
-7 -6 -5 -4 3 -2 0
-7 -6 -5 -4 3 2 0
185 0

Search space

$2^{50,000} \approx 3.1 \ 10^{15,051}$

Solved in one second
-7 260 0
7 -260 0
1072 1070 0
-15 -14 -13 -12 -11 -10 0
-15 -14 -13 -12 -11 10 0
-15 -14 -13 -12 11 -10 0
-15 -14 -13 -12 11 10 0
-7 -6 -5 -4 -3 -2 0
-7 -6 -5 -4 -3 2 0
-7 -6 -5 -4 3 -2 0
-7 -6 -5 -4 3 2 0
185 0

Search space

$2^{50,000} \approx 3.1 \ 10^{15,051}$

Solved in one second

How does it work?
Consensus/Resolution (1960's)⁸,²⁹

$$ \frac{\overbrace{(x_1 \lor l_1 \lor \dots \lor l_n)}^L \quad \overbrace{(\neg x_1 \lor r_1 \lor \dots \lor r_m)}^R}{(L \lor R)} $$
Boolean Constraint Propagation (BCP): unit clauses⁷ (L or R empty)

$$ \frac{(x_1) \quad (\neg x_1 \lor \overbrace{r_1 \lor \dots \lor r_m}^R)}{(R)} $$
Boolean Constraint Propagation (BCP): unit clauses⁷ (L or R empty)

$$ \frac{(x_1) \quad (\neg x_1 \lor \overbrace{r_1 \lor \dots \lor r_m}^R)}{(R)} $$

* A clause is shortened by one literal
Boolean Constraint Propagation (BCP): unit clauses⁷ (L or R empty)

$$ \frac{(x_1) \quad (\neg x_1 \lor \overbrace{r_1 \lor \dots \lor r_m}^R)}{(R)} $$

* A clause is shortened by one literal

* This may create new unit clauses (propagation)
Boolean Constraint Propagation (BCP): unit clauses⁷ (L or R empty)

$$ \frac{(x_1) \quad (\neg x_1 \lor \overbrace{r_1 \lor \dots \lor r_m}^R)}{(R)} $$

* A clause is shortened by one literal

* This may create new unit clauses (propagation)

* If the empty clause ☐ appears: no solution
Logic: Try to guess and reconsider (DPLL⁷)

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

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

SAT state-of-the-art in 1990

Hundreds of variables

Thousands of clauses
Long line of research in “symbolic” Artificial Intelligence³,¹⁰,²³,²⁴,³²

* Trace back failure to guesses through propagationᵃ

* Do backward resolution from conflict

* Add a new implied clause to the set of clauses

* Forces to reconsider an earlier guess

* Prevents refailing for a related reason (safe generalization)

Learns a more effective formulation of the problem as it solves it

<footnote>ᵃRichard M Stallman and Gerald J Sussman. "Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis". In: *Artificial intelligence* 9.2 (1977), pp. 135–196.</footnote>
Learning by "Activity based heuristics"²⁶

* On-line estimation of how often a variable is involved in recent clauses/failures

* Try guessing this variable first

Learns weak spots in the problem as it is solved (safe)
A lot of free data and free code...

* International competitions (> 50,000 benchmarks with many real problems)

* Open source solvers (autocatalytic)

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

<figure><img src="image_32.png" /></figure>
A lot of free data and free code...

* International competitions (> 50,000 benchmarks with many real problems)

* Open source solvers (autocatalytic)

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

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

Strong French presence

MADE IN
FRANCE

* Award winning solvers

(Glucose,² toulbar2¹⁵)

* Constraint programming solver/startup

(Choco)

* Strong presence in international conferences

(# of accepted papers in CP⁴)
A conjecture in combinatorics $\infty$

When one splits $\mathbb{N}$ in 2, one part must contain a Pythagorean triple ($a^2 = b^2 + c^2$)
A conjecture in combinatorics

∞

When one splits $N$ in 2, one part must contain a Pythagorean triple

$$ (a^2 = b^2 + c^2) $$

No known proof, puzzled mathematicians for decades (one offered a 100 $ reward)
A conjecture in combinatorics $\infty$

When one splits $\mathbb{N}$ in 2, one part must contain a Pythagorean triple ($a^2 = b^2 + c^2$)

No known proof, puzzled mathematicians for decades (one offered a 100 $ reward)

SAT solver proof$^{14,22}$

200 TB proof, compressed to 86 GB (stronger proof system)$^a$

<footnote>$^a$Oliver Kullmann. "The Science of Brute Force". In: *Communications of the ACM* (2017).</footnote>
<figure><img src="image_35.png" /></figure>

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

Whether it's maths or not...

Size matters!

* Not only there exists true unprovable statements (in powerful enough consistent sets of axioms¹²)

* There may be true provable statements we will never be able to prove because of their extremely long proofs²⁰

<figure><img src="image_37.png" /></figure>
# Is it bio-compatible?

## Biology

* Many discrete object ({A, T/U, G, C}, amino acids, genes, alleles, enzymes...)

* Lots of experimental data
# Is it bio-compatible?

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

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

## Biology

* Many discrete object ({{A, T/U, G, C}}, amino acids, genes, alleles, enzymes...)

* Lots of experimental data

## Exploiting Data + knowledge: Machine Learning

* (Stochastic) models can be built from knowledge and data

* And used to predict a "Most Likely/Optimal State" ⇒ easily NP-hard
<figure><img src="image_40.png" /></figure>

## Biology

* Many discrete object ({{A, T/U, G, C}}, amino acids, genes, alleles, enzymes...)

* Lots of experimental data

<figure><img src="image_41.png" /></figure>
## Most active molecules of life

Sequence of “amino-acids”, each chosen among a set of 20 natural ones

## Folding

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

Transporter, binder, regulator, motor, catalyst...

Hemoglobin, TAL effector, ATPase, dehydrogenases...
## Most active molecules of life

Sequence of “amino-acids”, each chosen among a set of 20 natural ones

## Inverse folding

Fiber →

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

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

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

Transporter, binder, regulator, motor, catalyst...

Hemoglobin, TAL effector, ATPase, dehydrogenases...
## Eco-friendly chemical/structural nano-agents

* New catalysts for biomass transformation (biofuels, food and feed, cosmetics...),

* New drugs for medicine

* New components for nanotechnologies
## Eco-friendly chemical/structural nano-agents

* New catalysts for biomass transformation (biofuels, food and feed, cosmetics...),

* New drugs for medicine

* New components for nanotechnologies

20ⁿ sequences! intractable for experimental techniques
<figure><img src="image_46.png" /></figure>

## Eco-friendly chemical/structural nano-agents

* New catalysts for biomass transformation (biofuels, food and feed, cosmetics...),

* New drugs for medicine

* New components for nanotechnologies

20ⁿ sequences!

intractable for experimental techniques

## CPD: From bits to atoms

From information to functional matter

* mind blowing mass 3d printing-like capacities at atomic level (bacterias)

* structural and functional purposes (powerful origami)

* produced new folds,¹⁹ catalysts,³¹ nano-components³⁶
## Ingredients

* Full atom model of a protein backbone (assumed to be rigid)

* Catalog of all 20 amino acids in different conformations (≈ 400 overall)

* Full atom energy function (bonds, electrostatics, solvant, statistics...)

* Maximum stability ≡ Minimum energy NP-hard²⁸

<figure><img src="image_47.png" /></figure>
Large input (> 1GB)

NP-hard problem

Toulbar2 is able to...

* provide a proven minimum energy solution

* exhaustively enumerate sequences close to it

* in spaces of size > $10^{200}$

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

Showed that an highly tuned biased Monte Carlo increasingly fails to find the optimal sequenceª

<footnote>ªDavid Simoncini et al. “Guaranteed Discrete Energy Optimization on Large Protein Design Problems”. In: *Journal of Chemical Theory and Computation* 11.12 (2015), pp. 5980–5989. DOI: 10.1021/acs.jctc.5b00594.</footnote>
<figure><img src="image_49.png" /></figure>

Asymptote: Size matters!

Asymptotic convergence can be arbitrarily slow...
C8 pseudo-symmetric 2OVP symmetrized into a nano-component

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

<figure><img src="image_51.png" /></figure>
C8 pseudo-symmetric 2OVP symmetrized into a nano-component

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

Tako: (R)evolution + Rosetta/talaris14

8 fold

2OVP

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

Tako

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

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

<figure><img src="image_56.png" /></figure>
C8 pseudo-symmetric 2OVP symmetrized into a nano-component

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

Tako: (R)evolution + Rosetta/talaris14 8 fold

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

Ika: toulbar2 + talaris14 4 fold

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

<figure><img src="image_60.png" /><figcaption>Ika</figcaption></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>
C8 pseudo-symmetric 2OVP symmetrized into a nano-component

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

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

Ika: toulbar2 + talaris14

4 fold

2OVP

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

Tako

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

Ika

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

8

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

4

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

2

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

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

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

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

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

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

## Assemble as 8-bladed propeller

* Ika* more stable than Tako8

* Temperature

* Chemical denaturation

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

<figure><img src="image_80.png" /></figure>
## Asymptotes: size matters

### NP is not exactly as we tend to think

* Als have made drastic progress in their logical capacities

* This progress also comes from (gradient-free) learning

* More progress is needed to supplement our limited human capacities

## Synergies between Logic and Intuition

* Logic can analyze and exploit learnt models (not only Neural Nets)

* Intuition can help logic without tainting it (guidance)
<figure><img src="image_81.png" /></figure>

Al/toulbar2

S. de Givry (INRA)

G. Katsirelos (INRA)

M. Zytnicki (PhD, INRA)

D. Allouche (INRA)

H. Nguyen (PhD, INRA)

M. Cooper (IRIT, Toulouse)

J. Larrosa (UPC, Spain)

F. Heras (UPC, Spain)

M. Sanchez (Spain)

E. Rollon (UPC, Spain)

P. Meseguer (CSIC, Spain)

G. Verfaillie (ONERA, ret.)

JH. Lee (CU, Hong Kong)

C. Bessiere (LIMM, Montpellier)

JP. Métivier (GREYC, Caen)

S. Loudni (GREYC, Caen)

M. Fontaine (GREYC, Caen)

Protein Design

A. Voet (KU Leuven)

D. Simoncini (INSA, Toulouse)

S. Barbe (INSA, Toulouse)

S. Traoré (PhD, CEA)

C. Viricel (PhD)

RosettaCommons (U. Washington)

W. Sheffler (U. Washington)

PyRosetta (U. John Hopkins)

B. Donald (U. North Carolina)

K. Roberts (U. North Carolina)

T. Simonson (Polytechnique)

J. Cortes (LAAS/CNRS)
[1] Albert Atserias, Johannes Klaus Fichte, and Marc Thurley. "Clause-learning algorithms with many restarts and bounded-width resolution". In: *Journal of Artificial Intelligence Research* 40 (2011), pp. 353-373.

[2] Gilles Audemard and Laurent Simon. "Predicting Learnt Clauses Quality in Modern SAT Solvers". In: *International Joint Conference in AI. Vol. 9. 2009, pp. 399-404*.

[3] Maurice Bruynooghe and Luis Moniz Pereira. "Deduction revision by intelligent backtracking". In: (1984).

[4] Association for Constraint Programming. *Publication statistics in CP per country every year*. URL http://www.a4cp.org/cparchive/countries_by_year.

[5] Martin C Cooper et al. "Soft arc consistency revisited". In: *Artificial Intelligence* 174.7 (2010), pp. 449-478.

[6] Matthieu Courbariaux et al. "Binarized neural networks: Training deep neural networks with weights and activations constrained to+1 or-1". In: *arXiv preprint arXiv:1602.02830* (2016).

[7] Martin Davis, George Logemann, and Donald Loveland. "A machine program for theorem-proving". In: *Communications of the ACM* 5.7 (1962), pp. 394-397.

[8] Martin Davis and Hilary Putnam. "A computing procedure for quantification theory". In: *Journal of the ACM (JACM)* 7.3 (1960), pp. 201-215.

[9] Leonardo De Moura and Nikolaj Bjarner. "Satisfiability modulo theories: introduction and applications". In: *Communications of the ACM* 54.9 (2011), pp. 69-77.

[10] Rina Dechter. "Enhancement schemes for constraint processing: Backjumping, learning, and cutset decomposition". In: *Artificial Intelligence* 41.3 (1990), pp. 273-312.
<figure><img src="image_82.png" /></figure>

[11] S Foissac et al. "Genome Annotation in Plants and Fungi: EuGène as a Model Platform". In: Current Bioinformatics 3.2 (2008), pp. 87-97.

[12] Kurt Gödel. "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I". In: Monatshefte für mathematik und physik 38.1 (1931), pp. 173-198.

[13] Carla P Gomes, Bart Selman, Henry Kautz, et al. "Boosting combinatorial search through randomization". In: AAAI/IAAI 98 (1998), pp. 431-437.

[14] Marijn JH Heule, Oliver Kullmann, and Victor W Marek. "Solving and verifying the boolean pythagorean triples problem via cube-and-conquer". In: International Conference on Theory and Applications of Satisfiability Testing. Springer. 2016, pp. 228-245.

[15] Barry Hurley et al. "Multi-language evaluation of exact solvers in graphical model discrete optimization". In: Constraints (2016), pp. 1-22.

[16] Peter Jeavons and Justyna Petke. "Local consistency and SAT-solvers". In: Journal of Artificial Intelligence Research 43 (2012), pp. 329-351.

[17] Guy Katz et al. "Reluplex: An efficient SMT solver for verifying deep neural networks". In: International Conference on Computer Aided Verification. Springer. 2017, pp. 97-117.

[18] Daphne Koller and Nir Friedman. *Probabilistic graphical models: principles and techniques*. MIT press, 2009.

[19] Brian Kuhlman et al. "Design of a novel globular protein fold with atomic-level accuracy". In: science 302.5649 (2003), pp. 1364-1368.
<figure><img src="image_83.png" /></figure>

[20] Oliver Kullmann. "The Science of Brute Force". In: *Communications of the ACM* (2017).

[21] John Lafferty, Andrew McCallum, and Fernando CN Pereira. "Conditional random fields: Probabilistic models for segmenting and labeling sequence data". In: *Proc. of the 18th International Conference on Machine Learning (ICML)*. 2001.

[22] Evelyn Lamb. "Maths proof smashes size record: supercomputer produces a 200-terabyte proof-but is it really mathematics?" In: *Nature* 534.7605 (2016), pp. 17-19.

[23] João P Marques-Silva and Karem A Sakallah. "GRASP: A search algorithm for propositional satisfiability". In: *IEEE Transactions on Computers* 48.5 (1999), pp. 506-521.

[24] David A McAllester. *An Outlook on Truth Maintenance*. Tech. rep. Massachusetts Inst Of Tech, Cambridge, Artificial Intelligence Lab., 1980.

[25] Antonio Morgado et al. "Iterative and core-guided MaxSAT solving: A survey and assessment". In: *Constraints* 18.4 (2013), pp. 478-534.

[26] Matthew W Moskewicz et al. "Chaff: Engineering an efficient SAT solver". In: *Proceedings of the 38th annual Design Automation Conference*. ACM, 2001, pp. 530-535.

[27] Nina Narodytska et al. "Verifying properties of binarized deep neural networks". In: *arXiv preprint arXiv:1709.06662* (2017).

[28] Niles A Pierce and Erik Winfree. "Protein design is NP-hard". In: *Protein engineering* 15.10 (2002), pp. 779-782.

[29] John Alan Robinson. "A machine-oriented logic based on the resolution principle". In: *Journal of the ACM (JACM)* 12.1 (1965), pp. 23-41.

[30] Francesca Rossi, Peter Van Beek, and Toby Walsh. *Handbook of constraint programming*. Elsevier, 2006.
<figure><img src="image_84.png" /></figure>

[31] Daniela Röthlisberger et al. "Kemp elimination catalysts by computational enzyme design". In: *Nature* 453.7192 (2008), p. 190.

[32] Thomas Schiex and Gérard Verfaillie. "Nogood recording for static and dynamic constraint satisfaction problems". In: *International Journal on Artificial Intelligence Tools* 3.02 (1994), pp. 187-207.

[33] David Simoncini et al. "Guaranteed Discrete Energy Optimization on Large Protein Design Problems". In: *Journal of Chemical Theory and Computation* 11.12 (2015), pp. 5980-5989. DOI: 10.1021/acs.jctc.5b00594.

[34] Richard M Stallman and Gerald J Sussman. "Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis". In: *Artificial intelligence* 9.2 (1977), pp. 135-196.

[35] Christian Szegedy et al. "Intriguing properties of neural networks". In: *arXiv preprint arXiv:1312.6199* (2013).

[36] Arnout RD Voet et al. "Computational design of a self-assembling symmetrical β-propeller protein". In: *Proceedings of the National Academy of Sciences* 111.42 (2014), pp. 15102-15107.
We do not understand the sources of their efficiency

CDCL solvers have an expected polynomial $O(n^k)$ runtime on SAT instances whose primal (Gaifman) graph has treewidth $k$.

Without ever trying to compute a treewidth/decomposition (NP hard).
Go on a $n \times n$ goban is PSPACE-hard

* PSPACE-hard to decide if there is a winning strategy

* AlphaGo 0 does not solve 19 × 19 Go

* It plays better than humans (and that's amazing!)
<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>
Additional ingredients (patented for some)

(I) stops, restarts with a better understanding of the problem¹³

(I) forgets learnt information predicted as “useless” (Glue clauses²)

• Lazy data structures²⁶

* Absolutely reliable combination of logic and intuition

* but we don't really understand why it can be so efficient¹,¹⁶
Neural nets and safety critical settings

It doesn't seem too hard to fool a standard Convolutional Neural Netª

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

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

<footnote>ªChristian Szegedy et al. “Intriguing properties of neural networks”. In: arXiv preprint arXiv:1312.6199 (2013).</footnote>
Neural nets and safety critical settings

It doesn't seem too hard to fool a standard Convolutional Neural Netª

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

<footnote>ªChristian Szegedy et al. “Intriguing properties of neural networks”. In: arXiv preprint arXiv:1312.6199 (2013).</footnote>
Neural nets and safety critical settings

It doesn't seem too hard to fool a standard Convolutional Neural Netª

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

<footnote>ªChristian Szegedy et al. “Intriguing properties of neural networks”. In: *arXiv preprint arXiv:1312.6199* (2013).</footnote>
Binarized Deep NN: $\pm 1$ activations/weights$^6$

* Lin: affine transformation with learnt binary weights (float bias).

* Bn: (Batch normalization) rescaling with learnt floats.

* Bin: binarization using the *Sign* function.

<figure><img src="image_94.png" /></figure>
Binarized Deep NN: ±1 activations/weights⁶

* Lin: affine transformation with learnt binary weights (float bias).

* Bn: (Batch normalization) rescaling with learnt floats.

* Bin: binarization using the *Sign* function.

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

A learnt block can be described as a SATª formula

(SMT(LI)¹⁷ for ReLU)

<footnote>ªNina Narodytska et al. “Verifying properties of binarized deep neural networks”. In: arXiv preprint arXiv:1709.06662 (2017).</footnote>
Adversarial Robustness of a classifier

A positive test input cannot be slightly modified to change class
<figure><img src="image_96.png" /></figure>

## Adversarial Robustness of a classifier

A positive test input cannot be slightly modified to change class

## Certified robustness by SAT

As a SAT formula: Neural Net + input + bounded perturbation + missclassification
<figure><img src="image_97.png" /></figure>

Adversarial Robustness of a classifier

A positive test input cannot be slightly modified to change class

Certified robustness by SAT

As a SAT formula: Neural Net + input + bounded perturbation + missclassification

* MNIST dataset, 4 blocks BNN with 100 to 200 neurons per layer, $L_\infty$ norm

* Millions of clauses: Glucose² certifies (non) robustness for most input in < 5' CPU time

<figure><img src="image_98.png" /></figure>
# Deciphering genomic DNA

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

DNA

<figure><img src="image_100.png" /></figure>
# Segmenting genomic DNA

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

### GENE 1

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

TSS

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

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

Polypeptide

TSS

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

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

Regulatory RNA

TSS

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

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

Transfer RNA

### GENE 2

### GENE 3
GENE 1

TSS

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

GENE 2

TSS

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

GENE 3

TSS

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

Transfer RNA

Similarities

RNA-Seq

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

UniProt

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

Conservation

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

Sequence stats

Markov chains

Site predictors

SVM

Neural nets
Optimization + decomposable probability distribution (Semi-CRF)²¹

* Derived from an actual human processor (S. Rumbauts, PhD)ᵃ

* Discriminative learning (don't try to model evidence!)

* Optimizes an empirical loss function (performance on a testing set: quality is crucial)

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

Prediction is in P

Main difficulty: collecting evidence, training and testing.

<footnote>ᵃS Foissac et al. "Genome Annotation in Plants and Fungi: EuGène as a Model Platform". In: *Current Bioinformatics* 3.2 (2008), pp. 87-97.</footnote>