Stronger Inference through Implied Literals from Conflicts and Knapsack Covers

  • Tobias Achterberg
  • Ashish Sabharwal
  • Horst Samulowitz
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7874)


Implied literals detection has been shown to improve performance of Boolean satisfiability (SAT) solvers for certain problem classes, in particular when applied in an efficient dynamic manner on learned clauses derived from conflicts during backtracking search. We explore this technique further and extend it to mixed integer linear programs (MIPs) in the context of conflict constraints. This results in stronger inference from clique tables and implication tables already commonly maintained by MIP solvers. Further, we extend the technique to knapsack covers and propose an efficient implementation. Our experiments show that implied literals, in particular through stronger inference from knapsack covers, improve the performance of the MIP engine of IBM ILOG CPLEX Optimization Studio 12.5, especially on harder instances.


Mixed Integer Programming Mixed Integer Linear Program Mixed Integer Programming Model Strong Inference Hard Instance 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Achterberg, T.: Conflict analysis in mixed integer programming. Discrete Optimization 4(1), 4–20 (2007); Special issue: Mixed Integer ProgrammingGoogle Scholar
  2. 2.
    Achterberg, T.: Constraint Integer Programming. PhD thesis, Technische Universität Berlin (July 2007)Google Scholar
  3. 3.
    Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: 21st IJCAI, Pasadena, CA, pp. 399–404 (July 2009)Google Scholar
  4. 4.
    Bacchus, F., Biere, A., Heule, M.: Personal Communication (2012)Google Scholar
  5. 5.
    Freeman, J.: Improvements to Propositional Satisfiability Search Algorithms. PhD thesis, University of Pennsylvania (1995)Google Scholar
  6. 6.
    Heule, M.J.H., Järvisalo, M., Biere, A.: Efficient CNF simplification based on binary implication graphs. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 201–215. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  7. 7.
    Koch, T., Achterberg, T., Andersen, E., Bastert, O., Berthold, T., Bixby, R.E., Danna, E., Gamrath, G., Gleixner, A.M., Heinz, S., Lodi, A., Mittelmann, H., Ralphs, T., Salvagnin, D., Steffy, D.E., Wolter, K.: MIPLIB 2010. Mathematical Programming Computation 3, 103–163 (2011)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Lynce, I., Marques-Silva, J.: Probing-based preprocessing techniques for propositional satisfiability. In: 15th ICTAI, Sacramento, CA, pp. 105–111 (November 2003)Google Scholar
  9. 9.
    Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions of Computers 48, 506–521 (1999)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Matsliah, A., Sabharwal, A., Samulowitz, H.: Augmenting clause learning with implied literals. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 500–501. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  11. 11.
    Savelsbergh, M.W.P.: Preprocessing and probing techniques for mixed integer programming problems. ORSA Journal on Computing 6, 445–454 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  12. 12.
    Soos, M.: CryptoMiniSat 2.9.x (2011),

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Tobias Achterberg
    • 1
  • Ashish Sabharwal
    • 2
  • Horst Samulowitz
    • 2
  1. 1.IBMGermany
  2. 2.IBM Watson Research CenterYorktown HeightsUSA

Personalised recommendations