Approximate Quantified Constraint Solving (AQCS)

Stefan Ratschan

AQCS is a program for solving quantified constraints approximately. A quantified constraint is a formula of first-order predicate logic containing the following symbols: Variables ranging over the reals, floating point interval constants, the function symbols + and ., the predicate symbols <= , =, <, >= and >, and the quantifiers exist and forall . The output for a given quantified constraint is a set of boxes on which the constraint is guaranteed to be true and a set of boxes on which the constraint is guaranteed to be false. For constraints with less than three free variables graphical output is also available.

Note that currently AQCS usually is only useful for inequalities but not for equalities. A new version that also efficiently deals with equalities will be available in short time!

Software Documentation:
HTML:
DVI:
Postscript:
Related Papers:
Download Linux Binaries:
Dynamically linked:
Small, but needs compatible shared libraries
Statically linked:
Larger, does not need compatible shared libraries
Copying:

This software in its binary form is available for free use provided that its usage is properly cited in resulting applications and publications. Further distribution is permitted under the constraint that the whole set of files is distributed without modification.

I would appreciate if you would notify me of your use of AQCS, inform be about bugs, and send me resulting publications.