Cardinality Networks: a theoretical and empirical study

1. Anbulagan, & Grastien, A. (2009). Importance of variables semantic in CNF encoding of cardinality constraints. In V. Bulitko, & J. C. Beck (Eds.), Eighth symposium on abstraction, reformulation, and approximation, SARA’09. Menlo Park: AAAI.

   Google Scholar 

2. Bailleux, O., & Boufkhad, Y. (2003). Efficient CNF encoding of Boolean cardinality constraints. In F. Rossi (Ed.), Principles and practice of constraint programming, 9th international conference, CP’03. Lecture notes in computer science (Vol. 2833, pp. 108–122). New York: Springer.

   Google Scholar 

3. Bailleux, O., Boufkhad, Y., & Roussel, O. (2006). A translation of pseudo Boolean constraints to SAT. Journal on Satisfiability, Boolean Modeling and Computation, JSAT, 2(1–4), 191–200.

   MATH  Google Scholar 

4. Bailleux, O., Boufkhad, Y., & Roussel, O. (2009). New encodings of pseudo-Boolean constraints into CNF. In O. Kullmann (Ed.), 12th international conference on theory and applications of satisfiability testing, SAT’09. Lecture notes in computer science (Vol. 5584, pp. 181–194). New York: Springer.

   Chapter  Google Scholar 

5. Batcher, K. E. (1968). Sorting networks and their applications. In AFIPS spring joint computing conference (pp. 307–314).

6. Biere, A. (2010). Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Technical report, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria, 2010. Technical report 10/1, August 2010, FMV Reports Series.

7. Büttner, M., & Rintanen, J. (2005). Satisfiability planning with constraints on the number of actions. In S. Biundo, K. L. Myers, & K. Rajan (Eds.), 15th international conference on automated planning and scheduling, ICAPS’05 (pp. 292–299). Menlo Park: AAAI.

   Google Scholar 

8. Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem-proving. Communications of the ACM, CACM, 5(7), 394–397.

   Article  MATH  MathSciNet  Google Scholar 

9. Eén, N., & Biere, A. (2005). Effective preprocessing in SAT through variable and clause elimination. In F. Bacchus, & T. Walsh (Eds.), 8th international conference on theory and applications of satisfiability testing, SAT’05. Lecture notes in computer science (Vol. 3569, pp. 61–75). New York: Springer.

   Google Scholar 

10. Eén, N., & Sörensson, N. (2006). Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2, 1–26.

    MATH  Google Scholar 

11. Marques-Silva, J., & Planes, J. (2008). Algorithms for maximum satisfiability using unsatisfiable cores. In 2008 conference on design, automation and test in Europe conference, DATE’08 (pp. 408–413). Los Alamitos: IEEE Computer Society.

    Chapter  Google Scholar 

12. Marques-Silva, J. P., & Lynce, I. (2007). Towards robust cnf encodings of cardinality constraints. In C. Bessiere (Ed.), Principles and practice of constraint programming, 13th international conference, CP’07. Lecture notes in computer science (Vol. 4741, pp. 483–497). New York: Springer.

    Google Scholar 

13. Nieuwenhuis, R., Oliveras, A., & Tinelli, C. (2006). Solving SAT and SAT modulo theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). Journal of the ACM, JACM, 53(6), 937–977.

    Article  MathSciNet  Google Scholar 

14. Sinz, C. (2005). Towards an optimal CNF encoding of boolean cardinality constraints. In P. v. Beek (Ed.), Principles and practice of constraint programming, 11th international conference, CP’05. Lecture notes in computer science (Vol. 3709, pp. 827–831). New York: Springer.

    Chapter  Google Scholar 

15. Warners, J. P. (1998). A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters, 68(2), 63–69.

    Article  MathSciNet  Google Scholar 

Download references