Finding Efficient Circuits Using SAT-solvers

Usage

python3 circuit2sat.py n r truthtable1 ... truthtablem

Here, n is the number of inputs of the function, r is the number of gates, m is the number of outputs (hence, truthtablei is a bit-string of length 2^n).

The script uses the minisat SAT-solver and assumes that there is an executable file minisat_static in the same folder.

For using other SAT-solvers, either adjust the line

os.system("./minisat_static tmp.cnf tmp.sat")

of the script or simply run your favourite SAT-solver on the CNF-formula tmp.cnf generated by the script.

Reduction

The reduction to CNF-SAT is described in [Kojevnikov, Kulikov, Yaroslavtsev. Finding Efficient Circuits Using SAT-Solvers. SAT 2009. (DOI)]. See also [D. E. Knuth, The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability, 1st ed. Addison-Wesley Professional, 2015. (Solution to exercise 477)] An implementation of the reduction by Knuth is available at http://www-cs-faculty.stanford.edu/∼knuth/programs.html (sat-chains.w file in SATexamples archive).

Open Problems

In this section, we describe a few CNF formulas. Each formula if satisfiable will give a new upper bound on circuit complexity of a certain symmetric function.

• The script openproblems/m3v4g11.py generates a CNF formula with 1831 variables and 642938 clauses. Most probably, it is unsatisfiable. But if it is satisfiable, then C(MOD_3) <= 2.75n+O(1).
• The script openproblems/m5v2g8.py generates a CNF formula with 797 variables and 3M clauses. If satisfiable, then CMOD(MOD_5) <= 4n+O(1).