SC Chapter 7 Linear Real Arithmetic
Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 7 Linear Real Arithmetic
Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 7 Linear Real Arithmetic
-
- 1 / 50
-
Lernkarten
What are the components of the syntax of linear real arithmetics? [3]
1. Terms t 2. constraints c and 3. formulas phi
What are the members of a term t of linear real arithmetics? [4]
0, 1, variable x, t + t
What is the member of a constraint c of linear real arithmetics?
t < t
What are the members of a formula phi of linear real arithmetics? [4]
c , \neg phi, phi \land phi, \exists x. phi
What is the input for the decision procedure of linear real arithmetics?
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?
Sumk aik*xk = bi
How can we specify the variable xj for linear real arithmetics? [2]
1. xj = bi/aij – Sumnot_j aik/aij *xk := betaj
2. Substitution of xj leads to equi-satisfiable problem in n-1 variables
How can we transform the set of constraints for linear real arithmetics?
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?
Fourier with earliest method for solving linear inequality systems
What happened 1936 regarding linear real arithmetics?
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 xn for linear real arithmetics?
If ain > 0 betai is upper bound betau on xn
What is the definition of an lower bound for xn for linear real arithmetics?
If ain < 0 : betai is lower bound betal on xn
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 → m2n
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 si upper and lower bound
2. Replace Sumi ai*xi |><| bj with Sumi ai*xi-sj=0
What are the components of the general form of the simplex algorithm? [4]
1. xi are called non-basic variables N
2. sj are called additional, basic or dependent variables B
3. A is a m x (n+m) matrix with A-I with tableau A
4. Assignment a to all variables
What are the characteristics of the assignment a of the general form of the simplex algorithm? [2]
1. Initially a(xi)=0
2. Required is Ax=0 // All non-basic variables satisfy bounds, but not necessary the basic variables
What holds for the satisfiability of the general form of the simplex algorithm? [2]
1. If all basic variables satisfy bounds return satisfiable
2. Else pivoting
How does pivoting of the general form of the simplex algorithm works? [5]
1. Find basic variable xi violating bounds
2. Find non-basic suitable variable xj
3. If no suitable variable is found return unsatisfiable
4. Swap xi and xj
5. Update
What are the constraints for a suitable variable in the general form of the simplex algorithm works? [2]
1. If aij>0 and a(xj)<uj
2. Else if aij<0 and a(xj)>lj
What has to be updated while pivoting in the general form of the simplex algorithm? [5]
1. I-th row accordingly with ai1→-ai1/aij,… ,aij→1/aij,… ,ain→-ain/aij
2. All other rows
3. a(xj) increasing by t=(li-a(xi))/aij //xj becomes a basic variable
4. a(xi) accordingly
5. a for all basic variables
What holds for cycles in the general form of the simplex algorithm? [2]
1. Local not possible
2. Bigger avoided with Bland’s rule
What is the definition of the Bland’s rule? [2]
1. Total order on variables
2. Choose first basic and non-basic variable for pivoting
What is the geometrical interpretation of the general form of the simplex algorithm?
Linear inequality constraints define convex polyhedron
What is the definition of a relaxed integer linear system?
Relaxed system relaxed(S) is a integer linear system without integrality requirement
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 ak>0 → xk \leq (b-Sumi!=k ai*li)/ak
2. If ak<0 → xk \geq (b-Sumi!=k ai*ui)/ak
What is the idea of the omega test?
Decide satisfiability for conjunctions of linear constraints Sum ai*xi \geq b over integers
