default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDAlbert Oliveras
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[j14]Robert Nieuwenhuis
, Albert Oliveras, Enric Rodríguez-Carbonell:
IntSat: integer linear programming by conflict-driven constraint learning. Optim. Methods Softw. 39(1): 169-196 (2024)- [c33]Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Rui Zhao:
Speeding up Pseudo-Boolean Propagation. SAT 2024: 22:1-22:18 - [i5]Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
IntSat: Integer Linear Programming by Conflict-Driven Constraint-Learning. CoRR abs/2402.15522 (2024) - [i4]Sam Buss, Jonathan Chung, Vijay Ganesh, Albert Oliveras:
Extended Resolution Clause Learning via Dual Implication Points. CoRR abs/2406.14190 (2024) - 2023
- [c32]Albert Oliveras, Enric Rodríguez-Carbonell, Rui Zhao:
Analyzing Multiple Conflicts in SAT: An Experimental Evaluation. LPAR 2023: 306-316 - [c31]Albert Oliveras, Chunxiao Li, Darryl Wu, Jonathan Chung, Vijay Ganesh:
Learning Shorter Redundant Clauses in SDCL Using MaxSAT. SAT 2023: 18:1-18:17 - 2021
- [j13]Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
A Heuristic Approach to the Design of Optimal Cross-Docking Boxes. IEEE Access 9: 122578-122588 (2021) - [j12]Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Emma Rollon:
Employee Scheduling With SAT-Based Pseudo-Boolean Constraint Solving. IEEE Access 9: 142095-142104 (2021) - 2020
- [c30]Robert Nieuwenhuis, Adrià Lozano, Albert Oliveras, Enric Rodríguez-Carbonell:
Decision levels are stable: towards better SAT heuristics. LPAR 2020: 1-11 - [i3]Cristina Borralleras, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers. CoRR abs/2008.13601 (2020)
2010 – 2019
- 2019
- [j11]Cristina Borralleras, Daniel Larraz, Enric Rodríguez-Carbonell, Albert Oliveras, Albert Rubio:
Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers. ACM Trans. Comput. Log. 20(4): 25:1-25:36 (2019) - 2017
- [c29]Cristina Borralleras, Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
Proving Termination Through Conditional Termination. TACAS (1) 2017: 99-117 - 2016
- [c28]Lorenzo Candeago, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
Speeding up the Constraint-Based Method in Difference Logic. SAT 2016: 284-301 - 2015
- [c27]Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
Compositional Safety Verification with Max-SMT. FMCAD 2015: 33-40 - [i2]Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
Compositional Safety Verification with Max-SMT. CoRR abs/1507.03851 (2015) - 2014
- [c26]Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
Proving Non-termination Using Max-SMT. CAV 2014: 779-796 - [c25]Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions. SAT 2014: 333-350 - [i1]Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Valentin Mayer-Eichberger:
A New Look at BDDs for Pseudo-Boolean Constraints. CoRR abs/1401.5860 (2014) - 2013
- [j10]Clark W. Barrett, Morgan Deters, Leonardo Mendonça de Moura, Albert Oliveras, Aaron Stump:
6 Years of SMT-COMP. J. Autom. Reason. 50(3): 243-277 (2013) - [c24]Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints. CP 2013: 80-96 - [c23]Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Peter J. Stuckey:
To Encode or to Propagate? The Best Choice for Each Constraint in SAT. CP 2013: 97-106 - [c22]Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
Proving termination of imperative programs using Max-SMT. FMCAD 2013: 218-225 - 2012
- [j9]Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Valentin Mayer-Eichberger:
A New Look at BDDs for Pseudo-Boolean Constraints. J. Artif. Intell. Res. 45: 443-480 (2012) - [j8]Cristina Borralleras, Salvador Lucas, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
SAT Modulo Linear Arithmetic for Solving Polynomial Constraints. J. Autom. Reason. 48(1): 107-131 (2012) - 2011
- [j7]Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
Cardinality Networks: a theoretical and empirical study. Constraints An Int. J. 16(2): 195-221 (2011) - [j6]Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
A Framework for Certified Boolean Branch-and-Bound Optimization. J. Autom. Reason. 46(1): 81-102 (2011) - [c21]Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
BDDs for Pseudo-Boolean Constraints - Revisited. SAT 2011: 61-75 - 2010
- [j5]Roberto Javier Asín Achá, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
Practical algorithms for unsatisfiability proof and core generation in SAT solvers. AI Commun. 23(2-3): 145-157 (2010) - [c20]Javier Larrosa, Albert Oliveras, Enric Rodríguez-Carbonell:
Semiring-Induced Propositional Logic: Definition and Basic Algorithms. LPAR (Dakar) 2010: 332-347
2000 – 2009
- 2009
- [c19]Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
Cardinality Networks and Their Applications. SAT 2009: 167-180 - [c18]Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates. SAT 2009: 453-466 - 2008
- [j4]Clark W. Barrett, Morgan Deters, Albert Oliveras, Aaron Stump:
Design and Results of the 3rd Annual Satisfiability Modulo Theories Competition (SMT-Comp 2007). Int. J. Artif. Intell. Tools 17(4): 569-606 (2008) - [j3]Federico Heras, Javier Larrosa, Albert Oliveras:
MiniMaxSAT: An Efficient Weighted Max-SAT solver. J. Artif. Intell. Res. 31: 1-32 (2008) - [c17]Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
The Barcelogic SMT Solver. CAV 2008: 294-298 - [c16]Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
A Write-Based Solver for SAT Modulo the Theory of Arrays. FMCAD 2008: 1-8 - [c15]Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
Efficient Generation of Unsatisfiability Proofs and Cores in SAT. LPAR 2008: 16-30 - [c14]Germain Faure, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers. SAT 2008: 77-90 - [e1]Sava Krstic, Albert Oliveras:
Proceedings of the 5th International Workshop on Satisfiability Modulo Theories, SMT@CAV 2007, Berlin, Germany, July 1-2, 2007. Electronic Notes in Theoretical Computer Science 198(2), Elsevier 2008 [contents] - 2007
- [j2]Robert Nieuwenhuis, Albert Oliveras:
Fast congruence closure and extensions. Inf. Comput. 205(4): 557-580 (2007) - [c13]Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
Challenges in Satisfiability Modulo Theories. RTA 2007: 2-18 - [c12]Federico Heras, Javier Larrosa, Albert Oliveras:
MiniMaxSat: A New Weighted Max-SAT Solver. SAT 2007: 41-55 - [c11]Sava Krstic, Albert Oliveras:
Preface. SMT@CAV 2007: 1-2 - 2006
- [j1]Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli:
Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T). J. ACM 53(6): 937-977 (2006) - [c10]Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras:
SMT Techniques for Fast Predicate Abstraction. CAV 2006: 424-437 - [c9]Clark W. Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli:
Splitting on Demand in SAT Modulo Theories. LPAR 2006: 512-526 - [c8]Robert Nieuwenhuis, Albert Oliveras:
On SAT Modulo Theories and Optimization Problems. SAT 2006: 156-169 - 2005
- [c7]Robert Nieuwenhuis, Albert Oliveras:
DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. CAV 2005: 321-334 - [c6]Robert Nieuwenhuis, Albert Oliveras:
Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools. LPAR 2005: 23-46 - [c5]Robert Nieuwenhuis, Albert Oliveras:
Proof-Producing Congruence Closure. RTA 2005: 453-468 - 2004
- [c4]Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli:
DPLL( T): Fast Decision Procedures. CAV 2004: 175-188 - [c3]Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli:
Abstract DPLL and Abstract DPLL Modulo Theories. LPAR 2004: 36-50 - 2003
- [c2]Robert Nieuwenhuis, Albert Oliveras:
Congruence Closure with Integer Offsets. LPAR 2003: 78-90
1990 – 1999
- 1991
- [c1]Eduardo Lleida, José B. Mariño, Climent Nadeu, Albert Oliveras:
Two level continuous speech recognition using demisyllable-based HMM word spotting. EUROSPEECH 1991: 1199-1202
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-22 20:48 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
