Z3 timed out? Try Gurobi

  • AND: y = x₁∧x₂∧…∧xₙ. Constraint: 0 ≤ Σxᵢ - ny ≤ n-1
  • OR: y = x₁∨x₂∨…∨xₙ. Constraint: 0 ≤ ny - Σxᵢ ≤ n-1
  • NOT: y= ¬ x. Constraint: y = 1 - x

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store