Constraint graphs & negative-cycle detection for IDL satisfiability
IDL / QF_IDL
IDL constraint: of the form x − y ≤ c with integer variables and constant c.
· Build a directed weighted graph: each constraint x−y≤c adds edge x→y with weight c.
· UNSAT iff the graph contains a negative-weight cycle.
· Detection via Bellman-Ford: if distances still decrease after |V| rounds, a negative cycle exists.
Input
Examples:
One per line: x - y <= 5 Ops: <= < >= > =
Examples:
Paste SMT-LIB2 or upload a .smt2 file. Supports QF_IDL assertions with (<= (- x y) c).