What is this about?

This webpage contains the best known lower bounds for any deterministic finite state automata (DFA) that encodes the solutions to given quantifier free Presburger formulas (QF_LIA).

The set of QF_LIA formulas under consideration are those from the QF_LIA category of SMT-LIB release 2024 that are listed in this file.

The lower bounds are given as certificates following a specific homemade format.

Improve the best known lower bounds by submitting your certificates.

How to contribute?

Submit certificates

Submit one or more certificates improving the best known lower bounds.

Contact us at patapsco@imdea.org and we will provide a link where you can upload your certificate(s).

Upon successful validation your improved lower bounds will appear in the scoreboard and the certificates thereof will be available for download.

Improve our certificate generator Patapsco

Submit a pull request to our github repo patapsco

Write your own certificate generator

If you implement your own certificate generator and let us know about it we will add a link to it on this webpage.

Certificates

The certifcates we provide below were produced by our tool Patapsco. For more details see our paper.

Format

A certificate is a file in zip format which itself contains three files in text format:

• data.info: list the instance name as well as the lower bound recomputable form the prefixes and suffixes files.
• data-0.prefixes: list the prefixes in base 2, least significant digit first.
• data-1.suffixes: list the suffixes using the same format as for the prefixes.

data.info

{instance XYZ.smt2}
{lower-bound 572}

To output the content of data.info from a certificate file run: funzip certificate.table, alternatively you can run unzip -p certificate.table /data.info.

data-0.prefixes

(0,(0,0,0,0,0))
…
(3,(0,6,4,0,0))
(3,(0,6,4,0,0))
(3,(0,6,6,3,1))
(3,(0,7,1,1,3)) ←
(3,(0,7,2,0,1))
(3,(1,0,0,0,0))
(3,(1,1,1,2,0))
(3,(1,1,2,0,5))
(3,(1,1,4,0,0))
(3,(1,1,5,2,0))
(3,(1,3,0,6,2))
…

data-1.suffixes

(0,(0,0,0,0,0))
…
(2,(0,0,1,0,1))
(2,(0,0,1,0,1))
(2,(0,0,1,0,1))
(2,(0,0,1,0,1))
(2,(0,0,1,0,1))
(2,(0,0,1,0,1))
(2,(0,0,1,0,2))
(2,(0,0,1,0,2))
(2,(0,0,1,1,0))
(2,(0,0,1,1,0))
(2,(0,0,1,1,0))
…

How to read the files

Take the entry (3,(0,7,1,1,3)) from the prefix file.

In the formula corresponding to this certificate entry there are 5 free variables which coincide with the dimension of the innermost vector (0,7,1,1,3). Our certificates assume a base 2 (binary digit 0 and 1) encoding for the valuations of the variables of the formula.
The first number of the entry (3 in this case) means that each encoded binary digits word consists exactly of three symbols. For instance 0 for the first variable stands for 000, 7 for the second variable stands for 111, and 3 for the 5th and last variable stands for 110. Observe that 110 stands for 3 and not 6 because our encoding is least significant digit first.

So this entry corresponds to prefix given by the word (000, 111, 100, 100, 110).

Certificate validation

Make sure your certificates pass our validation process by running patapsco as follows on certificate and the corresponding problem instance:

patapsco.py -f INSTANCE_FILE -c CERTIFICATE_FILE --check

Certificates to improve

Scoreboard

A table with all the instances is available at lower bounds.

Below is a list of the latest most impressive improvements to the lower bounds.