Semiring-Induced Propositional Logic: Definition and Basic Algorithms

  • Javier Larrosa
  • Albert Oliveras
  • Enric Rodríguez-Carbonell
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6355)


In this paper we introduce an extension of propositional logic that allows clauses to be weighted with values from a generic semiring. The main interest of this extension is that different instantiations of the semiring model different interesting computational problems such as finding a model, counting the number of models, finding the best model with respect to an objective function, finding the best model with respect to several independent objective functions, or finding the set of pareto-optimal models with respect to several objective functions.

Then we show that this framework unifies several solving techniques and, even more importantly, rephrases them from an algorithmic language to a logical language. As a result, several solving techniques can be trivially and elegantly transferred from one computational problem to another. As an example, we extend the basic DPLL algorithm to our framework producing an algorithm that we call SDPLL. Then we enhance the basic SDPLL in order to incorporate the three features that are common in all modern SAT solvers: backjumping, learning and restarts.

As a result, we obtain an extremely simple algorithm that captures, unifies and extends in a well-defined logical language several techniques that are valid for arbitrary semirings.


semiring marginalization problem DPLL 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aji, S., McEliece, R.: The generalized distributive law. IEEE Trans. on Information Theory 46(2), 325–343 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Bacchus, F., Dalmao, S., Pitassi, T.: Algorithms and complexity results for #SAT and Bayesian inference. In: FOCS, pp. 340–351 (2003)Google Scholar
  3. 3.
    Bertele, U., Brioschi, F.: Nonserial Dynamic Programming. Academic Press, London (1972)zbMATHGoogle Scholar
  4. 4.
    Birnbaum, E., Lozinskii, E.: The good old Davis-Putnam procedure helps counting models. JAIR 10, 457–477 (1999)MathSciNetzbMATHGoogle Scholar
  5. 5.
    Bistarelli, S., Montanari, U., Rossi, F.: Semiring-based constraint satisfaction and optimization. JACM 44(2), 201–236 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Bistarelli, S., Gadducci, M., Larrosa, J., Rollon, E.: A semiring-based approach to multi-objective optimization. In: Proc. of Intl. Workshop on Soft Constraints and Preferences (2008)Google Scholar
  7. 7.
    Borchers, B., Furman, J.: A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems. Journal of Combinatorial Optimization 2, 299–306 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Cooper, M., Schiex, T.: Arc consistency for soft constraints. Artif. Intell. 154(1-2), 199–227 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Crama, Y., Hansen, P., Jaumard, B.: The basic algorithm for pseudo-boolean programming revisited. Discrete Applied Mathmatics 29, 171–185 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Davis, M., Logemann, G., Loveland, G.: A machine program for theorem proving. Communications of the ACM 5, 394–397 (1962)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Davis, M., Putnam, H.: A computing procedure for quantification theory. JACM 3 (1960)Google Scholar
  12. 12.
    Dechter, R., Pearl, J.: Network-based heuristics for constraint-satisfaction problems. Artif. Intell. 34, 1–38 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Fu, Z., Malik, S.: On solving the partial Max-SAT problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 252–265. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  14. 14.
    Gavanelli, M.: An algorithm for multi-criteria optimization in CSPs. In: ECAI, pp. 136–140 (2002)Google Scholar
  15. 15.
    Golan, J.: Semirings and their applications. Kluwer Academic Publishers, Dordrecht (1999)CrossRefzbMATHGoogle Scholar
  16. 16.
    Heras, F., Larrosa, J., Oliveras, A.: MiniMaxSAT: An efficient Weighted Max-SAT Solver. JAIR 31, 1–32 (2008)MathSciNetzbMATHGoogle Scholar
  17. 17.
    Bayardo, R., Pehoushek, J.: Counting models using connected components. In: AAAI/IAAI, pp. 157–162 (2000)Google Scholar
  18. 18.
    Kindermann, R., Snell, L.: Markov Random Fields and Their Applications. AMS, Providence (1980)CrossRefzbMATHGoogle Scholar
  19. 19.
    Kohlas, J., Wilson, N.: Semiring induced valuation algebras: Exact and approximate local computation algorithms. Artif. Intell. 172(11), 1360–1399 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Larrosa, J., Heras, F., de Givry, S.: A logical approach to efficient Max-SAT solving. Artif. Intell. 172(2-3), 204–233 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Li, C., Manyà, F., Planes, J.: New inference rules for Max-SAT. JAIR 30, 321–359 (2007)MathSciNetzbMATHGoogle Scholar
  22. 22.
    Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC 2001, pp. 530–535. ACM Press, New York (2001)Google Scholar
  23. 23.
    Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL. JACM 53(6), 937–977 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Papadimitriou, C.: Computational Complexity. Addison-Wesley, USA (1994)zbMATHGoogle Scholar
  25. 25.
    Park, J.: Using weighted Max-SAT engines to solve MPE. In: AAAI 2002, pp. 682–687 (2002)Google Scholar
  26. 26.
    Pearl, J.: Probabilistic Inference in Intelligent Systems. Networks of Plausible Inference. Morgan Kaufmann, San Mateo (1988)zbMATHGoogle Scholar
  27. 27.
    Schiex, T., Fargier, H., Verfaillie, G.: Valued constraint satisfaction problems: hard and easy problems. In: IJCAI 1995, pp. 631–637 (1995)Google Scholar
  28. 28.
    Shafer, G.R., Shenoy, P.P.: Probability propagation. Anals of Mathematics and Artificial Intelligence 2, 327–352 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  29. 29.
    Shenoy, P., Shafer, G.: Axioms for probability and belief-function propagation. In: UAI 1988 (1988)Google Scholar
  30. 30.
    Xing, Z., Zhang, W.: Maxsolver: An efficient exact algorithm for (weighted) maximum satisfiability. Artif. Intell. 164(1-2), 47–80 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient Conflict Driven Learning in a Boolean Satisfiability Solver. In: ICCAD 2001, pp. 279–285 (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Javier Larrosa
    • 1
  • Albert Oliveras
    • 1
  • Enric Rodríguez-Carbonell
    • 1
  1. 1.Technical University of CataloniaBarcelonaSpain

Personalised recommendations