## SAT-to-SAT

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.

## Implementation

• 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).

## Simple Example

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.

## Related Publications

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.