[SMT-LIB] Extracting UTVPI Constraint Systems from SMT-LIB Benchmarks

[Zachary Santer]

Everyone, thank you for your suggestions.

Tim, yes, I am interested in conjunctions of UTVPI literals. Attached is an
example input file that my implementations can handle. Basically, just a
line to tell the solver how many variables to allocate space for; followed
by simple constraint equations, one per line; and C-style line and block
comments.

What I'm attempting to test with these implementations is simply their
running times and memory requirements. As such, large sets of constraints
are the most useful. Random constraint systems generated for this purpose
include systems with 1000 variables, and modulating the number of
constraints from 10000 to 200000; and systems with 100000 constraints, and
modulating the number of variables from 1000 to 20000. I assume such large
systems rarely occur naturally.

Any real-world source of UTVPI constraint systems, UTVPI subsets of other
systems included, would be useful.

The difference constraints contained in QF_IDL would likely be solved more
efficiently by more specialized difference constraint system solvers,
though I suppose they are still useful for my purposes. I assume filtering
non-UTVPI constraints out of QF_LIA benchmarks wouldn't add much work to
the overall task.

Thank you,
Zachary

On Mon, Jan 23, 2017 at 12:53 PM, Tim King <taking at google.com> wrote:

> Dear Zachary,
>
> Are you interested in extracting a set of UTVPI literals or extracting the
> original problem over UTVPI literals including the input propositional
> structure? If it is the latter, Dejan and Alerbto's suggestions are both
> really good.
>
> Given how you phrased this, I am guessing you want a set of literals. If
> so, what kinds of sets of literals are you interested in? Does this only
> include input problems that happen to already be equivalent to a set of
> literals? Or is the UTVPI subset of literals that are sent to a theory
> solver in a DPLL(T) combination interesting enough? There are a couple of
> other possible choices. It all depends on what you want to be testing.
>
> -Tim
>
> PS. Look into QF_IDL. Those are guaranteed to be translatable into UTVPI.
> For QF_LIA, you'll need to implement a filter of some kind.
>
> On Mon, Jan 23, 2017 at 12:32 AM Alberto Griggio <griggio at fbk.eu> wrote:
>
>> Dear Zachary,
>>
>> > I have implemented two algorithms for solving Unit Two Variable per
>> > Inequality (+/- x_i {+/- x_j} <= c, c ϵ Z) constraint systems, for the
>> > purposes of comparing them against one another empirically.
>> >
>> > I designed a simple input file format that would allow UTVPI constraint
>> > equations to be written normally, mainly for ease of testing. This
>> format
>> > also required minimal modifications to UTVPI constraint system files
>> > generated by a random generator provided by Dr. Peter Stuckey.
>> >
>> > I am interested in testing with real-world UTVPI constraint systems.
>> > However, I have struggled to find a source for such systems. It has been
>> > recommended that I extract the subset of systems within the QF_LIA
>> > benchmarks that are purely UTVPI.
>> >
>> > Even given the SMT-LIB 2 Lexer/Parser
>> > <https://es-static.fbk.eu/people/griggio/misc/smtlib2parser.html>
>> linked in
>> > the site, this appears to be a rather daunting task.
>> >
>> > Any guidance would be appreciated.
>>
>> I would not recommend that parser, in fact. It was meant more for solver
>> developers than for users, and it is way overkill for the task you want
>> to solve.
>>
>> Besides what Dejan said, I think you can take a look at pySMT
>> (www.pysmt.org), which offers many shortcuts that should let you write a
>> translator in a few lines of Python code.
>>
>> Alberto
>> _______________________________________________
>> SMT-LIB mailing list
>> SMT-LIB at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>>
>
-------------- next part --------------
/*
 * swtest5.txt
 * From Piotr's paper
 * Example 11, pg 17
 * Infeasible system
 */

4 variables
x1 - x2 <= -3
-x1 + x2 <= 4
-x1 + x4 <= 1
-x1 - x4 <= 1
x2 + x3 <= 1
x2 - x3 <= 1