Working with integers to solve math puzzles

models
1

I’ve been trying to see if I can model the following puzzle, which does have at least one solution:

Find the coefficients a, b, and c for this equation such that x = 1, 2, 3, 4 results in a perfect square, but x = 5 is not perfect

f(x) = ax^2 + bx + c

There is a solution at a=46, b=-166, c=184 but I cannot get this model to find it

Is there anything obviously wrong, or is this simply not the type of problem for which Alloy is well-suited? (i.e., I have noted the section on integers in “Software Abstractions”, in which it says Alloy is not suitable for numerical problems)

abstract sig Coefficient {
	value: Int
}

one sig A extends Coefficient {}
one sig B extends Coefficient {}
one sig C extends Coefficient {}

fun square (x: Int): Int {
	mul[x, x]
}

fun equation (a: A, b: B, c: C, x: Int): Int {
	plus[plus[mul[a.value, square[x]], mul[b.value, x]], c.value]
}

pred isPerfect [n: Int] {
	one x: {i: Int} | square[x] = n
}

pred solver {
	all a: A, b: B, c: C, x: {i: Int | i > 0 and i < 5} |
		isPerfect[equation[a, b, c, x]] 
	and not isPerfect[equation[a, b, c, {5}]]
}

run solver
2

Hey. From https://alloy.readthedocs.io/en/latest/language/sets-and-relations.html#integers:

By default, Alloy uses models with 4-bit signed integers: all integers between -8 and 7.

The easiest way to make it larger is by doing, e.g., run solver for 10 Int.

Then the following works, when executed with run solver for 11 Int, but not with run solver for 10 Int (please notice the commented out line that nudges it in the right direction):

open util/integer

fun square (x: Int): Int {
	mul[x, x]
}

fun add3(i, j, k: Int): Int {
	{ r: Int | int r = add[add[i, j], k] }
}

fun equation (a, b, c, x: Int) : Int {
	{
	  f: Int |
		int f = add3[
				mul[a, square[x]],
				mul[b, x],
				c
				]
	}
}

pred isPerfect[n: Int] {
    one sqrt: Int | (sqrt > 0) and n = square[sqrt]
}

pred solver {
	some a, b, c: Int |
		// int a = 46 and int b = -166 and
		isPerfect[equation[a, b, c, 1]] and
		isPerfect[equation[a, b, c, 2]] and
		isPerfect[equation[a, b, c, 3]] and
		isPerfect[equation[a, b, c, 4]] and
		not isPerfect[equation[a, b, c, 5]]
		
}

run solver for 6 Int
run solver for 10 Int
run solver for 11 Int

But when it’s executed with run solver for 6 Int, it finds bad examples, like a=1, b=2, c=1, because it’s still a perfect square when x=5, probably because of integer overflow.

3

Oh, I see, thank you for pointing that out!

Using for 11 Int with this small change to my original definition also gives me a valid solution (a=8, b=-40, c=57):

pred isPerfect [n: Int] {
	one x: {i: Int | i > 0} | square[x] = n
}

which I suppose is syntactically equivalent to having the non-negative condition outside the type, as you have it:

pred isPerfect[n: Int] {
    one sqrt: Int | (sqrt > 0) and n = square[sqrt]
}

Thank you, too for the bit of suggested refactor to the equation, by having add3 as a helper function (I’m still a n00b, so it didn’t occur to me to try it that way).

4

Well, the problem is shown above in a smaller scope: it mostly works, but sometimes it generates wrong answers. I’m not an expert, I’m not sure why. As far I understand, integers in Alloy are not real integers, they are elements of a set, and we describe relationships between them. This is not very efficient, and it causes the highlighted issue.