This is the third part of the SAT series. For your convenience you can find other parts in the table of contents in Part 1 — Boolean logic Today we are going to reduce ILP to SAT. Introduction Depending on the solver, typical ILP supports the following operations: Adding two variables Negating variable Subtracting variables … Continue reading SAT Part 3 — Reducing ILP to SAT

This is the second part of the SAT series. For your convenience you can find other parts in the table of contents in Part 1 — Boolean logic Today we’re going to implement some basic arithmetic in SAT. Addition We assume numbers are represented using U2 scheme. All we need to do is to implement … Continue reading SAT Part 2 — Arithmetic