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

This comes from Yurichev’s 2.2.1, copy pasted from this wikipedia page.

The following code solves this simple system of equations.

../_images/equation_1.svg
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.

../_images/equation_2.png
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.

../_images/np_complete.png
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.

../_images/sudoku4.png
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.

../_images/sudoku.jpg

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)