Abstract
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.
A version of this paper extended with proofs is available at http://www.lsi.upc.edu/ ~erodri/lpar16ex.pdf
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aji, S., McEliece, R.: The generalized distributive law. IEEE Trans. on Information Theory 46(2), 325–343 (2000)
Bacchus, F., Dalmao, S., Pitassi, T.: Algorithms and complexity results for #SAT and Bayesian inference. In: FOCS, pp. 340–351 (2003)
Bertele, U., Brioschi, F.: Nonserial Dynamic Programming. Academic Press, London (1972)
Birnbaum, E., Lozinskii, E.: The good old Davis-Putnam procedure helps counting models. JAIR 10, 457–477 (1999)
Bistarelli, S., Montanari, U., Rossi, F.: Semiring-based constraint satisfaction and optimization. JACM 44(2), 201–236 (1997)
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)
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)
Cooper, M., Schiex, T.: Arc consistency for soft constraints. Artif. Intell. 154(1-2), 199–227 (2004)
Crama, Y., Hansen, P., Jaumard, B.: The basic algorithm for pseudo-boolean programming revisited. Discrete Applied Mathmatics 29, 171–185 (1990)
Davis, M., Logemann, G., Loveland, G.: A machine program for theorem proving. Communications of the ACM 5, 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. JACM 3 (1960)
Dechter, R., Pearl, J.: Network-based heuristics for constraint-satisfaction problems. Artif. Intell. 34, 1–38 (1988)
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)
Gavanelli, M.: An algorithm for multi-criteria optimization in CSPs. In: ECAI, pp. 136–140 (2002)
Golan, J.: Semirings and their applications. Kluwer Academic Publishers, Dordrecht (1999)
Heras, F., Larrosa, J., Oliveras, A.: MiniMaxSAT: An efficient Weighted Max-SAT Solver. JAIR 31, 1–32 (2008)
Bayardo, R., Pehoushek, J.: Counting models using connected components. In: AAAI/IAAI, pp. 157–162 (2000)
Kindermann, R., Snell, L.: Markov Random Fields and Their Applications. AMS, Providence (1980)
Kohlas, J., Wilson, N.: Semiring induced valuation algebras: Exact and approximate local computation algorithms. Artif. Intell. 172(11), 1360–1399 (2008)
Larrosa, J., Heras, F., de Givry, S.: A logical approach to efficient Max-SAT solving. Artif. Intell. 172(2-3), 204–233 (2008)
Li, C., Manyà, F., Planes, J.: New inference rules for Max-SAT. JAIR 30, 321–359 (2007)
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)
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)
Papadimitriou, C.: Computational Complexity. Addison-Wesley, USA (1994)
Park, J.: Using weighted Max-SAT engines to solve MPE. In: AAAI 2002, pp. 682–687 (2002)
Pearl, J.: Probabilistic Inference in Intelligent Systems. Networks of Plausible Inference. Morgan Kaufmann, San Mateo (1988)
Schiex, T., Fargier, H., Verfaillie, G.: Valued constraint satisfaction problems: hard and easy problems. In: IJCAI 1995, pp. 631–637 (1995)
Shafer, G.R., Shenoy, P.P.: Probability propagation. Anals of Mathematics and Artificial Intelligence 2, 327–352 (1990)
Shenoy, P., Shafer, G.: Axioms for probability and belief-function propagation. In: UAI 1988 (1988)
Xing, Z., Zhang, W.: Maxsolver: An efficient exact algorithm for (weighted) maximum satisfiability. Artif. Intell. 164(1-2), 47–80 (2005)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Larrosa, J., Oliveras, A., Rodríguez-Carbonell, E. (2010). Semiring-Induced Propositional Logic: Definition and Basic Algorithms. In: Clarke, E.M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science(), vol 6355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17511-4_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-17511-4_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17510-7
Online ISBN: 978-3-642-17511-4
eBook Packages: Computer ScienceComputer Science (R0)