Skip to content

Monotonic Theories

Definition: a positive predicate or function is monotonic iff \(p(\cdots,0,\cdots)\to p(\cdots,1,\cdots)\)

If the original predicate/function is true, after we flip any input 0 to 1, the predicate/function is still true.

A theory \(T\) is monotonic iff

  • The only sort is Boolean
  • All predicates are monotonic
  • All functions are monotonic

Assumption: the theory is decidable and quantifier free

MonoSAT

Decision procedure for monotonic theories

Idea: split predicates and variables in two sets

Example predicates: Given a graph \(G\). The solver will select a subset of edges to include in the graph so that the predicate holds.

  • Reachability: given two vertices \(v_1,v_2\), enabling additional edges will add to reachability
  • Minimum spanning tree: given a weighted undirected graph, adding an edge could decrease the weight.

MonoSAT accepts an extension of DIMACS in input.

  • Edges are variables (not literals)
  • Every edge must be assigned a variable
  • No two edges can share the same variable

Applications of MonoSAT

Checking for some properties of AWS

Bounded Model Checking

Data-flow analysis to prove correct usage of could APIs

Monotonic SAT theories to check network configurations

Verification of AWS identity and access management

......