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.
sat-to-satinstance. Currently, the shell script only works with the output of
This example describes Hamiltonian path problem using two
instances. We use
gringo/satgrnd pipeline to generate the
First the main program (
-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.
And now the internal program (
cut(Y) | -cut(X) | -hp(X,Y) :- arc(X,Y).
-cut(X) : vertex(X).
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
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
planar (available in the misc section of
Then we call
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
reason.cnf into one file
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.