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
Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 8 Quantifier-free Non-linear Real Arithmetic
-
- 1 / 63
-
Lernkarten
What are the components of the syntax of nonlinear real arithmetics? [3]
1. Polynomials p 2. constraints c and 3. formulas phi
What are the members of a polynomials p of nonlinear real arithmetics? [5]
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]
p < 0, p = 0
What are the members of a formula phi of nonlinear real arithmetics? [3]
c, \neg phi, phi \land phi
What is a characteristic of interval constraint propagation (ICP)? [3]
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]
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]
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)?
Pair of constraint and variable
What are the characteristics of a contraction operator? [3]
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]
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. rk+1ij = gainrel = 1 – Dnew/Dold
2. Each contraction has weight wkij \in [0,1]
3. Update weight with wk+1ij = wkij + a*(rk+1ij – wkij)
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
How to gain new bounds for ICP contraction? [3]
1. Update via cut with old bound
2. If < or <= take lold and unew
3. If > or >= take lnew and uold
What are the two steps of the ICP contraction? [2]
1. Insert current bounds for all except one variable in one constraint
2. Choose box if split of intervals occurred
How does the preprocessing for INM contraction works? [2]
1. Transform e1 ~ e2 to e1-e2 ~ 0
2. Transform inequation p ~ 0 to h-p = 0
How to gain new bounds for INM contraction? [3]
1. Update via cut with old bound
2. If < or <= take lold and min of uold or 0
3. If > or >= take max of lold or 0 and uold
What are the two steps of the INM contraction? [3]
1. Set starting interval A and sample point s
2. Compute A’ with Newton method
3. Get new bound
What is the original idea of the Newton method? [3]
1. Make initial guess so for univariate polynomial f(x)
2. si+1 = si – f(si)/f’(si)
3. Usually converges quadratically to r with f(r) = 0
What is the original idea of the Taylor’s theorem? [2]
1. For all s,x\in A exists d\in A
2. With f(x) = f(s) + (x-s)*f’(d)
What is the original idea of the componentwise multivariate Newton?
si+1 = Ncmp(s,f(x),xj) = si – f(si)/[df/dxj](si)
What is the adapted idea of the Newton method?
s – f(s)/f’(A) with s\in A
What is the adapted idea of the componentwise multivariate Newton? [6]
1. A = A1 x … x An with mid(Aj) middle point of interval
2. si+1 = Ncmp(A,f(x),xj) = mid(Aj)- f(A1,…,An)/[df/dxj](A1,…,An)
3. If f(x)=0 then x is in Ncmp
4. If cut is empty no x yields to f(x) = 0
5. No diverging behavior as the original
6. Drop boxes if they contract to empty
What kind of procedure is virtual substitution?
Existential quantifier elimination procedure
What is the condition of virtual substitution?
For every constraint of formula p(x)~0 degree of x in p(x) <= 2
What are the steps of virtual substitution? [2]
1. \exists is replaced by t \in test candidates T [t//var]
2. Side conditions are added
What is the goal of virtual substitution?
Goal is to find and return satisfying solution or explain unsatisfiability
What are the finite endpoints cases for virtual substitution for p=ax²+bx+c? [4]
1. If p is constant (for a=b=0) or no zeros then sign-invariant
2. If a=0 and b!=0 then x0 = -c/b
3. If a!=0 and b²-4ac>=0 then x1 = -b+sqrt(b²-4ac)/2a
4. If a!=0 and b²-4ac>0 then x2 = -b-sqrt(b²-4ac)/2a
What are the solution intervals cases for virtual substitution? [4]
1. If p=0 then [xi,xi]
2. If p < > != 0 then (-inf,xi), (xi,xj) and (xi,inf)
3. If p <= >= 0 then (-inf,xi), [xi,xi], [xi,xj] and (xi,inf)
4. Always (-inf,inf)
What are the test candidates T cases for virtual substitution? [2]
1. If p <= >= = 0 then zeros of p and -inf (A sufficiently small value)
2. If p < > != 0 then zeros of p+eps and -inf
What are the types of test candidates for virtual substitution? [3]
1. -inf
2. +eps
3. Contains sqrt
What are the forms of polynomials?
[definition.CAD.QFNRA, 2]
1. Normal and 2. univariate
What is the definition?
[normal form.definition.CAD.QFNRA]
p = a1x1e11 … xnen1 + … + akx1e1k … xnenk
