Upgrade to Pro — share decks privately, control downloads, hide ads and more …

Constraint Programming

almo
March 04, 2021

Constraint Programming

Introduction to Constraint Programming using Google OR-Tools with Kotlin, presenting a brief introduction to complexity, motivational description of the linear programming required by casual inference about imperfect experiments and some coding examples of OR-Tools with Kotlin. Final examples of the application of these techniques to formal verification of software using Z3 and TLA+ with Picat.

almo

March 04, 2021
Tweet

More Decks by almo

Other Decks in Programming

Transcript

  1. A few words about me... Andres-Leonardo Martinez-Ortiz a.k.a almo is

    a member of the Google Engineering team, leading Google Developer Relations worldwide. Based in Zurich, he drives the success of Google's developer products and the Open Web by creating a thriving ecosystem of developers. Nurturing developers experts and partners in large companies, startups, universities and enterprises, almo fosters open standards and Google technologies. almo is also a member of IEEE, ACM, Linux Foundation and Computer Society. @davilagrau almo.dev almo
  2. Exponential Time Polynomial Space Polynomial Space Polynomial Hierarchy Nondeterministic Polynomial

    Time Polynomial time Bounded-error Quantum Polynomial time Complexity Zoo • Does P = NP? • if P = NP, then P = PH. • Every problem in P, NP and PH is in PSPACE. • BQP is contained in PSPACE and that BQP contains P. • There are problems that are in NP and not BQP and vice versa. • We know how to separate EXP and P. Polynomial time Bounded-error Probabilistic Polynomial time And there are also NP, NP-Hard, NP-Complete...
  3. Imperfect Experiment Inferenc Causal Inference and do-Calculus Imperfect experiments are

    those that deviate from ideal protocol of randomized control Treatment Assigned Treatment Received Observed Response Latent Factors Z X Y U P(y,x,z,u) = P(y|x,u) P(x|z,u) P(z) P(u) ? P(y | do(x)) = ⅀P(y | x,u ) P(u ) ACE (X→Y) = P(y 1 | do(x 1 )) - P(y 0 | do(x 0 ))
  4. Constraint Satisfaction Problems Definition 1. A set of variables {X

    1 ,..., X n } 2. A set of domains {D 1 ,..., D n } 3. A set of constraints defining the restriction of the values The state space of a CSP is defined by the assignments to some or all the variables i.e. {X 1 =v 1 ,..., X n =v n } A solution is a consistent complete assignment i.e. all the variables have value and these values doesn’t violate any constraint. IMPORTANT: the structure of the state space and use general-purpose heuristics allow to eliminate a big chunk of the search space. Icons made by Freepik from www.flaticon.com
  5. NP = P ?... sometimes P = NP? • Special

    case: polynomial time for fixed tractable parameters • Random algorithms • Approximation algorithms: close to optimal • Average Algorithms: Avoiding the worst case
  6. Solvers • Constraint Programming ◦ Cryptarithmetic Puzzles ◦ N-Queens ◦

    Job scheduling • Propositional Satisfiability Problem ◦ Planning in robotics ◦ Automatic Theorem Proving ◦ Software Verification • Linear optimization ◦ Optimal Manufacturing ◦ Planning xn + yn = zn SEND + MORE MONEY
  7. Dealing with the complexity • Problem modelling ◦ CP ◦

    SAT ◦ MIP • Representation ◦ OR-Tools ◦ PICAT ◦ MiniZinc • Solver ◦ PICAT ◦ GLOP ◦ Z3 ◦ CP-SAT ◦ MiniZinc N CP(s) SAT(s) MIP(s) 8 0.00 0.08 0.35 10 0.00 0.12 0.50 12 0.00 0.16 5.17 20 0.00 0.80 1557.3 50 0.00 8.74 - 100 0.02 48.10 - 200 0.56 105.61 - 400 4.86 - - 1000 5.02 - - N-Queens Problem
  8. OR-Tools • Open source software suite • Language ◦ C++

    • Wrappers ◦ Python ◦ C# ◦ Java ◦ Kotlin • Tough problems in ◦ Vehicle routing ◦ Flows ◦ Integer and linear programming ◦ Constraint programming • Multi Solvers: ◦ Gurobi ◦ CPLEX ◦ SCIP, ◦ GLPK ◦ GLOP ◦ CP-SAT Linear Scalability Apache 2.0
  9. Applications Vehicle routing: Find optimal routes for vehicle fleets that

    pick up and deliver packages given constraints (e.g., "this truck can't hold more than 20,000 pounds" or "all deliveries must be made within a two-hour window"). Scheduling: Find the optimal schedule for a complex set of tasks, some of which need to be performed before others, on a fixed set of machines, or other resources. Bin packing: Pack as many objects of various sizes as possible into a fixed number of bins with maximum capacities. Photo by Christian Chen on Unsplash Photo by Ivan Diaz on Unsplash
  10. Linear Optimization Example outcome: Number of variables = 2 Number

    of constraints = 3 Solution: Objective value = 33.99 x = 5.99 y = 3.99 Advanced usage: Problem solved in 5 milliseconds Problem solved in 2 iterations
  11. Assignment Example outcome: Total cost: 265.0 W 0 assigned to

    task 3. Cost = 70.0 W 1 assigned to task 2. Cost = 55.0 W 2 assigned to task 1. Cost = 95.0 W 3 assigned to task 0. Cost = 45.0 objective.setMinimization() + Using Arrays to Define a Model + 0 1 2 3 0 1 2 3 (090.0, 80.0, 75.0, 70.0) (035.0, 85.0, 55.0, 65.0) (125.0, 95.0, 90.0, 95.0) (045.0, 110.0, 95.0, 115.0) (050.0, 100.0, 90.0, 100.0) Tasks Workers
  12. Routing Important facts: • Vehicle routing problems are inherently intractable

    • There are specialized solvers for TSP such as Concorde • It is a very active research field yet: • Traveling salesman problem, the classic routing problem in which there is just one vehicle. • Vehicle routing problem, a generalisation of the TSP with multiple vehicles. • VRP with capacity constraints, in which vehicles have maximum capacities for the items they can carry. • VRP with time windows, where the vehicles must visit the locations in specified time intervals. • VRP with resource constraints, such as space or personnel to load and unload vehicles at the depot (the starting point for the routes). • VRP with dropped visits, where the vehicles aren't required to visit all locations, but must pay a penalty for each visit that is dropped. Vehicle routing problems are inherently intractable
  13. Scheduling Problems • Schedule employees in multiple shifts, subject to

    a complex set of constraints and staffing requirements. • Scheduling multiple jobs, processed on several machines Validation with TLA+ • For instance Missionaries and Cannibals Further support with Picat • Dynamic Programming • Robotics By Carloseow at English Wikipedia, CC BY 3.0, https://commons.wikimedia.org/w/index.php?curid=35846111
  14. Software Verification and Analysis Using Z3 • Modeling and analysis

    of an algorithm documented in an old version of the QUIC Transport protocol IETF draft. • Modeling of specific finite field arithmetic operations for elliptic curve cryptography, with integers represented using a uniform saturated limb schedule (four limbs of 64 bits), to prove equivalence with arbitrary-precision arithmetic, and for test cases generation. http://bit.ly/3b7lKG9
  15. Verifying TLA+ Models TLA+ is a high-level language for modeling

    programs and systems--especially concurrent and distributed ones. It's based on the idea that the best way to describe things precisely is with simple mathematics.