Second-order Interface for SAT-to-SAT

We provide a high-level (second-order) interface to sat-to-sat in order to relieve users of manually encoding sat-to-sat instances.

Input Language

The language of this interface is closely related to the IDP language, i.e., it is an ASCII representation of second-order theories (see the table below for logical connectives available).

Logic	SAT-to-SAT
∀	!
∃	?
∧	&
∨	|
⇒	=>
⇐	<=
⇔	<=>
¬	~

For example, an expression of the form

! X: in_node(X) => reach(X).

expresses that each node must be reachable. Furthermore, our tool (currently) makes the following assumptions about the input:

1. The names of predicates start with a lower case letter whereas the names of first-order variables with an upper case letter.
2. All predicates that will be interpreted in instance files start with the prefix "in_".
3. All variables that are not input predicates must be quantified.
4. Quantifications of first-order variables must be safe, in the sense that the scope of each quantification over such a variable must be bound by an input predicate. For example, expressions of the form
   !X: reach(X).
   are considered unsafe, while expressions of the forms
   ! X: in_node(X) => reach(X).
! X: ~in_node(X) | reach(X).
! X: reach(X) | ~in_node(X).
   are safe since in each of these expressions, the quantification over variable X is bound by the input-predicate in_node/1.
5. All sentences must end with a dot ".".

Usage

The tool so2grounder (R1068, available here for download) takes two arguments as input:

1. The first is a file containing a second-order specification.
2. The second is a directory in which so2grounder can write auxiliary files and output files.

For instance, so2grounder can be called as follows:

$ so2grounder instances/argumentation/DC-CO ./my_dir

This will create several files in the directory my_dir. One of those files is called "run.sh". The tool so2grounder creates a grounder that transforms an instance into a SAT-to-SAT specification. Hence, in order to actually do something with the output of so2grounder, we need an instance file that consists of a set of facts (logic programming-style) interpreting all input-predicates. I.e., a set of facts of the form

in_pred(args).

Generating the actual SAT-to-SAT instance is done by the following command

bash my_dir/run.sh link.sh instance.lp

where:

• my_dir is the directory you used in so2grounder
• link.sh is the SAT-to-SAT linker script that can be downloaded here
• instance.lp is the instance file

This step assumes that gringo and satgrnd are available somewhere in your path. The output of this command can be piped directly to sat-to-sat.

Examples

We provide some example files for the second-order interface of SAT-to-SAT.

• This archive contains 16 different files that correspond to 16 difference inference tasks in abstract argumentation frameworks. See here for more information on these inference tasks. Additionally, a script can be used to transform the actual input files from the argumentation competition into valid input for our tool.