| Nome |
# |
|
Solving SAT and MaxSAT with a quantum annealer: Foundations and a preliminary report, file e3835193-e0fa-72ef-e053-3705fe0ad821
|
491
|
|
Incremental Linearization: A practical approach to Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions, file e3835196-85c4-72ef-e053-3705fe0ad821
|
283
|
|
OptiMathSAT: A Tool for Optimization Modulo Theories, file e3835195-2999-72ef-e053-3705fe0ad821
|
276
|
|
Incremental Linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions, file e3835195-298b-72ef-e053-3705fe0ad821
|
182
|
|
Multi-objective reasoning with constrained goal models, file e3835195-2994-72ef-e053-3705fe0ad821
|
158
|
|
Planning with strategic goals, file e3835195-299d-72ef-e053-3705fe0ad821
|
148
|
|
Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories, file e3835192-3a7a-72ef-e053-3705fe0ad821
|
142
|
|
Modeling and reasoning on requirements evolution with constrained goal models, file e3835193-e101-72ef-e053-3705fe0ad821
|
140
|
|
Colors make theories hard, file e3835193-7494-72ef-e053-3705fe0ad821
|
139
|
|
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic, file e3835192-41bb-72ef-e053-3705fe0ad821
|
126
|
|
OptiMathSAT: A Tool for Optimization Modulo Theories, file e3835192-4863-72ef-e053-3705fe0ad821
|
117
|
|
The pywmi Framework and Toolbox for Probabilistic Inference using Weighted Model Integration, file e3835196-0cf3-72ef-e053-3705fe0ad821
|
95
|
|
Requirements evolution and evolution requirements with constrained goal models, file e3835193-7186-72ef-e053-3705fe0ad821
|
84
|
|
Optimization Modulo Non-linear Arithmetic via Incremental Linearization, file e3835198-b64e-72ef-e053-3705fe0ad821
|
59
|
|
Preface: Special Issue of Selected Extended Papers from IJCAR 2018, file e3835197-74f6-72ef-e053-3705fe0ad821
|
47
|
|
Efficiently Integrating Boolean Reasoning and Mathematical Solving, file 48eec8bc-7230-4b41-8f75-09c4c6c71894
|
46
|
|
A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions, file 707a350b-6a42-4298-8081-c9d867443d12
|
44
|
|
Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms and Requirements, file 334cb655-c596-4ac0-a64c-cf9088380c67
|
43
|
|
Improving the Encoding of LTL Model Checking into SAT, file 4cb40a10-2b80-4fe9-a139-380f2ccb69b7
|
41
|
|
Integrating BDD-based and SAT-based Symbolic Model Checking, file 3383f330-e78f-4d52-aa3f-f8312a9b01ee
|
28
|
|
Bounded Model Checking for Timed Systems, file e3c3620c-8a1b-4099-8fdf-a05a99df7591
|
27
|
|
Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test, file 0c8cceb4-2ef5-4e59-8d54-d51b0f0a726c
|
22
|
|
On the Benefits of Enhancing Optimization Modulo Theories with Sorting Networks for MaxSMT, file e3835195-2add-72ef-e053-3705fe0ad821
|
19
|
|
On CNF Conversion for Disjoint SAT Enumeration, file 1d1a068b-61fa-4e2a-9d77-7d2d626e3b36
|
18
|
|
SMT-based Weighted Model Integration with Structure Awareness, file 6cf816dd-afe8-4324-abda-c373a3f5dd46
|
18
|
|
Structured learning modulo theories, file e3835198-01e9-72ef-e053-3705fe0ad821
|
18
|
|
Lemmas for satisfiability modulo transcendental functions via incremental linearization, file e3835197-04ba-72ef-e053-3705fe0ad821
|
17
|
|
Optimization Modulo the Theories of Signed Bit-Vectors and Floating-Point Numbers, file e3835199-7b53-72ef-e053-3705fe0ad821
|
11
|
|
Constructive Learning Modulo Theories, file e3835193-f845-72ef-e053-3705fe0ad821
|
10
|
|
Structured learning modulo theories, file e3835194-4fff-72ef-e053-3705fe0ad821
|
10
|
|
A CEGAR-based Approach for Proving Invariant Properties of Transition Systems on Non-Linear Real Arithmetic, file e3835195-2adf-72ef-e053-3705fe0ad821
|
10
|
|
Satisfiability Modulo Transcendental Functions via Incremental Linearization, file e3835197-23cd-72ef-e053-3705fe0ad821
|
9
|
|
NuSMV2: an Open Source Tool for Symbolic Model Checking, file 7d07670e-f43d-45cc-9355-617c151c19ca
|
7
|
|
OpenMath and SMT-LIB, file e3835195-2172-72ef-e053-3705fe0ad821
|
7
|
|
More Deterministic" vs. "Smaller" Buechi Automata for Efficient LTL Model Checking", file 000c4aaa-a735-47e6-af81-52b6fe493032
|
5
|
|
A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories, file 3664ab65-c58a-47d6-a631-5661595d6665
|
5
|
|
Reasoning with Goal Models, file 3f7a1341-1641-451e-8bf5-d43b3645f368
|
5
|
|
On Efficiently Integrating Boolean and Theory-Specific Solving Procedures, file 828d0912-589e-4822-8722-139ce25b081d
|
5
|
|
Automated Reasoning on TBoxes with Qualified Number Restrictions via SMT, file 83cd21d5-f32c-49ea-8700-cc43a81debd1
|
5
|
|
Optimization Modulo the Theory of Floating-Point Numbers, file e3835197-5ec7-72ef-e053-3705fe0ad821
|
5
|
|
GSTE is Partitioned Model Checking, file 0ab02c8c-54d4-4555-819b-0408a84b1d30
|
4
|
|
From KSAT to delayed theory combination: exploiting DPLL outside the SAT domain, file 8a0cec0a-1f31-4f5a-a114-f6337f482328
|
4
|
|
Stochastic Local Search for SMT: A Preliminary Report, file b4a91a3b-7294-4fd0-ba7a-fee7daee9902
|
4
|
|
Towards a Unified Framework for Probabilistic Verification of AI Systems, file c26abeb5-f39d-403a-abb5-c5434919225d
|
4
|
|
null, file e3835192-3a82-72ef-e053-3705fe0ad821
|
4
|
|
Optimization Modulo Theories with Linear Rational Costs, file e3835192-434e-72ef-e053-3705fe0ad821
|
4
|
|
OptiMathSAT: A Tool for Optimization Modulo Theories, file e3835195-60dc-72ef-e053-3705fe0ad821
|
4
|
|
Multi-objective reasoning with constrained goal models, file e3835195-8d53-72ef-e053-3705fe0ad821
|
4
|
|
Invariant checking of NRA transition systems via incremental reduction to LRA with EUF, file e3835197-1d47-72ef-e053-3705fe0ad821
|
4
|
|
Software Model Checking via Large-Block Encoding, file e4737e61-1793-4059-a61f-83d49b701149
|
4
|
|
Efficient Interpolant Generation in Satisfiability Modulo Theories, file ebddc2d9-2dca-4166-88f4-2594639cacb5
|
4
|
|
Optimization in SMT with LA(Q) Cost Functions, file 35d9d691-d621-4f1a-b06b-5b75b38965df
|
3
|
|
To Ackermann-ize or not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF U T), file 4c4217c2-b02e-49b3-808d-b4d0451d0be1
|
3
|
|
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis, file 87fec377-ecef-4558-a79a-83971da17d88
|
3
|
|
Encoding the satisfiability of modal and description logics into SAT: the case study of K(m)/ALC, file acf1e529-af9b-4fcb-985a-8f88a1906578
|
3
|
|
Lazy Satisfiability Modulo Theories, file b5e7422f-e1d2-4413-a916-cb21c9cbbdc0
|
3
|
|
Planning with strategic goals, file e3835196-ff26-72ef-e053-3705fe0ad821
|
3
|
|
From MiniZinc to Optimization Modulo Theories, and Back, file e3835197-809c-72ef-e053-3705fe0ad821
|
3
|
|
From MiniZinc to Optimization Modulo Theories, and Back, file e3835198-ccd1-72ef-e053-3705fe0ad821
|
3
|
|
Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis, file 3befc3a1-aee9-4c96-ae17-15e2a0323070
|
2
|
|
A New General Method to Generate Random Modal Formulae for Testing Decision Procedures, file bb07ca2e-9855-449a-aa11-1aa513ee456f
|
2
|
|
Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking, file e3835192-15ea-72ef-e053-3705fe0ad821
|
2
|
|
Four Flavors of Entailment, file e3835197-aafb-72ef-e053-3705fe0ad821
|
2
|
|
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis, file c20b0185-72fd-4c50-aeae-089303f2e3ca
|
1
|
|
Efficient Interpolant Generation in Satisfiability Modulo Theories, file e3835191-d1df-72ef-e053-3705fe0ad821
|
1
|
|
null, file e3835192-3a7f-72ef-e053-3705fe0ad821
|
1
|
|
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic, file e3835192-3ac2-72ef-e053-3705fe0ad821
|
1
|
|
Automated Reasoning in ALCQ via SMT, file e3835192-42fd-72ef-e053-3705fe0ad821
|
1
|
|
Theory and Applications of Satisfiability Testing - SAT 2012- 15th International Conference., file e3835192-4433-72ef-e053-3705fe0ad821
|
1
|
|
Pushing the Envelope of Optimization Modulo Theories
with Linear-Arithmetic Cost Functions, file e3835192-5ba4-72ef-e053-3705fe0ad821
|
1
|
|
Verilog2SMV: A tool for word-level verification, file e3835193-6e44-72ef-e053-3705fe0ad821
|
1
|
|
Efficient Weighted Model Integration via SMT-Based Predicate Abstraction, file e3835193-e16c-72ef-e053-3705fe0ad821
|
1
|
|
Advanced SMT techniques for weighted model integration, file e3835195-b260-72ef-e053-3705fe0ad821
|
1
|
|
OptiMathSAT: A Tool for Optimization Modulo Theories, file e3835197-24a6-72ef-e053-3705fe0ad821
|
1
|
|
Incremental Linearization: A practical approach to Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions, file e3835197-5378-72ef-e053-3705fe0ad821
|
1
|
|
Four Flavors of Entailment for Projected Model Counting, file e3835197-cd87-72ef-e053-3705fe0ad821
|
1
|
|
Satisfiability Modulo Theories, file e3835198-b38c-72ef-e053-3705fe0ad821
|
1
|
|
SAT Techniques for Modal and Description Logics, file e3835198-f02c-72ef-e053-3705fe0ad821
|
1
|
|
Solving SAT (and MaxSAT) with a quantum annealer: Foundations, encodings, and preliminary results, file e3835199-1410-72ef-e053-3705fe0ad821
|
1
|
| Totale |
3.014 |