In the propositional case, this study has led to discovery of polynomially solvable cases [GS88], to new algorithms for the general satisfiability problem [GP95] [P93a] and to a linear algorithm for solving the Unique Horn Satisfiability problem [P93b]. The Maximum Satisfiability problem for Horn formulas (Max Horn SAT) is currently under study [GGPR98]. Max Horn SAT is reduced to the problem of finding a minimum cardinality cut in a directed hypergraph, for which different formulations based on a cut/hyperpath duality relation are proposed. A promising enumerative method based on this approach has been devised.

In the First Order case, approaches based on a Partial Instantiation schema have been used. The idea of this schema is that of solving a First Order Satisfiability Problem, by reducing it to a possibly infinite sequence of propositional satisfiability problems. First, we have considered the case of two decidable fragments, namely the Datalog [GR90] and the Schoenfinkel-Bernays ones [GR94], and then we have extended the obtained results to the general case [HR94]. Particular attention has been given to the use of models based on hypergraphs [R94]. We have also considered the case of mathematical constraints within Datalog formulas. In this contest, an application to a particular class of crew scheduling problems has been developed [CGR93].

[GGPR98] G.Gallo, C.Gentile, D.Pretolani and G.Rago "Max Horn Sat and the Minimum Cut Problem on Directed Hypergraphs" Mathematical Programming 80, p. 213-237, 1998

[GP95] G.Gallo, D.Pretolani "A new algorithm for the propositional satisfiability problem", Discrete Applied Mathematics 60 p. 159-179, 1995

[GR94] G.Gallo and G.Rago "The satisfiability problem for the Schoenfinkel-Bernays fragment: Partial Instantiation and Hypergraph Algorithms" TR 4/94, Dip. di Informatica, Univ. di Pisa, 1994

[HR94] J.Hooker, G.Rago, "Partial Instantiation Methods for Logic Programming" Working paper, 1994

[R94] G.Rago "Optimization, Hypergraphs and Logical Inference", TD 4/94, PhD Dissertation, Dip. di Informatica, Univ. di Pisa, 1994

[CGR93] P.Carraresi, G.Gallo and G.Rago "A hypergraph model for constraint logic programming and applications to bus drivers' scheduling", Annals on Mathematics and Artificial Intelligence 8, p. 247-270, 1993

[P93a] D.Pretolani "Satisfiability and Hypergraphs" Ph.D. Dissertation TD 12/93, Dip. di Informatica, Univ. di Pisa, 1993

[P93b] D. Pretolani "A linear time algorithm for unique Horn satisfiability", Information Processing Letters 48, p. 61-66, 1993

[GR90] G.Gallo, G.Rago "A hypergraph approach to logical inference for datalog formulae", TR 28/90, Dip. di Informatica, Univ. di Pisa, 1990

[GS88] G.Gallo, M.G.Scutellá "Polynomially solvable satisfiability problems" Information Processing Letters 29 p. 221-227, 1988