1,721,076 research outputs found
Integrating SAT Solvers with Math Reasoners: Foundations and Basic Algorithms
No full textIn the last years we have witnessed an impressive advance in the efficiency of SAT techniques, which has brought large previously intractable problems at the reach of state-of-the-art solvers. Unfortunately, simple boolean expressions are not expressive enough for representing many real-world problems, which require handling also integer or real values and operators. On the other hand, mathematical reasoners, like computer-algebra
systems or constraint solvers, cannot handle efficiently problems involving heavy boolean search, or do not handle them at all.
In this paper we present the foundations and the basic algorithms for a new class of procedures for solving boolean combinations of mathematical propositions, which combine SAT solvers and mathematical reasoner
Building Decision Procedures for Modal Logics from Propositional Decision Procedures: The Case Study of Modal K(m)
No full textAbstractThe goal of this paper is to propose a new technique for developing decision procedures for propositional modal logics. The basic idea is that propositional modal decision procedures should be developed on top of propositional decision procedures. As a case study, we consider satisfiability in modal K(m), that is modal K with m modalities, and develop an algorithm, called KSAT, on top of an implementation of the Davis–Putnam–Longemann–Loveland procedure. KSAT is thoroughly tested and compared with various procedures and in particular with the state-of-the-art tableau-based system KRIS. The experimental results show that KSAT outperforms KRIS and the other systems of orders of magnitude, highlight an intrinsic weakness of tableau-based decision procedures, and provide partial evidence of a phase transition phenomenon for K(m)
Servizi forniti dagli strati Safety Layer e Connection Manager
No full textObiettivo del presente documento è fornire una (proposta preliminare di) descrizione dei servizi forniti agli applicativi dagli strati Connection Manager (CM) e Safety Layer (SL), come perzialmente descritto nei documenti (1) e (3). Tale proposta è risultante della riunione in Ansaldo del 08-05-98 tra Ansaldo e Irs
Protocolli Safety Layer e Connection Manager: Descrizione del Codice SDL
No full textNel presente documento viene descritto in dettaglio il codice SDL della specifica formale dei protocolli Safety Layer (SL) e Connection Manager (CM) descritta in (1).
Il modello è realizzato attraverso i meccanismi di 'definizione di tipo' e di 'istanziazione' di SDL. Il codice è ripartito nei fine terminale_lib.pr, contenente la descrizione dei tipi (es. macchina SL, macchina CM), e Modello.pr, contentenente le istanze che realizzano la particolare configurazione analizzata
Il presente documento assume che il lettore abbia una certa conoscenza di SDL, e fa esplicito riferimento al listato dei file Modello.pr e terminale_lib.pr allegato
Specifica formale dei protocolli Safety Layer e Connection Manager
No full textIl presente documento descrive una specifica formale del protocollo di comunicazione tra applicativi in sicurezza basato su ridondanza. Il protocollo è stato suddiviso in due livelli separati, il Safety Layer (SL), come parzialmente descritto nei documenti (1) e (3), ed il Connection Manager (CM). Il S: e il CM sono stati specificati formalmente in SDL, e sono state applicate tecniche di validazione basate su simulazione esaustiva (model checking) attraverso il tool ObjectGEODE
Nel presente documento vengono descritti i servizi forniti da tali livelli, e viene descritta la specifica formale delle macchine a stati che realizzano i livelli CM e SL. i dettagli del codice SDL sono descritti nel documento (6)
From Tableau-based to SAT-based procedures - preliminary report
No full textTableau systems are very popular in AI for their simplicity and versatility. In recent papers we showed that tableau-based procedures are intrinsically inefficient, and proposed an alternative approach of building decision procedures on top of SAT decision procedure. We called this approach ‘SAT based’. In extensive empirical tests on the case study of modal K, a SAT-based procedure drastically outperformed a state-of-the-art tableau-based system. In this paper we provide the theoretical foundations for developing SAT-based decision procedures for many different modal logic
Applying the Davis-Putnam procedure to non-clausal formulas
No full textTraditionally, the satisfiability problem for propositional logics deals with formulas in Conjunctive Normal Form (CNF). A typical way to deal with non-CNF formulas requires (i) converting them into CNF, and (ii) applying solvers usually based on the Davis-Putnam (DP) procedure. A well known problem of this solution is that the CNF conversion may introduce many new variables, thus greatly widening the space of assignments in which the DP procedure has to search in order to find solutions.
In this paper we present two variants of the DP procedure which overcome the problem outlined above. The idea underlying these variants is that splitting should occur only for the variables in the original formula. The CNF conversion methods employed ensure their correctness and completeness. As a consequence, we get two decision procedures for non-CNF formulas (i) which can exploit all the present and future sophisticated technology of current DP implementations, and (ii) whose space of assignments they have to search in, is limited in size by the number of variables in the original input formula.
The preliminary analysis reported in [14] shows that these ideas can lead to a significant speed up of the search procedur
SAT-based decision procedures for normal modal logics: a theoretical framework
No full textTableau systems are very popular in AI for their simplicity and versatility. In recent papers we showed that tableau-based procedures are intrinsically inefficient, and proposed an alternative approach of building decision procedures on top of SAT decision procedure. We called this approach `SAT-based`. In extensive empirical tests on the case study of modal K, a SAT-based procedure drastically outperformed state-of-the-art tableau-based systems. In this paper we provide the theoretical foundations for developing SAT-based decision procedures for many different modal logic
- …
