Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Experimental Descriptive Complexity
Charles Jordan
Joint work with Marco Carmosino and Neil Immerman.
Festschrift for Dexter Kozen, LNCS 7230, pp. 24–34, 2012.
DE: http://www.cs.umass.edu/∼immerman/deMay 18, 2012

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Our Environment
DescriptiveEnvironment (DE)DE is a playground for (descriptive) complexity theorists.
Implements objects and tools of descriptive complexity.
Similar to Mathematica in spirit.
Helps us use computers to attack big problems.
Research finding counter-examples, reductions, examining
complicated maps between problems,visualization, . . . .
Teaching descriptive complexity, finite model theory, logic,complexity theory, . . . .
Development rapid programming, e.g., easily using SAT solvers
as general-purpose solvers in a rigorous way.
Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Outline1

Introduction

2

Examples3

Overview

4

Future Uses

5

Programming

6

Conclusion

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

ProgrammingConclusion

Relational Structures in DE
Examples in DE
string is new vocabulary{S:1}.
graph is new vocabulary{E:2, s, t}.

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Relational Structures in DE
Examples in DE
string is new vocabulary{S:1}.
graph is new vocabulary{E:2, s, t}.
primes100 is new structure{string,100, S:1 is (1<x1 &\A x, y.(x<=x1 & y<=x) : ((x*y=x1)->(x=1|y=1)))}.

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

ProgrammingConclusion

Relational Structures in DE
Examples in DE
string is new vocabulary{S:1}.
graph is new vocabulary{E:2, s, t}.
primes100 is new structure{string,100, S:1 is (1<x1 &\A x, y.(x<=x1 & y<=x) : ((x*y=x1)->(x=1|y=1)))}.
line10 is new structure{graph, 10, E:2 is x2=x1+1,s is 0, t is 9}.

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Relational Structures in DE
Examples in DE
string is new vocabulary{S:1}.
graph is new vocabulary{E:2, s, t}.
primes100 is new structure{string,100, S:1 is (1<x1 &\A x, y.(x<=x1 & y<=x) : ((x*y=x1)->(x=1|y=1)))}.
line10 is new structure{graph, 10, E:2 is x2=x1+1,s is 0, t is 9}.
primes100.S.
:{(2), (3), (5), (7), (11), (13), (17), (19), (23),(29), (31), (37), (41), (43), (47), (53), (59), (61),(67), (71), (73), (79), (83), (89), (97)}draw(line10).
Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

QueriesQuery (Computation)Let vocabulary τ := {Ra11 , . . . , Ras s , c1 , . . . , ct }.
A query f : STRUC(σ) → STRUC(τ) is an (s + t + 2)-tuple,hk, ϕ0 , ϕ1 , . . . , ϕs , ψ1 , . . . , ψt i .
Let A ∈ STRUC(σ). Then, f (A) is defined as follows:
1Universe U is {hx1 , . . . , xk i | xi ∈ UA , (A, hx1 , . . . , xk i) |= ϕ0 i.

2Rif (A)isUai ∩ {hhx11 , . . . , x1k i, . . . , hxa1i , . . . , xaki ii | (A, . . .) |= ϕi } .
3

cj is the unique hx1 , . . . , xk i such that (A, hx1 , . . . , xk i) |= ψj .

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Queries in DE
Examples in DE
Reach is new bquery{graph, TC[x,y:E(x,y)](s,t)}.

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Queries in DE
Examples in DE
Reach is new bquery{graph, TC[x,y:E(x,y)](s,t)}.
Reach(line10).
:\tthrcolor is new bquery{graph, \E R:1 : \E G:1 : \E
B:1 : \A x, y : ((R(x)|G(x)|B(x)) &(E(x,y)->∼((R(x)&R(y))|(G(x)&G(y))|(B(x)&B(y)))))}.
thrcolor(line10).
:\tExperimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Queries in DE
Examples in DE
Reach is new bquery{graph, TC[x,y:E(x,y)](s,t)}.
Reach(line10).
:\tthrcolor is new bquery{graph, \E R:1 : \E G:1 : \E
B:1 : \A x, y : ((R(x)|G(x)|B(x)) &(E(x,y)->∼((R(x)&R(y))|(G(x)&G(y))|(B(x)&B(y)))))}.
thrcolor(line10).
:\t
I is new query{graph,string,2,\t,S:1 is E(x1,x2)}.
set100 is I(line10).
set100.S.
Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Queries in DE
Examples in DE
Reach is new bquery{graph, TC[x,y:E(x,y)](s,t)}.
Reach(line10).
:\tthrcolor is new bquery{graph, \E R:1 : \E G:1 : \E
B:1 : \A x, y : ((R(x)|G(x)|B(x)) &(E(x,y)->∼((R(x)&R(y))|(G(x)&G(y))|(B(x)&B(y)))))}.
thrcolor(line10).
:\t
I is new query{graph,string,2,\t,S:1 is E(x1,x2)}.
set100 is I(line10).
set100.S.
:{(1), (12), (23), (34), (45), (56), (67), (78), (89)}
Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

ProgrammingConclusion

Reductions in DE
A reduction r from P to P 0 is a query such thatA ∈ P ⇐⇒ r(A) ∈ P 0 .
Examples in DE
thrcoltosat is new reduction{graph, sat, 3, x1<=3,P:2 is x1=3&x4=0&x2=0&x3=x6&x5<3,N:2 is x4=0 & E(x2,x3) & (x1=x5 & (x6=x2 | x6=x3)) &x1<3}.
scline is thrcoltosat(line10).
minisat(scline).
:\tthreecolorwithsat(line10).
:\tExperimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

ProgrammingConclusion

Finding Reductions
Examples in DE
a1 is new bquery{string, \forall x:S(x)}.
a0 is new bquery{string, \forall x:∼S(x)}.
redfind(a1,a0).
: A0:=new reduction{string,string,1,\t,S:1 is (∼S(x1))}.

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

ProgrammingConclusion

Finding Reductions
Examples in DE
a1 is new bquery{string, \forall x:S(x)}.
a0 is new bquery{string, \forall x:∼S(x)}.
redfind(a1,a0).
: A0:=new reduction{string,string,1,\t,S:1 is (∼S(x1))}.
rs is new vocabulary{R:1, S:1}.
gr is new vocabulary{E:2}.
eras is new bquery{rs, \exists x:R(x)&\forall y:S(y)}.
axey is new bquery{gr, \forall x:\exists y:E(x,y)}.
redfind(eras,axey).
: A0:=new reduction{rs,gr,1,\t,E:2 is (S(x1)&R(x2))}.

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Outline1

Introduction

2

Examples3

Overview

4

Future Uses

5

Programming

6

Conclusion

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

What does DE do?

Creating vocabularies and structures.
Defining queries and reductions in SO∃(TC).
Calling Mace41 to get a structure that satisfies a desired FO
property.
Using minisat() and zchaff() to use built-in SAT solvers
MiniSat and zChaff to evaluate Boolean satisfiability.
Loading structures (DIMACS-format graphs, etc.).
Saving and drawing structures.

1

A first-order model-finding program.

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

What will DE do?

1

Adding additional operators (IFP, etc.).

2

Try to find reductions (in progress).

3

Play Ehrenfeucht-Fraı̈ssé games.

4

Visualizing queries, TC, etc.

5

Example-driven query construction.

6

Other UIs.

7

Possibly interact with automatic synthesis of fastprograms.

8

New functionality with plug-ins.

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Outline1

Introduction

2

Examples3

Overview

4

Future Uses

5

Programming

6

Conclusion

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Finding Reductions I
ReductionFinder
Crouch, Immerman and Moss (2010) developed a reduction
finding tool. We are integrating an improved version into DE.
Basic idea (trying A 6 B):
1Take a random G0 of small size. Ask the SAT solver for asimple reduction f0 s.t. G0 ∈ A ⇐⇒ f (G0 ) ∈ B.

2

Ask the SAT solver for a small G1 that’s a counter-example
to f (i.e., G1 ∈ A ⊕ f (G1 ) ∈ B).

3

Repeat: ask for a new reduction on the examples so far,then ask for a new counter-example.

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

ProgrammingConclusion

Finding Reductions II

NL=coNL
NI’s original proof of NL=coNL constructed an 8-ary,quantifier-free projection from REACH to REACH.
Are computers fast enough to put this reduction in reach ofautomatic discovery? ReductionFinder is too slow; possible todo better.
Question
What else could be found?

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Property Testing

Recent Proofs by CJ
There are untestable properties in [∀∃∀, (0, 1)] in one model oftestability.
To extend to other models,
are large models of a particular FO formula probably far
from models of another?
I’d like to check (large) examples – adding distancecomputation to DE would help.
The distances are probably non-trivial to compute.

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Playing EF Games

Plans
We plan to automate EF games:
1

Playing the computer.

2

The computer plays itself.

3

Analysis of strategies.

Uses
Can DE help with complicated games, like those forFO(rank,LFP)?

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Outline1

Introduction

2

Examples3

Overview

4

Future Uses

5

Programming

6

Conclusion

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Programming with Reductions IBasic Problem
Many times, we have some problem we want to solve. So, wewrite a program to solve it.
Problems:
Error-prone and time-consuming.
Hard to produce a program that is really optimized.

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Programming with Reductions I
Basic Problem
Many times, we have some problem we want to solve. So, wewrite a program to solve it.
Problems:
Error-prone and time-consuming.
Hard to produce a program that is really optimized.
Programming with Reductions
Write a reduction to (e.g.,) SAT and use a good SAT solver.
Usually, these reductions are easy.
Computation is dominated by SAT solver.
Leverage research effort on SAT solvers.
Easy and fast development of decently-optimized
programs.
Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Programming with Reductions II
ExamplesKugele. Efficient Solving of Combinatorial Problems using
SAT-Solvers. Diplomarbeit in Informatik, TU München, 2006.

Ramani, Aloul, Markov and Sakallah. Breaking
Instance-Independent Symmetries in Exact GraphColoring. J. Artif. Intell. Res. 26:289–322, 2006.
Mitchell and Ternovska. Knowledge Representation,
Search Problems and Model Expansion. Knowing,
Reasoning and Acting, 347–362, 2011.
Joao Marques-Silva. Practical applications of Boolean
satisfiability. Proc. WODES 2008, 74–80, 2008.
Why use descriptive complexity?

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Programming with Reductions II
ExamplesKugele. Efficient Solving of Combinatorial Problems using
SAT-Solvers. Diplomarbeit in Informatik, TU München, 2006.

Ramani, Aloul, Markov and Sakallah. Breaking
Instance-Independent Symmetries in Exact Graph
Coloring. J. Artif. Intell. Res. 26:289–322, 2006.
Mitchell and Ternovska. Knowledge Representation,
Search Problems and Model Expansion. Knowing,
Reasoning and Acting, 347–362, 2011.
Joao Marques-Silva. Practical applications of Boolean
satisfiability. Proc. WODES 2008, 74–80, 2008.
Why use descriptive complexity?
A rigorous way to do what is currently done adhoc.
Nobody wants to write Turing machine transition tables all day.
Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Outline1

Introduction

2

Examples3

Overview

4

Future Uses

5

Programming

6

Conclusion

Experimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Summary

We implemented DescriptiveEnvironment (DE), an interactive
playground for descriptive complexity.
Freely available2 under an ISC license.
Usable now (we use it), plans for improvement.
We encourage anyone to use it, please give us suggestions,improvements, etc.

2

http://www.cs.umass.edu/∼immerman/deExperimental Descriptive Complexity

Charles Jordan

Introduction

ExamplesOverview

Future Uses

Programming

Conclusion

Thank you!

Experimental Descriptive Complexity

Charles Jordan