GitHub

SAT Solving

This section explains the satisfiability solving capabilities of SymbolicSMT.jl.

Satisfiability vs Provability

SymbolicSMT.jl provides two main types of queries:

Satisfiability (issatisfiable)

Question: "Can this expression be true given the constraints?"

using Symbolics, SymbolicSMT

@variables x::Real y::Real
constraints = Constraints([x > 0, y > 0])

# Can x be greater than 10?
issatisfiable(x > 10, constraints)  # true - yes, it's possible

Provability (isprovable)

Question: "Is this expression always true given the constraints?"

# Is x always positive?
isprovable(x > 0, constraints)  # true - yes, always true

# Is x always greater than y?
isprovable(x > y, constraints)  # false - not necessarily true

Understanding Return Values

Three-Valued Logic

Both functions can return three possible values:

  • true: Yes (satisfiable/provable)
  • false: No (unsatisfiable/not provable)
  • nothing: Unknown (solver timeout or undecidable)
result = issatisfiable(complex_expression, constraints)

if result === true
    println("Satisfiable!")
elseif result === false
    println("Unsatisfiable!")
else  # result === nothing
    println("Solver couldn't determine")
end

Practical Interpretation

For issatisfiable:

  • true: There exists at least one solution
  • false: No solution exists
  • nothing: Solver cannot determine (rare)

For isprovable:

  • true: Statement is always true (tautology under constraints)
  • false: Statement can be false (not a tautology)
  • nothing: Solver cannot determine (rare)

Resolution with resolve

The resolve function combines both operations to simplify expressions:

@variables t::Real
time_constraints = Constraints([t >= 0, t <= 24])

# Expressions that resolve to constants
resolve(t >= 0, time_constraints)   # true (always true)
resolve(t < 0, time_constraints)    # false (never true)
resolve(t > 30, time_constraints)   # false (impossible)

# Expressions that cannot be resolved
resolve(t > 12, time_constraints)   # t > 12 (unchanged)

Practical Examples

Example 1: Geometric Reasoning

@variables x::Real y::Real

# Points inside unit circle
unit_circle = Constraints([x^2 + y^2 <= 1])

# Can a point be outside the circle?
issatisfiable(x^2 + y^2 > 1, unit_circle)  # false

# Are all points within distance 1 of origin?
isprovable(x^2 + y^2 <= 1, unit_circle)    # true

Example 2: Logical Reasoning

@variables p::Bool q::Bool r::Bool

# Logical constraints: if p then q, if q then r
implications = Constraints([
    !p | q,  # p => q
    !q | r   # q => r
])

# If p is true, is r necessarily true?
isprovable(p => r, implications)  # true (transitivity)

# Can all three be false?
issatisfiable(!p & !q & !r, implications)  # true

Example 3: Optimization Bounds

@variables x::Real y::Real

# Feasible region for optimization
feasible = Constraints([
    x >= 0, y >= 0,           # Non-negativity
    x + y <= 10,              # Resource constraint
    2*x + y <= 15             # Additional constraint
])

# Is the origin feasible?
issatisfiable(x == 0 & y == 0, feasible)  # true

# Is there a solution with both variables > 5?
issatisfiable(x > 5 & y > 5, feasible)    # false

Advanced SAT Solving Concepts

Contradiction Detection

Detect when constraint sets are unsatisfiable:

contradictory = Constraints([x > 5, x < 3])

# Any expression is unsatisfiable with contradictory constraints
issatisfiable(true, contradictory)   # false
issatisfiable(x == 4, contradictory) # false

Implication Checking

Check if one expression implies another:

@variables a::Real b::Real

constraints = Constraints([a > 0, b > 0])

# Does a > 5 imply a + b > 5?
# This is equivalent to: isprovable(a + b > 5, constraints * {a > 5})
extended = Constraints([a > 0, b > 0, a > 5])
isprovable(a + b > 5, extended)  # true

Equivalence Checking

Check if two expressions are equivalent under constraints:

expr1 = x + y
expr2 = y + x

# Are they equivalent? (Check both directions)
left_to_right = isprovable(expr1 == expr2, constraints)   # true
right_to_left = isprovable(expr2 == expr1, constraints)   # true

Solver Limitations

Current Limitations

  • Real arithmetic: Currently mapped to integer arithmetic in Z3
  • Division: Limited support for division operations
  • Nonlinear expressions: Complex nonlinear constraints may be slow
  • Quantifiers: No direct support for universal/existential quantifiers

When Z3 Cannot Decide

Some problems are undecidable or too complex:

# Very complex nonlinear constraint
complex = Constraints([sin(x*y) + cos(x^2 + y^2) > exp(x - y)])

result = issatisfiable(x > 0, complex)
# May return `nothing` if too complex

Debugging Tips

Check Constraint Satisfiability First

Always verify your constraints have solutions:

cs = Constraints([...])
if issatisfiable(true, cs) == false
    println("Warning: Constraint set is unsatisfiable!")
end

Simplify Complex Expressions

Break down complex expressions:

# Instead of one complex constraint
complex_expr = (x > 0) & (y > 0) & (x^2 + y^2 < 1) & (x + y > 0.5)

# Use multiple simpler constraints
simple_constraints = Constraints([
    x > 0,
    y > 0,
    x^2 + y^2 < 1,
    x + y > 0.5
])

Test with Known Solutions

Verify your constraint logic with known solutions:

cs = Constraints([x >= 0, y >= 0, x + y <= 1])

# Test a known feasible point
issatisfiable(x == 0.3 & y == 0.3, cs)  # Should be true

# Test a known infeasible point
issatisfiable(x == 0.8 & y == 0.8, cs)  # Should be false