Satisfiability problem is the task to establish either a given CNF logical formula admits a model or not. It is known to be the canonical NP-complete problem. We study in this note the relationship between matchings in bipartite graphs and the satisfiability problem, and prove that some restrictions of formulae including the known r-r-SAT1 class are trivially satisfiable. We present an algorithm which finds a model for such formulas in polynomial time complexity if one exists or, failing this, proves in polynomial time complexity that the current formula is not an element of the restricted class.
El problema de la satisfacibilidad consiste en establecer si una fórmula lógica CNF dada admite o no un modelo. Se conoce como el problema canónico NP completo. En este trabajo se estudia la relación entre la equiparación en grafos bipartitos y el problema de la satisfacibilidad y se demuestra que algunas restricciones de las fórmulas, entre ellas la clase conocida r-r-SAT, son satisfacibles de forma trivial. Se presenta un algoritmo que encuentra, si existe, un modelo para tales fórmulas en tiempo polinomial y, en su defecto, demuestra, también en tiempo polinomial, que la fórmula actual no es un elemento de la clase restringida.
@article{urn:eudml:doc:41035,
title = {Satisfiability and matchings in bipartite graphs: relationship and tractability.},
journal = {RACSAM},
volume = {98},
year = {2004},
pages = {55-63},
zbl = {1103.68805},
language = {en},
url = {http://dml.mathdoc.fr/item/urn:eudml:doc:41035}
}
Benhamou, Belaid. Satisfiability and matchings in bipartite graphs: relationship and tractability.. RACSAM, Tome 98 (2004) pp. 55-63. http://gdmltest.u-ga.fr/item/urn:eudml:doc:41035/