QF_NRA Logic

Quantifier-Free Nonlinear Real Arithmetic Explained

What is QF_NRA?

QF_NRA stands for Quantifier-Free Nonlinear Real Arithmetic. It's a logical theory used in SMT (Satisfiability Modulo Theories) solvers to describe and solve problems involving real numbers and nonlinear constraints.

Breaking Down the Acronym:

  • QF (Quantifier-Free): No ∀ (for all) or ∃ (there exists) quantifiers
  • N (Nonlinear): Variables can multiply: x·y, x², x³
  • R (Real): Real numbers (3.14, -2.5, √2), not just integers
  • A (Arithmetic): Operations like +, -, ×, ÷, <, ≤, =

Your Optimization Problem

Your constrained optimization problem is a perfect example of QF_NRA:

Minimize: (x₁ - 2)² + (x₂ - 1)²
Subject to: x₁² + x₂² ≤ 1

Why this is QF_NRA:

  • ✓ Real variables (x₁, x₂ ∈ ℝ)
  • ✓ Nonlinear (squaring: x₁², x₂²)
  • ✓ No quantifiers (no ∀ or ∃)

Examples in QF_NRA

Example 1: Circle Constraint

x² + y² ≤ 1 ; All points inside or on a unit circle

Example 2: Polynomial Constraint

x³ - 2x² + x - 5 ≤ 0 ; A cubic polynomial constraint

Example 3: Product Constraint

x·y ≥ 10 ∧ x + y ≤ 20 ; Product of two variables with linear constraint

What QF_NRA Can Express

✓ Supported Operations

  • Basic Arithmetic: x + y, x - y, x · y, x / y, x²
  • Comparisons: x < y, x ≤ y, x > y, x ≥ y, x = y, x ≠ y
  • Boolean Logic: AND (∧), OR (∨), NOT (¬)

✗ Not Supported

  • Transcendental Functions: sin(x), cos(x), exp(x), log(x)
  • Integer Constraints: x ∈ ℤ (would need QF_NIA)
  • Quantifiers: ∀x, φ(x) (would need NRA without QF)

Comparison of SMT Logics

Logic Name Variables Multiply? Number Type
QF_LRA Linear Real Arithmetic ✗ No ℝ (reals)
QF_NRA Nonlinear Real Arithmetic ✓ Yes ℝ (reals)
QF_LIA Linear Integer Arithmetic ✗ No ℤ (integers)
QF_NIA Nonlinear Integer Arithmetic ✓ Yes ℤ (integers)

Why It Matters for Your Problem

The Issue with MathSAT

Your MathSAT installation only supports QF_LRA (linear arithmetic), not QF_NRA (nonlinear). This is why you got the error:

pysmt.exceptions.NonLinearError: ((x2 + -1.0) * (x2 + -1.0))

To support QF_NRA, MathSAT needs to be compiled with the MPFR library.

Z3 to the Rescue!

Z3 supports QF_NRA natively, which is why it works perfectly for your problem. Z3 uses sophisticated techniques including:

  • Interval arithmetic for variable bounds
  • Cylindrical algebraic decomposition (CAD) for exact solutions
  • Numerical methods for approximations

SMT-LIB Example

Here's how your problem looks in SMT-LIB 2.0 format:

; Declare we're using QF_NRA logic (set-logic QF_NRA) ; Declare real variables (declare-fun x1 () Real) (declare-fun x2 () Real) ; Constraint: x1² + x2² ≤ 1 (assert (<= (+ (* x1 x1) (* x2 x2)) 1.0)) ; Check if objective can be ≤ 1.6 (assert (<= (+ (* (- x1 2.0) (- x1 2.0)) (* (- x2 1.0) (- x2 1.0))) 1.6)) (check-sat) (get-model)

Key Takeaways

QF_NRA = Quantifier-Free Nonlinear Real Arithmetic

  • ✓ Perfect for your optimization problem
  • ✓ Z3 supports it natively
  • ⚠ MathSAT needs MPFR library for QF_NRA
  • ⚠ More complex than linear problems
  • ⚠ Solutions may be approximate

The solution for your problem: x₁ ≈ 0.894427, x₂ ≈ 0.447214, f(x) ≈ 1.527864

This represents the point on the unit circle closest to (2, 1).