SC Chapter 7 Linear Real Arithmetic

Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 7 Linear Real Arithmetic

0.0 (0)

R. B.

Lernen

R. B.

Über diese Lernkartei

This flashcard set covers advanced university-level topics in computer science, focusing on linear real arithmetic and related algorithms. It delves into the omega test, branch and bound methods, and the simplex algorithm, exploring their definitions, phases, constraints, and optimizations. The set also discusses variable elimination, bounds, and the historical context of linear real arithmetic. Ideal for students and researchers, this flashcard set provides a comprehensive overview of solving linear inequality and equality problems, making it invaluable for those studying algorithmic problem-solving and optimization techniques.

Karten

Lernende

Sprache

Englisch

Kategorie

Informatik

Stufe

Universität

Erstellt / Aktualisiert

18.02.2017 / 28.02.2017

Ähnliche Karteien

What is the idea of branch in the branch and bound method?

Branch means split the search space

What is the idea of bound in the branch and bound method?

Bound means exclude unsatisfiable sub-spaces

What is the definition of the branch and bound method? [6]

Input is an integer linear system S

Output is SAT or UNSAT

1. Set res to LP(relaxed(S))

2. If res is UNSAT return UNSAT

3. Else if res is integral return SAT

4. Choose v assigned to non-integral value r

5. Perform res’=branch-and-bound(S with v\leq OR \geq round_down(r))

6. Return res’

What is the problem of the branch and bound method?

Incomplete due to real but no integer solutions

What are the reactions on the incomplete problem for the branch and bound method? [2]

1. Small-world property

2. Mixed integer linear programming

What is the definition of the small-world property for the branch and bound method?

If solution exists then One exists within computable finite bound

What is the definition of mixed integer linear programming for the branch and bound method?

Mix integer and real values

What are possible optimizations for the branch and bound method? [2]

1. Remove redundant constraints

2. Tighten bounds

What is the definition of tighten bounds for the branch and bound method? [2]

1. If a_k>0 → x_k \leq (b-Sum_i!=k a_i*l_i)/a_k

2. If a_k<0 → x_k \geq (b-Sum_i!=k a_i*u_i)/a_k

What is the idea of the omega test?

Decide satisfiability for conjunctions of linear constraints Sum ai*xi \geq b over integers

What are the characteristics of the omega test? [2]

1. From compiler optimization

2. Extension of Fourier Motzkin

What are the three phases of the omega test? [3]

1. Real 2. dark and 3. grey shadow

What is the definition of the real shadow phase of the omega test? [2]

1. Real solution with integer value in given dimension

2. If no solution return UNSAT

How is a solution computed in the real shadow phase of the omega test? [2]

1. For variable z compute with b,c > 0 beta \leq b*z and c*z \leq gamma → c*beta \leq c*b*z \leq b*gamma

2. Add new constraint for variable z

How are new constraints added for variable z in the real shadow phase of the omega test? [2]

1. c*beta \leq b*gamma // If not last variable

2. round_up(beta/b) \leq round_down(gamma/c) // If last variable

What is the definition of the dark shadow phase of the omega test? [2]

1. Check sufficient condition for integer solution

2. If sufficient return SAT

How do we check the sufficient condition in the dark shadow phase of the omega test? [3]

1. Try to prove existence of integer between beta/b and gamma/c

2. Condition is b*gamma-c*beta \geq (c-1)*(b-1)

3. In case of c=b=1 we talk about an exact projection

What is the problem of the sufficient condition in the dark shadow phase of the omega test?

Might not detect possible integer solutions

What is the definition of the grey shadow phase of the omega test? [2]

1. Further checks for integer solution not sufficient

2. If passing return SAT else UNSAT

How do we check in the grey shadow phase of the omega test? [3]

1. Search in real shadow without dark shadow

2. Test all values (cb-c-b)/c + beta \geq b*z \geq beta

3. Optimization with test for all b*z \geq beta, b*z = beta + i : for 0 \leq i \leq (cb-c-b)/c

What are the components of the syntax of linear real arithmetics? [3]

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

1. Terms t 2. constraints c and 3. formulas phi

What are the members of a term t of linear real arithmetics? [4]

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

0, 1, variable x, t + t

What is the member of a constraint c of linear real arithmetics?

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

t < t

What are the members of a formula phi of linear real arithmetics? [4]

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

c , \neg phi, phi \land phi, \exists x. phi

What is the input for the decision procedure of linear real arithmetics?

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

For sets of m constraints out of equations and inequations and n variables

How does the i-th constraint looks like for linear real arithmetics?

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

Sum_k a_ik*x_k = b_i

How can we specify the variable x_j for linear real arithmetics? [2]

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

1. x_j = b_i/a_ij – Sum_{not_j} a_ik/a_ij *x_k := beta_j

2. Substitution of x_j leads to equi-satisfiable problem in n-1 variables

How can we transform the set of constraints for linear real arithmetics?

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

Transform \Land_i Sum_j a_ij*x_j <= b_i → A*x <= b with A m x n

What happened 1826 regarding linear real arithmetics?

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

Fourier with earliest method for solving linear inequality systems

What happened 1936 regarding linear real arithmetics?

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

Motzkin with re-discovering Fourier’s solution

What is the idea of variable elimination for linear real arithmetics?

Pick variable and put requirements on lower and upper bounds

What is the definition of an upper bound for x_n for linear real arithmetics?

If a_in > 0 beta_i is upper bound beta_u on x_n

What is the definition of an lower bound for x_n for linear real arithmetics?

If a_in < 0 : beta_i is lower bound beta_l on x_n

What are the two possibilities for variable elimination for linear real arithmetics? [2]

1. Remove unbounded variables and constraints that use them

2. Add constraint beta_l <= beta_u for both ways bounded variables

What is the worst case complexity for variable elimination for linear real arithmetics?

From m → m²ⁿ

What is the simple algorithm to solve a linear equality problem?

Gaussian algorithm turning A of Ax=b into upper-triangular form and solve backwards

What is the advanced algorithm to solve a linear inequality problem?

Simplex algorithm

What are the characteristics of simplex algorithm? [3]

1. Originally for solving optimization problems

2. Applicable for feasibility/satisfiability problems

3. Solve the satisfiability problem fast

What is the input for the general simplex algorithm?

Input Ax<=b

How does converting into general form in simplex algorithm works? [2]

1. A(x,s)=0 and for all s_i upper and lower bound

2. Replace Sum_i a_i*x_i |><| b_j with Sum_i a_i*x_i-s_j=0

1 / 50

Lernkarten

What are the characteristics of the omega test? [2]

1. From compiler optimization

2. Extension of Fourier Motzkin

What are the three phases of the omega test? [3]

1. Real 2. dark and 3. grey shadow

What is the definition of the real shadow phase of the omega test? [2]

1. Real solution with integer value in given dimension

2. If no solution return UNSAT

How is a solution computed in the real shadow phase of the omega test? [2]

1. For variable z compute with b,c > 0 beta \leq b*z and c*z \leq gamma → c*beta \leq c*b*z \leq b*gamma

2. Add new constraint for variable z

How are new constraints added for variable z in the real shadow phase of the omega test? [2]

1. c*beta \leq b*gamma // If not last variable

2. round_up(beta/b) \leq round_down(gamma/c) // If last variable

What is the definition of the dark shadow phase of the omega test? [2]

1. Check sufficient condition for integer solution

2. If sufficient return SAT

How do we check the sufficient condition in the dark shadow phase of the omega test? [3]

1. Try to prove existence of integer between beta/b and gamma/c

2. Condition is b*gamma-c*beta \geq (c-1)*(b-1)

3. In case of c=b=1 we talk about an exact projection

What is the problem of the sufficient condition in the dark shadow phase of the omega test?

Might not detect possible integer solutions

What is the definition of the grey shadow phase of the omega test? [2]

1. Further checks for integer solution not sufficient

2. If passing return SAT else UNSAT

How do we check in the grey shadow phase of the omega test? [3]

1. Search in real shadow without dark shadow

2. Test all values (cb-c-b)/c + beta \geq b*z \geq beta

3. Optimization with test for all b*z \geq beta, b*z = beta + i : for 0 \leq i \leq (cb-c-b)/c

Lernen

SC Chapter 7 Linear Real Arithmetic

Lernkarteien erstellen oder kopieren

Lernkarten

Bitte melde dich an

Google

Apple ID

Microsoft

Switch edu-ID

Edulog

Google

Apple ID

Microsoft

Switch edu-ID

Edulog