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:

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.