A Benchmark Generator Based on Factoring for SAT and ASP Solvers

This package developed by Tuomo Pyhälä contains a generator of benchmarks for CNF / Boolean circuit SAT solvers and ASP solvers. It is able to produce hard problem instances in Smodels, DIMACS and BCSat formats. The package has been tested to work under Debian Linux operating system, but it is expected to work also under different flavors of Unix.

The benchmarks are based on the problem of factoring, i.e., finding numbers which when multiplied produce some given number. The approach here is to construct a problem instance modelling a well-known multiplier circuit with its outputs set to given values. The way to satisfy such an instance is to find a truth value assignment for the inputs such that the circuit computes the given output values. Outputs can be set to (truth values giving) a prime number (in binary encoding), corresponding an unsatisfiable instance, or to a composite number, corresponding to a satisfiable instance.

For using the package, download the source files and see the README file for further instructions.

For more detailed description of the generator see a report [PS]