Sat Approach For Maximizing Satisfiability In Qualitative Spatial And Temporal Constraint Networks

In this paper, we focus on a recently introduced problem in the context of spatial and temporal qualitative reasoning, called the MAX-QCN problem. This problem involves obtaining a spatial or temporal configuration that maximizes the number of satisfied constraints in a qualitative constraint network (QCN). To efficiently solve the MAX-QCN problem, we introduce and study two families of encodings of the partial maximum satisfiability problem (PMAX-SAT). Each of these encodings is based on, what we call, a forbidden covering with regard to the composition table of the considered qualitative calculus. Intuitively, a forbidden covering allows us to express, in a more or less compact manner, the nonfeasible configurations for three spatial or temporal entities. The experimentation that we have conducted with qualitative constraint networks from the Interval Algebra shows the interest of our approach.