TY - GEN
T1 - Simple but hard mixed horn formulas
AU - Namasivayam, Gayathri
AU - Truszczyński, Mirosław
N1 - Copyright:
Copyright 2010 Elsevier B.V., All rights reserved.
PY - 2010
Y1 - 2010
N2 - We study simple classes of mixed Horn formulas, in which the structure of the Horn part is drastically constrained. We show that the SAT problem for formulas in these classes remains NP-complete, and demonstrate experimentally that formulas randomly generated from these classes are hard for the present SAT solvers, both complete and local-search ones.
AB - We study simple classes of mixed Horn formulas, in which the structure of the Horn part is drastically constrained. We show that the SAT problem for formulas in these classes remains NP-complete, and demonstrate experimentally that formulas randomly generated from these classes are hard for the present SAT solvers, both complete and local-search ones.
UR - https://www.scopus.com/pages/publications/77955010646
UR - https://www.scopus.com/inward/citedby.url?scp=77955010646&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-14186-7_36
DO - 10.1007/978-3-642-14186-7_36
M3 - Conference contribution
AN - SCOPUS:77955010646
SN - 3642141854
SN - 9783642141850
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 382
EP - 387
BT - Theory and Applications of Satisfiability Testing - 13th International Conference, SAT 2010, Proceedings
T2 - 13th International Conference on Theory and Applications of Satisfiability Testing, SAT 2010
Y2 - 11 July 2010 through 14 July 2010
ER -