SAT Part 3 — Reducing ILP to SAT

November 13, 2021July 20, 2021 ~ afish ~ 1 Comment

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

SAT Part 2 — Arithmetic

November 6, 2021July 19, 2021 ~ afish ~ 1 Comment

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

SAT Part 1 — Boolean logic

October 30, 2021November 13, 2021 ~ afish ~ 2 Comments

This is the first part of the SAT series. For your convenience you can find other parts using the links below: SAT Part 1 — Boolean logic SAT Part 2 — Arithmetic Part 3 — Reducing ILP to SAT Today we are going to implement some Boolean logic in SAT. Equal and not equal Let’s … Continue reading SAT Part 1 — Boolean logic