# Appendix: Experimental support for models and counter-examples generation

Alt-Ergo is specialized in program verification, and thus focuses on proving that formulas are Valid (UNSAT).

However, even in the context of program verification, it may be useful to build counter-examples, explaining to the programmer why the formulas are Invalid.

In the context of SAT (Invalid being its negative formulation) this can be interpreted as the construction of a model for each formula which is satisfiable.

Alt-Ergo’s support for models and counter-examples is still experimental, but should be extended in future versions.

## Options for model generation

Two options are available to create models/counter-examples. When alt-ergo is used in command line, they correspond to --model and --interpretation.

Their maximum level are respectively --model=complete and --interpretation = 3.

Using them, here is the kind of output you could get.

Example: No model generation

logic x, y: int

goal g:not(
x+y = 8  and
x*y = 12
)


Example: Using model = complete

logic x, y: int

goal g:not(
x+y = 8  and
x*y = 12
)


Example: Using interpretation = 3

logic x, y: int

goal g:not(
x+y = 8  and
x*y = 12
)


## Examples

All of the code boxes below have been set up with interpretation = 3.

### Simple equations

Model generation can be used to solve simple equations.

All four examples below come from the fun book “SAT/SMT by example” by Dennis Yurichev. Don’t hesitate to check his book for more fun applications of SMT-solvers, such as cracking programs using rand, solving nonograms, checking hacks from Henry Warren’s “Hacker’s delight”, or superoptimization.

School-level system of equation

The following code solves this simple system of equations. logic x,y,z:real

goal system: not(
3.*x+2. *y-   z =  1. and
2.*x-2. *y+4.*z = -2. and
-x+ .5*y+   z =  0.
)


Another school-level system of equations

This comes from Yurichev’s 2.2.2, and was apparently found “somewhere on Facebook”.

The following code solves this system. logic circle, square, triangle: int

goal system: not(
circle + circle = 10 and
circle*square + square = 12 and
circle*square - triangle*circle = circle
)


XKCD 287

This comes from Yurichev’s 3.1, inspired by xkcd 287. logic a,b,c,d,e,f:int

axiom positive:
a>=0 and b>=0 and c>=0 and d>=0 and e>=0 and f>=0

goal system: not(
215*a+275*b+335*c+355*d+420*e+580*f=1505

(* Uncomment to find another solution *)
(* and not(a=7 and b=0 and c=0 and d=0 and e=0 and f=0) *)

(* Valid if next line uncommented *)
(* and not(a=1 and b=0 and c=0 and d=2 and e=0 and f=1 *)
)


Art of Problem Solving

This comes from Yurichev’s 3.6, inspired by this problem from the Art of Problem Solving.

The sum of two nonzero real numbers is 4 times their product.
What is the sum of the reciprocals of the two numbers?

logic x,y:real
logic res:real

axiom positive:
x>0. and y>0.

axiom result:
res = 1./x + 1./y

goal g:not(
x+y = 4.*x*y
)


### Other examples

Primality tester

Strangely enough, Alt-Ergo seems to prove that $$57$$, “Grothendieck’s prime”, is not actually prime.

logic a,b,n:int

axiom init: n=57
axiom range: 1<=a<=n and 1<=b<=n

goal is_prime:
a*b = n ->
a=1 or b=1


Sudoku solver 4*4

This solves the following sudoku puzzle. type one_four = One | Two | Three | Four

logic grid: int, int -> one_four

predicate by_row =
forall i:int. 0<=i<4 ->
distinct(grid(i,0),grid(i,1),grid(i,2),grid(i,3))

predicate by_column =
forall j:int. 0<=j<4 ->
distinct(grid(0,j),grid(1,j),grid(2,j),grid(3,j))

predicate by_square =
forall i,j:int. 0<=i<2 -> 0<=j<2 ->
distinct(grid(2*i,2*j),grid(2*i,2*j+1),grid(2*i+1,2*j),grid(2*i+1,2*j+1))

axiom init:
grid(0,0)=Three and grid(0,1)=Four and grid(0,2)=One and
grid(1,1)=Two and
grid(2,2)=Two and
grid(3,1)=One and grid(3,2)=Four and grid(3,3)=Three

goal g: not
(by_row and by_column and by_square)


Sudoku solver 9*9

The following sudoku puzzle has been designed by the Finnish mathematician Arto Inkala, and has been coined “the world’s hardest sudoku” by several newspapers. Using the following code, Alt-Ergo solves it in about 30 000 steps, which is ~ $$2$$ seconds on a cheap personal computer (not with the in-browser version).

type one_nine = One   | Two   | Three
| Four  | Five  | Six
| Seven | Eight | Nine

logic grid: int, int -> one_nine

predicate by_row =
distinct(grid(0,0),grid(0,1),grid(0,2),
grid(0,3),grid(0,4),grid(0,5),
grid(0,6),grid(0,7),grid(0,8)) and
distinct(grid(1,0),grid(1,1),grid(1,2),
grid(1,3),grid(1,4),grid(1,5),
grid(1,6),grid(1,7),grid(1,8)) and
distinct(grid(2,0),grid(2,1),grid(2,2),
grid(2,3),grid(2,4),grid(2,5),
grid(2,6),grid(2,7),grid(2,8)) and
distinct(grid(3,0),grid(3,1),grid(3,2),
grid(3,3),grid(3,4),grid(3,5),
grid(3,6),grid(3,7),grid(3,8)) and
distinct(grid(4,0),grid(4,1),grid(4,2),
grid(4,3),grid(4,4),grid(4,5),
grid(4,6),grid(4,7),grid(4,8)) and
distinct(grid(5,0),grid(5,1),grid(5,2),
grid(5,3),grid(5,4),grid(5,5),
grid(5,6),grid(5,7),grid(5,8)) and
distinct(grid(6,0),grid(6,1),grid(6,2),
grid(6,3),grid(6,4),grid(6,5),
grid(6,6),grid(6,7),grid(6,8)) and
distinct(grid(7,0),grid(7,1),grid(7,2),
grid(7,3),grid(7,4),grid(7,5),
grid(7,6),grid(7,7),grid(7,8)) and
distinct(grid(8,0),grid(8,1),grid(8,2),
grid(8,3),grid(8,4),grid(8,5),
grid(8,6),grid(8,7),grid(8,8))

predicate by_column =
distinct(grid(0,0),grid(1,0),grid(2,0),
grid(3,0),grid(4,0),grid(5,0),
grid(6,0),grid(7,0),grid(8,0)) and
distinct(grid(0,1),grid(1,1),grid(2,1),
grid(3,1),grid(4,1),grid(5,1),
grid(6,1),grid(7,1),grid(8,1)) and
distinct(grid(0,2),grid(1,2),grid(2,2),
grid(3,2),grid(4,2),grid(5,2),
grid(6,2),grid(7,2),grid(8,2)) and
distinct(grid(0,3),grid(1,3),grid(2,3),
grid(3,3),grid(4,3),grid(5,3),
grid(6,3),grid(7,3),grid(8,3)) and
distinct(grid(0,4),grid(1,4),grid(2,4),
grid(3,4),grid(4,4),grid(5,4),
grid(6,4),grid(7,4),grid(8,4)) and
distinct(grid(0,5),grid(1,5),grid(2,5),
grid(3,5),grid(4,5),grid(5,5),
grid(6,5),grid(7,5),grid(8,5)) and
distinct(grid(0,6),grid(1,6),grid(2,6),
grid(3,6),grid(4,6),grid(5,6),
grid(6,6),grid(7,6),grid(8,6)) and
distinct(grid(0,7),grid(1,7),grid(2,7),
grid(3,7),grid(4,7),grid(5,7),
grid(6,7),grid(7,7),grid(8,7)) and
distinct(grid(0,8),grid(1,8),grid(2,8),
grid(3,8),grid(4,8),grid(5,8),
grid(6,8),grid(7,8),grid(8,8))

predicate by_square =
distinct(grid(0,0),grid(0,1),grid(0,2),
grid(1,0),grid(1,1),grid(1,2),
grid(2,0),grid(2,1),grid(2,2)) and
distinct(grid(0,3),grid(0,4),grid(0,5),
grid(1,3),grid(1,4),grid(1,5),
grid(2,3),grid(2,4),grid(2,5)) and
distinct(grid(0,6),grid(0,7),grid(0,8),
grid(1,6),grid(1,7),grid(1,8),
grid(2,6),grid(2,7),grid(2,8)) and
distinct(grid(3,0),grid(3,1),grid(3,2),
grid(4,0),grid(4,1),grid(4,2),
grid(5,0),grid(5,1),grid(5,2)) and
distinct(grid(3,3),grid(3,4),grid(3,5),
grid(4,3),grid(4,4),grid(4,5),
grid(5,3),grid(5,4),grid(5,5)) and
distinct(grid(3,6),grid(3,7),grid(3,8),
grid(4,6),grid(4,7),grid(4,8),
grid(5,6),grid(5,7),grid(5,8)) and
distinct(grid(6,0),grid(6,1),grid(6,2),
grid(7,0),grid(7,1),grid(7,2),
grid(8,0),grid(8,1),grid(8,2)) and
distinct(grid(6,3),grid(6,4),grid(6,5),
grid(7,3),grid(7,4),grid(7,5),
grid(8,3),grid(8,4),grid(8,5)) and
distinct(grid(6,6),grid(6,7),grid(6,8),
grid(7,6),grid(7,7),grid(7,8),
grid(8,6),grid(8,7),grid(8,8))

axiom init:
grid(0,0)=Eight and grid(1,2)=Three and grid(2,1)=Seven and
grid(1,3)=Six   and grid(2,4)=Nine  and
grid(2,6)=Two   and
grid(3,2)=Five  and
grid(3,5)=Seven and grid(4,4)=Four  and grid(4,5)=Five  and grid(5,3)=One and
grid(4,6)=Seven and grid(5,7)=Three and
grid(6,2)=One   and grid(7,2)=Eight and grid(8,1)=Nine  and
grid(7,3)=Five  and
grid(6,7)=Six   and grid(6,8)=Eight and grid(7,7)=One   and grid(8,6)=Four

goal g: not
(by_row and by_column and by_square)


The output provided by Alt-Ergo is

( (by_row FT:[by_row]) (by_column FT:[by_row]) (by_square FT:[by_row])

((grid 8 6) X5(Sum):[Four])
((grid 6 0) X5(Sum):[Four])
((grid 7 5) X5(Sum):[Four])
((grid 3 7) X5(Sum):[Four])
((grid 1 8) X5(Sum):[Four])
((grid 2 3) X5(Sum):[Four])
((grid 5 1) X5(Sum):[Four])
((grid 4 4) X5(Sum):[Four])
((grid 0 2) X5(Sum):[Four])
((grid 8 4) X5(Sum):[One])
((grid 6 2) X5(Sum):[One])
((grid 7 7) X5(Sum):[One])
((grid 3 8) X5(Sum):[One])
((grid 1 6) X5(Sum):[One])
((grid 2 5) X5(Sum):[One])
((grid 5 3) X5(Sum):[One])
((grid 4 0) X5(Sum):[One])
((grid 0 1) X5(Sum):[One])
((grid 8 3) X5(Sum):[Eight])
((grid 6 8) X5(Sum):[Eight])
((grid 7 2) X5(Sum):[Eight])
((grid 3 6) X5(Sum):[Eight])
((grid 1 5) X5(Sum):[Eight])
((grid 2 7) X5(Sum):[Eight])
((grid 5 4) X5(Sum):[Eight])
((grid 4 1) X5(Sum):[Eight])
((grid 0 0) X5(Sum):[Eight])
((grid 8 5) X5(Sum):[Six])
((grid 6 7) X5(Sum):[Six])
((grid 7 1) X5(Sum):[Six])
((grid 3 4) X5(Sum):[Six])
((grid 1 3) X5(Sum):[Six])
((grid 2 2) X5(Sum):[Six])
((grid 5 0) X5(Sum):[Six])
((grid 4 8) X5(Sum):[Six])
((grid 0 6) X5(Sum):[Six])
((grid 8 7) X5(Sum):[Five])
((grid 6 1) X5(Sum):[Five])
((grid 7 3) X5(Sum):[Five])
((grid 3 2) X5(Sum):[Five])
((grid 1 4) X5(Sum):[Five])
((grid 2 0) X5(Sum):[Five])
((grid 5 6) X5(Sum):[Five])
((grid 4 5) X5(Sum):[Five])
((grid 0 8) X5(Sum):[Five])
((grid 8 1) X5(Sum):[Nine])
((grid 6 5) X5(Sum):[Nine])
((grid 7 6) X5(Sum):[Nine])
((grid 3 3) X5(Sum):[Nine])
((grid 1 0) X5(Sum):[Nine])
((grid 2 4) X5(Sum):[Nine])
((grid 5 8) X5(Sum):[Nine])
((grid 4 2) X5(Sum):[Nine])
((grid 0 7) X5(Sum):[Nine])
((grid 8 0) X5(Sum):[Three])
((grid 6 6) X5(Sum):[Three])
((grid 7 4) X5(Sum):[Three])
((grid 3 1) X5(Sum):[Three])
((grid 1 2) X5(Sum):[Three])
((grid 2 8) X5(Sum):[Three])
((grid 5 7) X5(Sum):[Three])
((grid 4 3) X5(Sum):[Three])
((grid 0 5) X5(Sum):[Three])
((grid 8 8) X5(Sum):[Seven])
((grid 6 4) X5(Sum):[Seven])
((grid 7 0) X5(Sum):[Seven])
((grid 3 5) X5(Sum):[Seven])
((grid 1 7) X5(Sum):[Seven])
((grid 2 1) X5(Sum):[Seven])
((grid 5 2) X5(Sum):[Seven])
((grid 4 6) X5(Sum):[Seven])
((grid 0 3) X5(Sum):[Seven])
((grid 8 2) X5(Sum):[Two])
((grid 6 3) X5(Sum):[Two])
((grid 7 8) X5(Sum):[Two])
((grid 3 0) X5(Sum):[Two])
((grid 1 1) X5(Sum):[Two])
((grid 2 6) X5(Sum):[Two])
((grid 5 5) X5(Sum):[Two])
((grid 4 7) X5(Sum):[Two])
((grid 0 4) X5(Sum):[Two])

)
File "", line 105, characters 9-53:
I don't know (1.9514) (30079 steps) (goal g)