On SAT Representations of XOR Constraints

  • Matthew Gwynne
  • Oliver Kullmann
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8370)


We consider the problem of finding good representations, via boolean conjunctive normal forms F (clause-sets), of systems S of XOR-constraints x 1 ⊕ … ⊕ x n  = ε, ε ∈ {0,1} (also called parity constraints), i.e., systems of linear equations over the two-element field. These representations are to be used as parts of SAT problems F * ⊃ F, such that F * has “good” properties for SAT solving. The basic quality criterion is “arc consistency”, that is, for every partial assignment φ to the variables of S, all assignments x i  = ε forced by φ are determined by unit-clause propagation on the result φ* F of the application. We show there is no arc-consistent representation of polynomial size for arbitrary S. The proof combines the basic method by Bessiere et al. 2009 ([2]) on the relation between monotone circuits and “consistency checkers”, adapted and simplified in the underlying report Gwynne et al. [10], with the lower bound on monotone circuits for monotone span programs in Babai et al. 1999 [1]. On the other side, our basic positive result is that computing an arc-consistent representation is fixed-parameter tractable in the number m of equations of S. To obtain stronger representations, instead of mere arc-consistency we consider the class \({\mathcal{PC}}\) of propagation-complete clause-sets, as introduced in Bordeaux et al. 2012 [4]. The stronger criterion is now \(F \in{\mathcal{PC}}\), which requires for all partial assignments, possibly involving also the auxiliary (new) variables in F, that forced assignments can be determined by unit-clause propagation. We analyse the basic translation, which for m = 1 lies in \({\mathcal{PC}}\), but fails badly so already for m = 2, and we show how to repair this.


arc consistency parity constraints monotone circuits monotone span programs unit-propagation complete acyclic incidence graph 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Babai, L., Gál, A., Wigderson, A.: Superpolynomial lower bounds for monotone span programs. Combinatorica 19(3), 301–319 (1999)CrossRefzbMATHMathSciNetGoogle Scholar
  2. 2.
    Bessiere, C., Katsirelos, G., Narodytska, N., Walsh, T.: Circuit complexity and decompositions of global constraints. In: Twenty-First International Joint Conference on Artificial Intelligence (IJCAI 2009), pp. 412–418 (2009)Google Scholar
  3. 3.
    Biere, A., Heule, M.J., van Maaren, H., Walsh, T.: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (February 2009)Google Scholar
  4. 4.
    Bordeaux, L., Marques-Silva, J.: Knowledge compilation with empowerment. In: Bieliková, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Turán, G. (eds.) SOFSEM 2012. LNCS, vol. 7147, pp. 612–624. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  5. 5.
    Courtois, N.T., Bard, G.V.: Algebraic cryptanalysis of the Data Encryption Standard. In: Galbraith, S.D. (ed.) Cryptography and Coding 2007. LNCS, vol. 4887, pp. 152–169. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  6. 6.
    Eén, N., Sörensson, N.: Translating pseudo-boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation 2, 1–26 (2006)zbMATHGoogle Scholar
  7. 7.
    Gent, I.P.: Arc consistency in SAT. In: van Harmelen, F. (ed.) 15th European Conference on Artificial Intelligence (ECAI 2002), pp. 121–125. IOS Press (2002)Google Scholar
  8. 8.
    Gwynne, M., Kullmann, O.: Generalising and unifying SLUR and unit-refutation completeness. In: van Emde Boas, P., Groen, F.C.A., Italiano, G.F., Nawrocki, J., Sack, H. (eds.) SOFSEM 2013. LNCS, vol. 7741, pp. 220–232. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  9. 9.
    Gwynne, M., Kullmann, O.: Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution. Journal of Automated Reasoning 52(1), 31–65 (2014), doi:10.1007/s10817-013-9275-8CrossRefMathSciNetGoogle Scholar
  10. 10.
    Gwynne, M., Kullmann, O.: On SAT representations of XOR constraints. Tech. Rep. arXiv:1309.3060v4 [cs.CC], arXiv (December 2013)Google Scholar
  11. 11.
    Gwynne, M., Kullmann, O.: Trading inference effort versus size in CNF knowledge compilation. Tech. Rep. arXiv:1310.5746v2 [cs.CC], arXiv (November 2013)Google Scholar
  12. 12.
    Haanpää, H., Järvisalo, M., Kaski, P., Niemelä, I.: Hard satisfiable clause sets for benchmarking equivalence reasoning techniques. Journal of Satisfiability, Boolean Modeling and Computation 2, 27–46 (2006)zbMATHGoogle Scholar
  13. 13.
    Kleine Büning, H., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Biere, et al. (eds.) [3], ch. 11, pp. 339–401Google Scholar
  14. 14.
    Kullmann, O.: Investigating a general hierarchy of polynomially decidable classes of CNF’s based on short tree-like resolution proofs. Tech. Rep. TR99-041, Electronic Colloquium on Computational Complexity (ECCC) (October 1999)Google Scholar
  15. 15.
    Kullmann, O.: Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems. Annals of Mathematics and Artificial Intelligence 40(3-4), 303–352 (2004)CrossRefzbMATHMathSciNetGoogle Scholar
  16. 16.
    Kullmann, O.: Hardness measures and resolution lower bounds. Tech. Rep. arXiv:1310.7627v1 [cs.CC], arXiv (October 2013)Google Scholar
  17. 17.
    Laitinen, T., Junttila, T., Niemelä, I.: Extending clause learning DPLL with parity reasoning. In: Coelho, H., Studer, R., Wooldridge, M. (eds.) ECAI 2010 – 19th European Conference on Artificial Intelligence, pp. 21–26. IOS Press (2010)Google Scholar
  18. 18.
    Laitinen, T., Junttila, T., Niemelä, I.: Equivalence class based parity reasoning with DPLL(XOR). In: ICTAI 2011 – 23rd International Conference on Tools with Artificial Intelligence, pp. 649–658 (2011)Google Scholar
  19. 19.
    Laitinen, T., Junttila, T., Niemelä, I.: Classifying and propagating parity constraints. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 357–372. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  20. 20.
    Laitinen, T., Junttila, T., Niemelä, I.: Conflict-driven XOR-clause learning. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 383–396. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  21. 21.
    Laitinen, T., Junttila, T., Niemelä, I.: Extending clause learning SAT solvers with complete parity reasoning. In: ICTAI 2012 – 24th International Conference on Tools with Artificial Intelligence, pp. 65–72 (2012)Google Scholar
  22. 22.
    Laitinen, T., Junttila, T., Niemelä, I.: Simulating parity reasoning. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 568–583. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  23. 23.
    Li, C.M.: Equivalency reasoning to solve a class of hard SAT problems. Information Processing Letters 76, 75–81 (2000)CrossRefzbMATHMathSciNetGoogle Scholar
  24. 24.
    Rossi, F., van Beek, P., Walsh, T. (eds.): Handbook of Constraint Programming. Foundations of Artificial Intelligence. Elsevier (2006)Google Scholar
  25. 25.
    Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244–257. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  26. 26.
    Tseitin, G.: On the complexity of derivation in propositional calculus. In: Seminars in Mathematics, vol. 8. V.A. Steklov Mathematical Institute, Leningrad (1968); English translation: Slisenko, A.O.(ed.) Studies in mathematics and mathematical logic, Part II, pp. 115–125 (1970)Google Scholar
  27. 27.
    Urquhart, A.: Hard examples for resolution. Journal of the ACM 34, 209–219 (1987)CrossRefzbMATHMathSciNetGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Matthew Gwynne
    • 1
  • Oliver Kullmann
    • 1
  1. 1.Computer Science DepartmentSwansea UniversityUK

Personalised recommendations