Computer Algebra & Symbolic Computation

I am a member of the Reduce developer group. Reduce is an open source computer algebra system written entirely in Standard Lisp. Up till now I mainly contributed to the Redlog (Reduce logic) package. I wrote a SAT, QSAT and PQSAT solver, and a quantifier elimination procedure based on these for quantifier elimination over initial Boolean algebras. For a closer look and a manual for these implementations, have a look into my master’s thesis.

Examples

Here I present some examples of the (P/Q)SAT engine of Redlog at work.

Example 1 (Quantifier elimination with rlqsat)
Quantifier elimination for the formula: \exists x \ \forall y \ \forall u \ (x \lor y \lor \neg u) \land (\neg x \lor \neg y \lor w)
(light lines are input, dark lines are output)

load redlog;
rlset ibalp;
f := (X or Y or not U) and (not X or not Y or W);
f := (x = 1 or y = 1 or not(u = 1)) and (not(x = 1) or not(y = 1) or w = 1)
g := ex(x,all(y,all(u,f)));
g := ex x all y all u ((x = 1 or y = 1 or not(u = 1))
     and (not(x = 1) or not(y = 1) or w = 1))
rlqsat g;
w = 1



Example 2 (Solving of a .cnf or .qdimacs file in Dimacs format)

load redlog;
rlset ibalp;
rlqsatdimacs "test.qdimacs";
true



Example 3 (Reading of a .cnf or .qdimacs file in Dimacs format)

load redlog;
rlset ibalp;
f := rlreaddimacs "test.qdimacs";
f := ex var2 all var3 ex var1 ((var1 = 1 or var3 = 1) and (var3 = 0 or var2 = 1)
     and (var2 = 0 or var3 = 0 or var1 = 1) and var2 = 1)
Publications

  • Generalised SAT Checking in a First-Order Logic Framework
    Christoph Zengler
    Diploma Thesis at the University of Passau, 2008
    Download Thesis

Talks