A SAT Benchmark Suite for LTL Specification Sketching

LTL_Sketcher-SAT_Benchmark

This repository contains a set of formulas in Propositional Boolean Logic.These formulas are generated during the execution of our LTLSketcher tool.Given an LTL sketch (i.e., a partial LTL formula) and a sample (i.e., a set of program executions labeled desired and undesired), the tool solves the LTL sketching problem, i.e., complete the sketch to a specification consistent with the data. (feel freet to check out our paper for more information on this problem)In essence, this is done by reducing the problem to a series of formulas in Propositional Boolean Logic and checking their satisfiability.

Naming convention:

This repository contains each formula both in the DIMACS and SMTLib format.Each file follows the same naming convention:

type__sample-file__sketch__size__algorithm-configuration__satisifability

type: indicates whether the formula is stored in the DIMACS or SMTLib formatsample-file: refers to the sample (cf., here) used by the LTLSketcher toolsketch: refers to the sketch (cf., See experimental evaluation of our paper) used by the LTLSketcher toolsize: refers to the size of the complete solution (i.e., the number of subformulas of the complete specification)algorithm-configuration: our algorithm can be extended by two heuristics (BMC and suffix), this indicates which combination of heuristics was used (none, either one of the two, both)satisfiability: indicates whether the formula is satisfiable or not