toysolver-0.2.0: Assorted decision procedures for SAT, Max-SAT, PB, MIP, etc

Copyright(c) Masahiro Sakai 2011-2013
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

ToySolver.Arith.FourierMotzkin

Contents

Description

Naïve implementation of Fourier-Motzkin Variable Elimination

Reference:

Synopsis

Primitive constraints

data Constr Source

Atomic constraint

Constructors

IsNonneg ExprZ

e ≥ 0

IsPos ExprZ

e > 0

IsZero ExprZ

e = 0

Projection

project :: Var -> [Atom Rational] -> [([Atom Rational], Model Rational -> Model Rational)] Source

project x φ returns [(ψ_1, lift_1), …, (ψ_m, lift_m)] such that:

  • ⊢_LRA ∀y1, …, yn. (∃x. φ) ↔ (ψ_1 ∨ … ∨ φ_m) where {y1, …, yn} = FV(φ) \ {x}, and
  • if M ⊧_LRA ψ_i then lift_i M ⊧_LRA φ.

projectN :: VarSet -> [Atom Rational] -> [([Atom Rational], Model Rational -> Model Rational)] Source

projectN {x1,…,xm} φ returns [(ψ_1, lift_1), …, (ψ_n, lift_n)] such that:

  • ⊢_LRA ∀y1, …, yp. (∃x. φ) ↔ (ψ_1 ∨ … ∨ φ_n) where {y1, …, yp} = FV(φ) \ {x1,…,xm}, and
  • if M ⊧_LRA ψ_i then lift_i M ⊧_LRA φ.

Quantifier elimination

eliminateQuantifiers :: Formula (Atom Rational) -> Maybe (Formula (Atom Rational)) Source

Eliminate quantifiers and returns equivalent quantifier-free formula.

eliminateQuantifiers φ returns (ψ, lift) such that:

  • ψ is a quantifier-free formula and LRA ⊢ ∀y1, …, yn. φ ↔ ψ where {y1, …, yn} = FV(φ) ⊇ FV(ψ), and
  • if M ⊧_LRA ψ then lift M ⊧_LRA φ.

φ may or may not be a closed formula.

Constraint solving

solveFormula :: VarSet -> Formula (Atom Rational) -> SatResult Rational Source

  • solveFormula {x1,…,xm} φ returns Sat M such that M ⊧_LRA φ when such M exists,
  • returns Unsat when such M does not exists, and
  • returns Unknown when φ is beyond LRA.

solve :: VarSet -> [Atom Rational] -> Maybe (Model Rational) Source

solve {x1,…,xn} φ returns Just M that M ⊧_LRA φ when such M exists, returns Nothing otherwise.

FV(φ) must be a subset of {x1,…,xn}.