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.