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

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

ToySolver.Arith.Cooper

Contents

Description

Naive implementation of Cooper's algorithm

Reference:

See also:

Synopsis

Language of presburger arithmetics

type ExprZ = Expr Integer Source

Linear arithmetic expression over integers.

data Lit Source

Literals of Presburger arithmetic.

Constructors

IsPos ExprZ

IsPos e means e > 0

Divisible Bool Integer ExprZ
  • Divisible True d e means e can be divided by d (i.e. d | e)
  • Divisible False d e means e can not be divided by d (i.e. ¬(d | e))

Instances

type QFFormula = BoolExpr Lit Source

Quantifier-free formula of Presburger arithmetic.

fromLAAtom :: Atom Rational -> QFFormula Source

(.|.) :: Integer -> ExprZ -> QFFormula Source

d | e means e can be divided by d.

evalQFFormula :: Model Integer -> QFFormula -> Bool Source

evalQFFormula M φ returns whether M ⊧_LIA φ or not.

type Model r = VarMap r Source

A Model is a map from variables to values.

Projection

project :: Var -> QFFormula -> (QFFormula, Model Integer -> Model Integer) Source

project x φ returns (ψ, lift) such that:

  • ⊢_LIA ∀y1, …, yn. (∃x. φ) ↔ ψ where {y1, …, yn} = FV(φ) \ {x}, and
  • if M ⊧_LIA ψ then lift M ⊧_LIA φ.

projectN :: VarSet -> QFFormula -> (QFFormula, Model Integer -> Model Integer) Source

projectN {x1,…,xm} φ returns (ψ, lift) such that:

  • ⊢_LIA ∀y1, …, yn. (∃x1, …, xm. φ) ↔ ψ where {y1, …, yn} = FV(φ) \ {x1,…,xm}, and
  • if M ⊧_LIA ψ then lift M ⊧_LIA φ.

projectCases :: Var -> QFFormula -> [(QFFormula, Model Integer -> Model Integer)] Source

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

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

projectCasesN :: VarSet -> QFFormula -> [(QFFormula, Model Integer -> Model Integer)] Source

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

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

Quantifier elimination

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

Eliminate quantifiers and returns equivalent quantifier-free formula.

eliminateQuantifiers φ returns (ψ, lift) such that:

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

φ may or may not be a closed formula.

Constraint solving

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

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

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

solveQFFormula :: VarSet -> QFFormula -> Maybe (Model Integer) Source

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

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

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

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

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

solveQFLIRAConj {x1,…,xn} φ I returns Just M that M ⊧_LIRA φ when such M exists, returns Nothing otherwise.

  • FV(φ) must be a subset of {x1,…,xn}.
  • I is a set of integer variables and must be a subset of {x1,…,xn}.