I'm interested in what happens when using the Simplex algorithm on Difference logic, inspired by problem 5.4 in Kroening and Strichman's Decision Procedures.

Clearly, in this case, all constraints of the program will have only two variables, with coefficients 1 and -1, so the matrix will be of a special type. What happens when running the Simplex algorithm on such a program? Is it easier to solve?

Thanks for any help!

  • $\begingroup$ Could you sketch in a few words what you mean by difference logic for readers without access to Kroening & Strichman? $\endgroup$ Sep 23, 2023 at 14:01


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.