2019-04-28

SAT solving with reverse division

It seems like when I’m trying to solve magic squares with bit blasting + SAT solvers running division in reverse comes up with solutions faster than doing normal multiplication.

Context

The above sentence may not make much sense without at least some context.

I’ve been trying to solve some magic square problems with SAT solvers. It’s an unsolved mathematical problem involving finding integer assignments on a 3x3 square.

I made a software that turns integer problems into SAT problems to try and see if I could solve any of them.

To implement operations like addition, multiplication or division and cast that problem into SAT world, you implement the boolean circuit that will perform the operation.

My multiplication boolean circuit is problematic. The school-board style multiplication results in a circuit that is size O(N^2) to the number of bits. As a result, I’ve had a lot of trouble making any problem solve fast on a SAT solver that involves many multiplications. Magic square problem has a few multiplications so getting multiplication work fast in SAT world would go a long way into being able to check larger classes of possible solutions to magic square problem.

Division circuit in reverse

Something you can do in SAT but no so much in real life is running circuits in reverse.

In pseudo-code, you could say I originally had something liket his:

ASSERT: 'a'  is an integer between 0-8191
ASSERT: 'a2' is an integer between 0-67108864
ASSERT: 'a2' is 'a * a'
...

In other words, I specify that I have two integers and the other integer is the square of the first one. This is bit-blasted to a SAT problem.

This is what I found seems to be a bit faster.

ASSERT: 'a'  is an integer between 0-8191
ASSERT: 'a2' is an integer between 0-67108864
ASSERT: 'a'  is 'a2 / a'
ASSERT: 0    is 'a2 % a'

We assert that ‘a’ is the result of a division with 0 remainder instead of doing multiplication.

Why is better?

I have no idea why division circuit ended up being faster. It could be due to bad implementation of my multiplication circuit generation. Or it might only work for magic square problems.

As division algorithm I simply used long division method for binary and made it into a circuit. The multiplication algorithm was school-board type boolean circuit.

Takeaway

If you are solving mathematical problems with SAT, then the circuits you are using to cast that problem into SAT can have substantial effect on how quickly we will find solutions.