Applying GSAT to Non-Clausal Formulas. - Roberto Sebastiani (CoRR, 1994)

Applying GSAT to Non-Clausal Formulas (Research Note). - Roberto Sebastiani (J. Artif. Intell. Res., 1994)

Computing Abstraction Hierarchies by Numerical Simulation. - Alan Bundy; Fausto Giunchiglia; Roberto Sebastiani; Toby Walsh (AAAI/IAAI, Vol. 1, 1996)

A General Purpose Reasoner for Abstraction. - Fausto Giunchiglia; Roberto Sebastiani; Adolfo Villafiorita; Toby Walsh (AI, 1996)

Building Decision Procedures for Modal Logics from Propositional Decision Procedure - The Case Study of Modal K. - Fausto Giunchiglia; Roberto Sebastiani (CADE, 1996)

A New Method for Testing Decision Procedures in Modal and Terminological Logics. - Fausto Giunchiglia; Marco Roveri; Roberto Sebastiani (Description Logics, 1996)

An SAT-based Decision Procedure for ALC. - Fausto Giunchiglia; Roberto Sebastiani (Description Logics, 1996)

A SAT-based Decision Procedure for ALC. - Fausto Giunchiglia; Roberto Sebastiani (KR, 1996)

Calculating Criticalities. - Alan Bundy; Fausto Giunchiglia; Roberto Sebastiani; Toby Walsh (Artif. Intell., 1996)

A New Method for Testing Decision Procedures in Modal Logics. - Fausto Giunchiglia; Marco Roveri; Roberto Sebastiani (CADE, 1997)

Act, and the Rest Will Follow: Exploiting Determinism in Planning as Satisfiability. - Enrico Giunchiglia; Alessandro Massarotto; Roberto Sebastiani (AAAI/IAAI, 1998)

SAT-Based Decision Procedures for Normal Modal Logics: A Theoretical Framework. - Roberto Sebastiani; Adolfo Villafiorita (AIMSA, 1998)

More Evaluation of Decision Procedures for Modal Logics. - Enrico Giunchiglia; Fausto Giunchiglia; Roberto Sebastiani; Armando Tacchella (KR, 1998)

Applying the Davis-Putnam Procedure to Non-clausal Formulas. - Enrico Giunchiglia; Roberto Sebastiani (AI*IA, 1999)

Formal Specification and Validation of a Vital Communication Protocol. - Alessandro Cimatti; P. L. Pieraccini; Roberto Sebastiani; Paolo Traverso; Adolfo Villafiorita (World Congress on Formal Methods, 1999)

Formal Specification and Development of a Safety-Critical Train Management System. - Angelo Chiappini; Alessandro Cimatti; Carmen Porzia; G. Rotondo; Roberto Sebastiani; Paolo Traverso; Adolfo Villafiorita (SAFECOMP, 1999)

Building Decision Procedures for Modal Logics from Propositional Decision Procedures: The Case Study of Modal K(m). - Fausto Giunchiglia; Roberto Sebastiani (Inf. Comput., 2000)

An Analysis of Empirical Testing for Modal Decision Procedures. - Ian Horrocks 001; Peter F. Patel-Schneider; Roberto Sebastiani (Log. J. IGPL, 2000)

SAT vs. translation based decision procedures for modal logics: a comparative evaluation. - Enrico Giunchiglia; Fausto Giunchiglia; Roberto Sebastiani; Armando Tacchella (J. Appl. Non Class. Logics, 2000)

A New System and Methodology for Generating Random Modal Formulae. - Peter F. Patel-Schneider; Roberto Sebastiani (IJCAR, 2001)

Model Checking Syllabi and Student Carreers. - Roberto Sebastiani; Alessandro Tomasi 002; Fausto Giunchiglia (TACAS, 2001)

Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and Requirements. - Gilles Audemard; Piergiorgio Bertoli; Alessandro Cimatti; Artur Kornilowicz; Roberto Sebastiani (AISC, 2002)

A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. - Gilles Audemard; Piergiorgio Bertoli; Alessandro Cimatti; Artur Kornilowicz; Roberto Sebastiani (CADE, 2002)

NuSMV 2: An OpenSource Tool for Symbolic Model Checking. - Alessandro Cimatti; Edmund M. Clarke; Enrico Giunchiglia; Fausto Giunchiglia; Marco Pistore; Marco Roveri; Roberto Sebastiani; Armando Tacchella (CAV, 2002)

Reasoning with Goal Models. - Paolo Giorgini; John Mylopoulos; Eleonora Nicchiarelli; Roberto Sebastiani (ER, 2002)

Bounded Model Checking for Timed Systems. - Gilles Audemard; Alessandro Cimatti; Artur Kornilowicz; Roberto Sebastiani (FORTE, 2002)

Integrating BDD-Based and SAT-Based Symbolic Model Checking. - Alessandro Cimatti; Enrico Giunchiglia; Marco Pistore; Marco Roveri; Roberto Sebastiani; Armando Tacchella (FroCoS, 2002)

Improving the Encoding of LTL Model Checking into SAT. - Alessandro Cimatti; Marco Pistore; Marco Roveri; Roberto Sebastiani (VMCAI, 2002)

Editorial: The Integration of Automated Reasoning and Computer Algebra Systems. - Steve Linton; Roberto Sebastiani (J. Symb. Comput., 2002)

"More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking. - Roberto Sebastiani; Stefano Tonetta (CHARME, 2003)

A New General Method to Generate Random Modal Formulae for Testing Decision Procedures. - Peter F. Patel-Schneider; Roberto Sebastiani (J. Artif. Intell. Res., 2003)

Formal Reasoning Techniques for Goal Models. - Paolo Giorgini; John Mylopoulos; Eleonora Nicchiarelli; Roberto Sebastiani (J. Data Semant., 2003)

Simple and Minimum-Cost Satisfiability for Goal Models. - Roberto Sebastiani; Paolo Giorgini; John Mylopoulos (CAiSE, 2004)

Verifying Industrial Hybrid Systems with MathSAT. - Gilles Audemard; Marco Bozzano; Alessandro Cimatti; Roberto Sebastiani (BMC@CAV, 2004)

The MathSAT 3 System. - Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi A. Junttila; Peter van Rossum; Stephan Schulz 001; Roberto Sebastiani (CADE, 2005)

Efficient Satisfiability Modulo Theories via Delayed Theory Combination. - Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi A. Junttila; Silvio Ranise; Peter van Rossum; Roberto Sebastiani (CAV, 2005)

An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. - Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi A. Junttila; Peter van Rossum; Stephan Schulz 001; Roberto Sebastiani (TACAS, 2005)

Goal-oriented requirements analysis and reasoning in the Tropos methodology. - Paolo Giorgini; John Mylopoulos; Roberto Sebastiani (Eng. Appl. Artif. Intell., 2005)

Encoding RTL Constructs for MathSAT: a Preliminary Report. - Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Ziyad Hanna; Zurab Khasidashvili; Amit Palti; Roberto Sebastiani (PDPAR@CAV, 2005)

MathSAT: Tight Integration of SAT and Mathematical Decision Procedures. - Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi A. Junttila; Peter van Rossum; Stephan Schulz 001; Roberto Sebastiani (J. Autom. Reason., 2005)

To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF ÈT). - Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Alberto Griggio; Alessandro Santuari; Roberto Sebastiani (LPAR, 2006)

Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ALC. - Roberto Sebastiani; Michele Vescovi (SAT, 2006)

Building Efficient Decision Procedures on Top of SAT Solvers. - Alessandro Cimatti; Roberto Sebastiani (SFM, 2006)

Preface and Foreword. - Byron Cook; Roberto Sebastiani (PDPAR/PaUL@FLoC, 2006)

Efficient theory combination via boolean search. - Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi A. Junttila; Silvio Ranise; Peter van Rossum; Roberto Sebastiani (Inf. Comput., 2006)

A Lazy and Layered SMT($ mathcal{BV}$) Solver for Hard Industrial Verification Problems. - Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Alberto Griggio; Ziyad Hanna; Alexander Nadel; Amit Palti; Roberto Sebastiani (CAV, 2007)

From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain. - Roberto Sebastiani (FroCoS, 2007)

A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories. - Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani (SAT, 2007)

Property-Driven Partitioning for Abstraction Refinement. - Roberto Sebastiani; Stefano Tonetta; Moshe Y. Vardi (TACAS, 2007)

GSTE is partitioned model checking. - Roberto Sebastiani; Eli Singerman; Stefano Tonetta; Moshe Y. Vardi (Formal Methods Syst. Des., 2007)

Preface to Special Issue on Satisfiability Modulo Theories. - Byron Cook; Roberto Sebastiani (J. Satisf. Boolean Model. Comput., 2007)

Lazy Satisability Modulo Theories. - Roberto Sebastiani (J. Satisf. Boolean Model. Comput., 2007)

The MathSAT 4SMT Solver. - Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Alberto Griggio; Roberto Sebastiani (CAV, 2008)

Efficient Interpolant Generation in Satisfiability Modulo Theories. - Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani (TACAS, 2008)

Interpolant Generation for UTVPI. - Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani (CADE, 2009)

Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis. - Roberto Sebastiani; Michele Vescovi (CADE, 2009)

Software model checking via large-block encoding. - Dirk Beyer 001; Alessandro Cimatti; Alberto Griggio; M. Erkan Keremoglu; Roberto Sebastiani (FMCAD, 2009)

Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. - Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Alberto Griggio; Roberto Sebastiani (Ann. Math. Artif. Intell., 2009)

Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability. - Roberto Sebastiani; Michele Vescovi (J. Artif. Intell. Res., 2009)

Satisfiability Modulo Theories. - Clark W. Barrett; Roberto Sebastiani; Sanjit A. Seshia; Cesare Tinelli (Handbook of Satisfiability, 2009)

SAT Techniques for Modal and Description Logics. - Roberto Sebastiani; Armando Tacchella (Handbook of Satisfiability, 2009)

Applying SMT in symbolic execution of microcode. - Anders Franzén; Alessandro Cimatti; Alexander Nadel; Roberto Sebastiani; Jonathan Shalev (FMCAD, 2010)

Satisfiability Modulo the Theory of Costs: Foundations and Applications. - Alessandro Cimatti; Anders Franzén; Alberto Griggio; Roberto Sebastiani; Cristian Stenico (TACAS, 2010)

Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic - Alberto Griggio; Thi Thieu Hoa Le; Roberto Sebastiani (Log. Methods Comput. Sci., 2010)

Efficient generation of craig interpolants in satisfiability modulo theories. - Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani (ACM Trans. Comput. Log., 2010)

Goal Modeling and Reasoning in Tropos. - Paolo Giorgini; John Mylopoulos; Roberto Sebastiani (Social Modeling for Requirements Engineering, 2011)

Automated Reasoning in ALCQ mathcal{ALCQ} via SMT. - Volker Haarslev; Roberto Sebastiani; Michele Vescovi (CADE, 2011)

Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT. - Alberto Griggio; Quoc-Sang Phan; Roberto Sebastiani; Silvia Tomasi (FroCoS, 2011)

Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories. - Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani (J. Artif. Intell. Res., 2011)

Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking. - Roberto Sebastiani; Stefano Tonetta; Moshe Y. Vardi (Int. J. Softw. Tools Technol. Transf., 2011)

Optimization in SMT with ${ mathcal LA}$ (ℚ) Cost Functions. - Roberto Sebastiani; Silvia Tomasi (IJCAR, 2012)

Optimization in SMT with LA(Q) Cost Functions - Roberto Sebastiani; Silvia Tomasi (CoRR, 2012)

A Modular Approach to MaxSAT Modulo Theories. - Alessandro Cimatti; Alberto Griggio; Bastiaan Joost Schaafsma; Roberto Sebastiani (SAT, 2013)

The MathSAT5 SMT Solver. - Alessandro Cimatti; Alberto Griggio; Bastiaan Joost Schaafsma; Roberto Sebastiani (TACAS, 2013)

Hybrid SRL with Optimization Modulo Theories. - Stefano Teso; Roberto Sebastiani; Andrea Passerini (CoRR, 2014)

Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions. - Roberto Sebastiani; Patrick Trentin (TACAS, 2015)

Optimization Modulo Theories with Linear Rational Costs. - Roberto Sebastiani; Silvia Tomasi (ACM Trans. Comput. Log., 2015)

Colors Make Theories Hard. - Roberto Sebastiani (IJCAR, 2016)

On the Benefits of Enhancing Optimization Modulo Theories with Sorting Networks for MaxSMT. - Roberto Sebastiani; Patrick Trentin (SMT@IJCAR, 2016)

Verilog2SMV: A tool for word-level verification. - Ahmed Irfan; Alessandro Cimatti; Alberto Griggio; Marco Roveri; Roberto Sebastiani (DATE, 2016)

Requirements Evolution and Evolution Requirements with Constrained Goal Models. - Chi Mai Nguyen; Roberto Sebastiani; Paolo Giorgini; John Mylopoulos (ER, 2016)

Multi Object Reasoning with Constrained Goal Model. - Chi Mai Nguyen; Roberto Sebastiani; Paolo Giorgini; John Mylopoulos (CoRR, 2016)

Satisfiability Modulo Transcendental Functions via Incremental Linearization. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (CADE, 2017)

Solving SAT and MaxSAT with a Quantum Annealer: Foundations and a Preliminary Report. - Zhengbing Bian; Fabián A. Chudak; William G. Macready; Aidan Roy; Roberto Sebastiani; Stefano Varotti (FroCoS, 2017)

Efficient Weighted Model Integration via SMT-Based Predicate Abstraction. - Paolo Morettin; Andrea Passerini; Roberto Sebastiani (IJCAI, 2017)

Modeling and Reasoning on Requirements Evolution with Constrained Goal Models. - Chi Mai Nguyen; Roberto Sebastiani; Paolo Giorgini; John Mylopoulos (SEFM, 2017)

Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (TACAS (1), 2017)

On Optimization Modulo Theories, MaxSMT and Sorting Networks. - Roberto Sebastiani; Patrick Trentin (TACAS (2), 2017)

Structured learning modulo theories. - Stefano Teso; Roberto Sebastiani; Andrea Passerini (Artif. Intell., 2017)

Planning with Strategic Goals. - Evellin Cristine Souza Cardoso; Jennifer Horkoff; Roberto Sebastiani; John Mylopoulos (EDOC, 2018)

Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (SAT, 2018)

Incremental linearization: A practical approach to satisfiability modulo nonlinear arithmetic and transcendental functions. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (SYNASC, 2018)

OpenMath and SMT-LIB. - James H. Davenport; Matthew England 001; Roberto Sebastiani; Patrick Trentin (CoRR, 2018)

Multi-objective reasoning with constrained goal models. - Chi Mai Nguyen; Roberto Sebastiani; Paolo Giorgini; John Mylopoulos (Requir. Eng., 2018)

Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (ACM Trans. Comput. Log., 2018)

Optimization Modulo the Theory of Floating-Point Numbers. - Patrick Trentin; Roberto Sebastiani (CADE, 2019)

The pywmi Framework and Toolbox for Probabilistic Inference using Weighted Model Integration. - Samuel Kolb; Paolo Morettin; Pedro Zuidberg Dos Martires; Francesco Sommavilla; Andrea Passerini; Roberto Sebastiani; Luc De Raedt (IJCAI, 2019)

Lemmas for Satisfiability Modulo Transcendental Functions via Incremental Linearization. - Ahmed Irfan; Alessandro Cimatti; Alberto Griggio; Marco Roveri; Roberto Sebastiani (SC-square@SIAM AG, 2019)

Advanced SMT techniques for weighted model integration. - Paolo Morettin; Andrea Passerini; Roberto Sebastiani (Artif. Intell., 2019)

From MiniZinc to Optimization Modulo Theories, and Back (Extended Version). - Francesco Contaldo; Patrick Trentin; Roberto Sebastiani (CoRR, 2019)

From MiniZinc to Optimization Modulo Theories, and Back. - Francesco Contaldo; Patrick Trentin; Roberto Sebastiani (CPAIOR, 2020)

Four Flavors of Entailment. - Sibylle Möhle; Roberto Sebastiani; Armin Biere (SAT, 2020)

Are You Satisfied by This Partial Assignment? - Roberto Sebastiani (CoRR, 2020)

Solving SAT (and MaxSAT) with a quantum annealer: Foundations, encodings, and preliminary results. - Zhengbing Bian; Fabián A. Chudak; William G. Macready; Aidan Roy; Roberto Sebastiani; Stefano Varotti (Inf. Comput., 2020)

Preface: Special Issue of Selected Extended Papers from IJCAR 2018. - Didier Galmiche; Stephan Schulz 001; Roberto Sebastiani (J. Autom. Reason., 2020)

OptiMathSAT: A Tool for Optimization Modulo Theories. - Roberto Sebastiani; Patrick Trentin (J. Autom. Reason., 2020)

Optimization Modulo Non-linear Arithmetic via Incremental Linearization. - Filippo Bigarella; Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Martin Jonás; Marco Roveri; Roberto Sebastiani; Patrick Trentin (FroCoS, 2021)

Optimization Modulo the Theories of Signed Bit-Vectors and Floating-Point Numbers. - Patrick Trentin; Roberto Sebastiani (J. Autom. Reason., 2021)

Satisfiability Modulo Theories. - Clark W. Barrett; Roberto Sebastiani; Sanjit A. Seshia; Cesare Tinelli (Handbook of Satisfiability, 2021)

SAT Techniques for Modal and Description Logics. - Roberto Sebastiani; Armando Tacchella (Handbook of Satisfiability, 2021)

Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test. - Alessandro Cimatti; Alberto Griggio; Enrico Lipparini; Roberto Sebastiani (ATVA, 2022)

SMT-based weighted model integration with structure awareness. - Giuseppe Spallitta; Gabriele Masina; Paolo Morettin; Andrea Passerini; Roberto Sebastiani (UAI, 2022)

On CNF Conversion for Disjoint SAT Enumeration. - Gabriele Masina; Giuseppe Spallitta; Roberto Sebastiani (SAT, 2023)

On CNF Conversion for SAT Enumeration. - Gabriele Masina; Giuseppe Spallitta; Roberto Sebastiani (CoRR, 2023)

Enumerating Disjoint Partial Models without Blocking Clauses. - Giuseppe Spallitta; Roberto Sebastiani; Armin Biere (CoRR, 2023)

Effective Prime Factorization via Quantum Annealing by Modular Locally-structured Embedding. - Jingwen Ding; Giuseppe Spallitta; Roberto Sebastiani (CoRR, 2023)

Disjoint Partial Enumeration without Blocking Clauses. - Giuseppe Spallitta; Roberto Sebastiani; Armin Biere (AAAI, 2024)

Canonical Decision Diagrams Modulo Theories. - Massimo Michelutti; Gabriele Masina; Giuseppe Spallitta; Roberto Sebastiani (ECAI, 2024)

Entailing Generalization Boosts Enumeration. - Dror Fried; Alexander Nadel; Roberto Sebastiani; Yogev Shalmon (SAT, 2024)

A Unified Framework for Probabilistic Verification of AI Systems via Weighted Model Integration. - Paolo Morettin; Andrea Passerini; Roberto Sebastiani (CoRR, 2024)

Experimenting with D-Wave quantum annealers on prime factorization problems. - Jingwen Ding; Giuseppe Spallitta; Roberto Sebastiani (Frontiers Comput. Sci., 2024)

Enhancing SMT-based Weighted Model Integration by structure awareness. - Giuseppe Spallitta; Gabriele Masina; Paolo Morettin; Andrea Passerini; Roberto Sebastiani (Artif. Intell., 2024)

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses: TabularAllSAT source code. - Giuseppe Spallitta; Armin Biere; Roberto Sebastiani (Zenodo, 2024)

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses: TabularAllSMT. - Giuseppe Spallitta; Armin Biere; Roberto Sebastiani (Zenodo, 2024)

Entailment vs. Verification for Partial-Assignment Satisfiability and Enumeration. - Roberto Sebastiani (CADE, 2025)

A Probabilistic Neuro-symbolic Layer for Algebraic Constraint Satisfaction. - Leander Kurscheidt; Paolo Morettin; Roberto Sebastiani; Andrea Passerini; Antonio Vergari (UAI, 2025)

Disjoint projected enumeration for SAT and SMT without blocking clauses. - Giuseppe Spallitta; Roberto Sebastiani; Armin Biere (Artif. Intell., 2025)

On enumerating short projected models. - Sibylle Möhle; Roberto Sebastiani; Armin Biere (Discret. Appl. Math., 2025)

On CNF Conversion for SAT and SMT Enumeration. - Gabriele Masina; Giuseppe Spallitta; Roberto Sebastiani (J. Artif. Intell. Res., 2025)

Exploiting Partial Assignments in Optimization Modulo Theories. - Gabriele Masina; Roberto Sebastiani (CoRR, 2025)