SC Chapter 8 Quantifier-free Non-linear Real Arithmetic

Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 8 Quantifier-free Non-linear Real Arithmetic

0.0 (0)

R. B.

Lernen

R. B.

Über diese Lernkartei

This flashcard set covers advanced topics in quantifier-free non-linear real arithmetic at the university level. It delves into concepts like polynomial constraints, propagation, and the Cauchy bound, focusing on the characteristics and properties of polynomials, roots, and regions. The set also explores methods like the Sturm sequence, virtual substitution, and the Newton method, which are crucial for solving and understanding non-linear arithmetic problems. This flashcard set is particularly beneficial for university students and researchers in computer science who need to grasp the intricacies of real arithmetic and its applications in algorithmic problem-solving.

Karten

Lernende

Sprache

Englisch

Kategorie

Informatik

Stufe

Universität

Erstellt / Aktualisiert

18.02.2017 / 28.02.2017

Ähnliche Karteien

When is a formula phi linear?

[definition.CAD.QFNRA]

If every p has deg(p)<2

When is a formula phi non-linear?

[definition.CAD.QFNRA]

If one p has deg(p)>1

What is the solution space?

[definition.CAD.QFNRA]

Possible assignment for variables

What is the sign of a polynomial for input a?

[definition.CAD.QFNRA]

One element of {-1,0,1}

What are the characteristics?

[region.definition.CAD.QFNRA, 4]

1. Non-empty

2. Connected

3. Subset of Rⁿ

4. Sign-invariant if all polynomials have same sign

What does connected means?

[region.definition.CAD.QFNRA]

If for all A,B holds (R cut A) cup (R cut B) is R

What are the characteristics?

[roots.definition.CAD.QFNRA, 4]

1. Amount lies between 0 and deg(p)

2. Sign changes only here

3. sigma(e) is number of sign changes in a sequences

4. For each a<b #distinctRealRoots of p is sigma(a)-sigma(b)

What are the types?

[roots.definition.CAD.QFNRA, 4]

1. Rational

2. Irrational

3. Not representable by radicals

4. Interval representation with one root in (l,r)

What is the idea?

[CAD.QFNRA, 3]

1. Assume finite set P of polynomials with sign condition for each p

2. Produce decompositions of Rⁿ into a finite number of P-sign-invariant regions (So-called CAD cells)

3. Test sample point from each CAD cells

What are the outcomes of testing the sample point?

[idea.CAD.QFNRA]

If all sign conditions satisfied for #point>0 return SAT else return UNSAT

What is the cauchy bound C?

[for R.CAD.QFNRA, 2]

1. C = 1+max(|a_i|/|a_k|) >= real root |e| with a_k most-left coefficient

2. (-C,C) is interval containing all real roots

What is the idea?

[sturm seq.for R.CAD.QFNRA, 2]

1. Counts real roots in open interval

2. Finites sequence of polynomials of decreasing degree

How to compute?

[sturm seq.for R.CAD.QFNRA, 3]

1. p₀=p

2. p₁=p’

3. p_i=-rem(p_i-2,p_i-1) with rem is remainder of polynomial division of p₀ by p₁

What are the properties?

[sturm seq.for R.CAD.QFNRA, 4]

1. If p(a)=0 then sgn(p_i(a))=sgn(p’(a)) and sgn(p’(a)!=0

2. If p_i(a)=0 then sgn(p_i-1(a))=-sgn(p_i+1(a))

3. p_l does not change its sign

4. rem(p_l-1,p_l)=0

What is the procedure?

[for R.CAD.QFNRA]

Split C until each sub-interval I contains at most one real root

What are possible enhancements?

[for R.CAD.QFNRA, 2]

1. Incrementality with split regarding to new constraint

2. Collect infeasible subsets for each CAD interval one constraint not satisfying the sign condition

What are the two phases?

[for Rⁿ.CAD.QFNRA, 2]

1. In projection phase decrease dimension step by step

2. In construction phase increase dimension step by step

What holds for delineability for P?

[for Rⁿ.CAD.QFNRA, 3]

1. #roots of p_i(a) is constant

2. #differentRoots of p_i(a) is constant

3. #commonRoots of p_i(a) and p_j(a) is constant

What holds for CAD C?

[for Rⁿ.CAD.QFNRA, 4]

1. Cup C = Rⁿ

2. For all cells of C the cut is empty

3. If n=1 then every cell is maximal P-sign Invariant region

4. If n>1 then every cell of C’ is P-delineable and cell \subseteq cell’ x R is a maximal P-sign invariant region

What holds for CAD projection?

[for Rⁿ.CAD.QFNRA, 3]

1. Mapping decreasing one dimension

2. If any region R of R^n-1 is proj(P)-sign invariant iff R is P-delineable

3. Usually |proj(P)| = |P|² // O(|P|^{2^n-1}) for univariate case

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

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

1. Polynomials p 2. constraints c and 3. formulas phi

What are the members of a polynomials p of nonlinear real arithmetics? [5]

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

const, variable x, p+p, p–p, p*p // * makes the difference to linear

What are the members of a constraint c of nonlinear real arithmetics? [2]

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

p < 0, p = 0

What are the members of a formula phi of nonlinear real arithmetics? [3]

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

c, \neg phi, phi \land phi

What is a characteristic of interval constraint propagation (ICP)? [3]

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

1. Incomplete, might return “unknown”

2. Combine with complete procedure implemented in the backend

3. Cheap reduction of search space method in case of “unknown”

What is the definition of an interval I? [5]

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

1. Left and right including or excluding (with inf) bounds

2. Simple case with [l,u], [l,inf) and (-inf,u] only

3. Bounded if both bounds are real-valued

4. Diameter is width of interval

5. n-dimensional box with [l1,u1] x … x [ln,un]

What are the rules for interval arithmetic? [7]

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

1. Constants and variables are interval-valued

2. A+B = [la+lb, ua+ub]

3. A-B = [la-ub, ua-lb]

4. A*B = [min_prod, max_prod]

5. A*A = [min_prod, max_prod] cut [0,inf)

6. A/B = A*1/B // 0 \notin B

7. A/B = (-inf,1/min] cup [1/max,inf) // 0 \in B

What is the definition of a contraction candidate (CC)?

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

Pair of constraint and variable

What are the characteristics of a contraction operator? [3]

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

1. Not dropping solutions

2. Does current box has no solution? // Usually not guaranteed

3. Contract as long as gain is large enough

What are possible contraction operators? [2]

Tastatur-Befehle:

= drehen,

= vor-/rückwärts,

= scrollen

1. Interval constraint propagation (ICP)

2. Interval Newton method (INM)

What is the goal of the interval constraint propagation algorithm?

Goal is to obtain an empty box (UNSAT) or to reach a diameter

What is the solution of the interval constraint propagation algorithm?

Solution is a non-empty box forwarded to a completing method

What is the step of the interval constraint propagation algorithm?

Choose CC and perform a contraction

What are the characteristics of the weight heuristic for the next contraction in the interval constraint propagation algorithm? [5]

1. r_k+1^ij = gain_rel = 1 – D_new/D_old

2. Each contraction has weight w_k^ij \in [0,1]

3. Update weight with w_k+1^ij = w_k^ij + a*(r_k+1^ij – w_k^ij)

4. Choose CC with highest weight over threshold eps

5. If no CC is over threshold eps split manually

What is another heuristic beside the weight heuristic for the next contraction in the interval constraint propagation algorithm?

Traverse history tree pre-order

What are the characteristics of the history tree for the interval constraint propagation algorithm? [4]

1. Search box

2. Applied contractions

3. Splitting dimensions

4. Collect infeasible subsets // Also possible

What are possible improvements of the interval constraint propagation algorithm? [5]

1. More sophisticated contraction (INM)

2. Linear solver for linear constraints

3. Box validation against linear feasible regions // Separate inside from partly covered case

4. SAT-solver for box-choice

5. Splitting heuristics

How complex is satisfiability checking for QFNRA?

Best known method for QFNRA formulas have exponential complexity

What holds for the diameter D of an interval? [4]

1. D_i = u-l

2. inf if i unbounded

3. 0 if i apoint interval

4. negative if i empty

How does the preprocessing for ICP contraction works?

Linearization, separate linear and nonlinear constrains with new variables

1 / 63

Lernkarten

What is the definition?

[univariate form.definition.CAD.QFNRA]

p = a_kx^k + … + a₁x¹ + a₀x⁰ with a_k != 0

What does square free means?

[definition.CAD.QFNRA]

No square factors i.e. no repeated roots

What is the degree of a polynomial?

[definition.CAD.QFNRA]

deg(p) = max_0<j<k+1(Sum_i=1ⁿe_ij) // Max sum of exponents

When is a formula phi linear?

[definition.CAD.QFNRA]

If every p has deg(p)<2

When is a formula phi non-linear?

[definition.CAD.QFNRA]

If one p has deg(p)>1

What is the solution space?

[definition.CAD.QFNRA]

Possible assignment for variables

What is the sign of a polynomial for input a?

[definition.CAD.QFNRA]

One element of {-1,0,1}

What are the characteristics?

[region.definition.CAD.QFNRA, 4]

1. Non-empty

2. Connected

3. Subset of Rⁿ

4. Sign-invariant if all polynomials have same sign

What does connected means?

[region.definition.CAD.QFNRA]

If for all A,B holds (R cut A) cup (R cut B) is R

What are the characteristics?

[roots.definition.CAD.QFNRA, 4]

1. Amount lies between 0 and deg(p)

2. Sign changes only here

3. sigma(e) is number of sign changes in a sequences

4. For each a<b #distinctRealRoots of p is sigma(a)-sigma(b)

What are the types?

[roots.definition.CAD.QFNRA, 4]

1. Rational

2. Irrational

3. Not representable by radicals

4. Interval representation with one root in (l,r)

What is the idea?

[CAD.QFNRA, 3]

1. Assume finite set P of polynomials with sign condition for each p

2. Produce decompositions of Rⁿ into a finite number of P-sign-invariant regions (So-called CAD cells)

3. Test sample point from each CAD cells

What are the outcomes of testing the sample point?

[idea.CAD.QFNRA]

If all sign conditions satisfied for #point>0 return SAT else return UNSAT

What is the cauchy bound C?

[for R.CAD.QFNRA, 2]

1. C = 1+max(|a_i|/|a_k|) >= real root |e| with a_k most-left coefficient

2. (-C,C) is interval containing all real roots

What is the idea?

[sturm seq.for R.CAD.QFNRA, 2]

1. Counts real roots in open interval

2. Finites sequence of polynomials of decreasing degree

How to compute?

[sturm seq.for R.CAD.QFNRA, 3]

1. p₀=p

2. p₁=p’

3. p_i=-rem(p_i-2,p_i-1) with rem is remainder of polynomial division of p₀ by p₁

What are the properties?

[sturm seq.for R.CAD.QFNRA, 4]

1. If p(a)=0 then sgn(p_i(a))=sgn(p’(a)) and sgn(p’(a)!=0

2. If p_i(a)=0 then sgn(p_i-1(a))=-sgn(p_i+1(a))

3. p_l does not change its sign

4. rem(p_l-1,p_l)=0

What is the procedure?

[for R.CAD.QFNRA]

Split C until each sub-interval I contains at most one real root

What are possible enhancements?

[for R.CAD.QFNRA, 2]

1. Incrementality with split regarding to new constraint

2. Collect infeasible subsets for each CAD interval one constraint not satisfying the sign condition

What are the two phases?

[for Rⁿ.CAD.QFNRA, 2]

1. In projection phase decrease dimension step by step

2. In construction phase increase dimension step by step

What holds for delineability for P?

[for Rⁿ.CAD.QFNRA, 3]

1. #roots of p_i(a) is constant

2. #differentRoots of p_i(a) is constant

3. #commonRoots of p_i(a) and p_j(a) is constant

What holds for CAD C?

[for Rⁿ.CAD.QFNRA, 4]

1. Cup C = Rⁿ

2. For all cells of C the cut is empty

3. If n=1 then every cell is maximal P-sign Invariant region

4. If n>1 then every cell of C’ is P-delineable and cell \subseteq cell’ x R is a maximal P-sign invariant region

What holds for CAD projection?

[for Rⁿ.CAD.QFNRA, 3]

1. Mapping decreasing one dimension

2. If any region R of R^n-1 is proj(P)-sign invariant iff R is P-delineable

3. Usually |proj(P)| = |P|² // O(|P|^{2^n-1}) for univariate case

Lernen

SC Chapter 8 Quantifier-free Non-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