Exploration of Hard to Solve 3-sat Problems

Robert Amador, Chen-Fu Chiang and Chang-Yu Hsieh

Abstract


We designed and implemented an efficient tough random symmetric 3-SAT generator and propose two deterministic algorithms that efficiently generate 3-SAT instances with a unique solution. We quantify the first algorithms hardness in terms of CPU time, numbers of restarts, decisions, propagations, conflicts and conflicted literals that occur when a solver tries to solve 3-SAT instances. In this experiment, the clause variable ratio was chosen to be around the conventional critical phase transition number 4.24. The experiment shows that instances generated by our generator are significantly harder than instances generated by the Tough K-SAT generator. The two deterministic algorithms generate 3-SAT instances with the number of clauses scaling as 4n, where n is the number of variables, and (n+6), respectively. By combining these two algorithms along with a simple padding algorithm, we prove a hybrid algorithm that can generate n-variable instances with the number of clauses that scale between (n+6) and 7n(n-1)(n-2). Overall, all proposed SAT generators seek to explore unique difficult to solve SAT problems.

Keywords


3-SAT, Satisfiability, Efficient Tough Random Symmetric 3-SAT Generator, Tunable Unique-Solution, Critical Phase Transition

References


S. A. Cook, “The complexity of theorem-proving procedures,” in Proceedings of the third annual ACM symposium on Theory of computing, 1971.

R. M. Karp, “Reducibility among combinatorial problems,” in Complexity of computer computations, Springer, 1972, pp. 85-103.

C. H. Papadimitriou and M. Yannakakis, “Optimization, approximation, and complexity classes,” Journal of computer and system sciences, vol. 43, pp. 425-440, 1991.

R. Marino, G. Parisi and F. Ricci-Tersenghi, “The backtracking survey propagation algorithm for solving random K-SAT problems,” Nature communications, vol. 7, p. 12996, 2016.

S. Cocco and R. Monasson, “Statistical physics analysis of the computational complexity of solving random satisfiability problems using backtrack algorithms,” The European Physical Journal BCondensed Matter and Complex Systems, vol. 22, pp. 505-531, 2001.

A. Percus, G. Istrate and C. Moore, Computational complexity and statistical physics, OUP USA, 2006.

B. A. Huberman and T. Hogg, “Phase transitions in artificial intelligence systems,” Artificial Intelligence, vol. 33, pp. 155-171, 1987.

M. Mézard, G. Parisi and R. Zecchina, “Analytic and algorithmic solution of random satisfiability problems,” Science, vol. 297, pp. 812- 815, 2002.

M. Žnidarič, “Scaling of the running time of the quantum adiabatic algorithm for propositional satisfiability,” Physical Review A, vol. 71, p. 062305, 2005.

A. Aspuru-Guzik, A. D. Dutoi, P. J. Love and M. Head-Gordon, “Simulated quantum computation of molecular energies,” Science, vol. 309, no. 5741, pp. 1704-1707, 2005.

S. Boixo, V. N. Smelyanskiy, A. Shabani, S. V. Isakov, M. Dykman, V. S. Denchev, M. H. Amin, A. Y. Smirnov, M. Mohseni and H. Neven, “Computational multiqubit tunnelling in programmable quantum annealers,” Nature Communications, vol. 7, 2016.

B. Berger and T. Leighton, “Protein folding in the hydrophobichydrophilic (HP) model is NP-complete,” Journal of Computational Biology, vol. 5, no. 1, pp. 27-40, 1998.

M. Motoki and R. Uehara, “Unique solution instance generation for the 3-Satisfiability (3SAT) problem,” SAT, pp. 293-305, 2000.

https://toughsat.appspot.com/, “Tough SAT generation,” 2017.

N. Een, “MiniSat: A SAT solver with conflict-clause minimization,” in Proc. SAT-05: 8th International Conference on Theory and Applications of Satisfiability Testing, 2005.

N. Eén and A. Biere, “Effective preprocessing in SAT through variable and clause elimination,” in International conference on theory and applications of satisfiability testing, 2005.


Full Text: PDF

Refbacks

  • There are currently no refbacks.


Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 License.

IT in Innovation IT in Business IT in Engineering IT in Health IT in Science IT in Design IT in Fashion

IT in Industry @ http://www.it-in-industry.com . ISSN (Online): 2203-1731; ISSN (Print): 2204-0595