We present a novel encoding of modal satisfiability problems as Constraint Satisfaction Problems. We allow the domains of the resulting constraints to contain other values than just the Boolean $0$ or $1$, and add various constraints to reason about these values. This modelling is pivotal to speeding up the performance of our constraint-based procedure for modal satisfiability in Constraint Logic Programming (CLP). Our encoding results in a correct solver that attempts to minimize the size of the tree model that it is implicitly trying to generate. An important advantage of our modelling is that we do not need to change the underlying CSP algorithms, and can use them almost as `black boxes`

Finite CSP solvers for modal satisfiability

Gennari, Rosella;
2003-01-01

Abstract

We present a novel encoding of modal satisfiability problems as Constraint Satisfaction Problems. We allow the domains of the resulting constraints to contain other values than just the Boolean $0$ or $1$, and add various constraints to reason about these values. This modelling is pivotal to speeding up the performance of our constraint-based procedure for modal satisfiability in Constraint Logic Programming (CLP). Our encoding results in a correct solver that attempts to minimize the size of the tree model that it is implicitly trying to generate. An important advantage of our modelling is that we do not need to change the underlying CSP algorithms, and can use them almost as `black boxes`
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/2055
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact