c2b_default

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

50
0.0 (0)
R. B.
Study
R. B.
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.
Flashcards
50
Students
1
Language
English
Category
Computer Science
Level
University
Created / Updated
18.02.2017 / 28.02.2017
  • 1  / 50

Flashcards

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

Study