The tool is a SAT solver that accepts nested SAT instances and thus goes beyond complexity class NP. While SAT-to-SAT easily accepts DIMACS input as any other SAT solver, in order to give it a nested input, you need to use the linker script provided with SAT-to-SAT.

- For the moment, we provide a proof-of-concept version of
`sat-to-sat`

(R1068). - We provide a shell script
that works in bash version 4 and higher and combines two
DIMACS files into one
`sat-to-sat`

instance. Currently, the shell script only works with the output of`satgrnd`

. - A second-order
interface
is available for an automatic generation of solvers
based on
`sat-to-sat`

. - Additionally, we provide an
implementation
of the
*stable-unstable semantics*of logic programs that has been built on top of SAT-to-SAT. For more information, on stable-unstable semantics, see the respective publication (cited below).

This example describes Hamiltonian path problem using two
instances. We use `gringo/satgrnd`

pipeline to generate the
input to `sat-to-sat`

.

First the main program (`ham-path.lp`

):

```
-hp(X,Y1) | -hp(X,Y2) :- arc(X,Y1), arc(X,Y2), Y1 < Y2.
```

-hp(X1,Y) | -hp(X2,Y) :- arc(X1,Y), arc(X2,Y), X1 < X2.

#hide.

#show -hp/2.

And now the internal program (`cut-detection.lp`

):

```
cut(0).
```

cut(Y) | -cut(X) | -hp(X,Y) :- arc(X,Y).

-cut(X) : vertex(X).

#hide.

#show cut/1.

#show -cut/1.

#show -hp_u/2.

Here, the main program selects a collection of arcs such that no two
arcs originate from the same vertex and no two arcs end in the same
vertex. The predicates related with the search part (and their
negations) are kept visible. Similarly, the internal program checks if
the SAT solver find a cut in the partially selected set of arcs? Given
that the semantics of `sat-to-sat`

is so that we are looking for a model
for the external program so that the internal program is unsatisfiable
over that model, the two programs together define the Hamiltonian path
problem.

In order to run this problem, we do as follows:

```
$ planar 100 $RANDOM > graph-100.lp
```

$ gringo ham-path.lp graph-100.lp | satgrnd > main.cnf

$ gringo cut-detection.lp graph-100.lp | satgrnd > prop.cnf

$ touch reason.cnf

$ ./link.sh main.cnf prop.cnf reason.cnf -u hp hp > ham-path.sts

$ ./sat-to-sat ham-path.sts

First, we create a random 100-vertex planar graph
using `planar`

(available in the misc section of
ASPTOOLS).
Then we call `gringo`

plus
`satgrnd`

twice to ground the main problem specification as
well as the propagator specification. We create an empty file called
`reason.cnf`

which is needed for historical reasons (and
would not be needed in future versions). We then link the three files
`main.cnf`

, `prop.cnf`

and `reason.cnf`

into one file
called `ham-path.sts`

using our the linker script. The
result is then given as input to `sat-to-sat`

for solving.

T. Janhunen, S. Tasharrofi, and E. Ternovska:
*SAT-to-SAT: Declarative
Extension of SAT Solvers with New Propagators.*
In the Proceedings of the 30th AAAI Conference
on Artificial Intelligence (AAAI-16), 978 984.
Phoenix, Arizona, February 2016. AAAI Press.

B. Bogaerts, T. Janhunen and S. Tasharrofi:
*Stable-Unstable Semantics: Beyond NP with Normal Logic Programs*,
TPLP, 2016, Special Issue on
the 32nd International Conference on Logic Programming (ICLP 2016),
in press.