×

zbMATH — the first resource for mathematics

Marques-Silva, João P.

Compute Distance To:
Author ID: marques-silva.joao-p Recent zbMATH articles by "Marques-Silva, João P."
Published as: Marques-Silva, J.; Marques-Silva, Joao; Marques-Silva, João; Marques-Silva, João P.
Documents Indexed: 95 Publications since 1999, including 1 Book

Publications by Year

Citations contained in zbMATH Open

81 Publications have been cited 492 times in 283 Documents Cited by Year
GRASP: a search algorithm for propositional satisfiability. Zbl 1392.68388
Marques-Silva, João P.; Sakallah, Karem A.
86
1999
Solving QBF with counterexample guided refinement. Zbl 1273.68178
Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund
20
2012
Algorithms for weighted Boolean optimization. Zbl 1247.68258
Manquinho, Vasco; Marques-Silva, Joao; Planes, Jordi
20
2009
Expansion-based QBF solving versus Q-resolution. Zbl 1309.68168
Janota, Mikoláš; Marques-Silva, Joao
19
2015
Iterative and core-guided maxsat solving: a survey and assessment. Zbl 1317.90199
Morgado, Antonio; Heras, Federico; Liffiton, Mark; Planes, Jordi; Marques-Silva, Joao
19
2013
Towards efficient MUS extraction. Zbl 1248.68450
Belov, Anton; Lynce, Inês; Marques-Silva, Joao
14
2012
Fast, flexible MUS enumeration. Zbl 1334.90080
Liffiton, Mark H.; Previti, Alessandro; Malik, Ammar; Marques-Silva, Joao
13
2016
Categorisation of clauses in conjunctive normal forms: minimally unsatisfiable sub-clause-sets and the lean kernel. Zbl 1187.68552
Kullmann, Oliver; Lynce, Inês; Marques-Silva, João
12
2006
Abstraction-based algorithm for 2QBF. Zbl 1330.68115
Janota, Mikoláš; Marques-Silva, Joao
11
2011
Using randomization and learning to solve hard real-world instances of satisfiability. Zbl 1044.68736
Baptista, Luís; Marques-Silva, João
11
2000
Algorithms for computing backbones of propositional formulae. Zbl 1373.68379
Janota, Mikoláš; Lynce, Inês; Marques-Silva, Joao
9
2015
MUSer2: an efficient MUS extractor. Zbl 1322.68178
Belov, Anton; Marques-Silva, Joao
9
2014
Solving QBF with counterexample guided refinement. Zbl 1351.68254
Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund
8
2016
On propositional QBF expansions and Q-resolution. Zbl 1390.03017
Janota, Mikoláš; Marques-Silva, Joao
8
2013
Boolean lexicographic optimization: algorithms & applications. Zbl 1242.90199
Marques-Silva, Joao; Argelich, Josep; Graça, Ana; Lynce, Inês
8
2011
Towards robust CNF encodings of cardinality constraints. Zbl 1145.68525
Marques-Silva, Joao; Lynce, Inês
8
2007
A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. Zbl 1128.68477
Mneimneh, Maher; Lynce, Inês; Andraus, Zaher; Marques-Silva, João; Sakallah, Karem
8
2005
Algebraic simplification techniques for propositional satisfiability. Zbl 1044.68781
Marques-Silva, João
8
2000
Improvements to core-guided binary search for MaxSAT. Zbl 1273.68357
Morgado, Antonio; Heras, Federico; Marques-Silva, Joao
7
2012
On the query complexity of selecting minimal sets for monotone predicates. Zbl 1351.68117
Janota, Mikoláš; Marques-Silva, Joao
6
2016
Progression in maximum satisfiability. Zbl 1366.68266
Ignatiev, A.; Morgado, A.; Manquinho, V.; Lynce, I.; Marques-Silva, J.
6
2014
Computing minimally unsatisfiable subformulas: state of the art and future directions. Zbl 1394.68359
Marques-Silva, Joao
6
2012
Knowledge compilation with empowerment. Zbl 1302.68248
Bordeaux, Lucas; Marques-Silva, Joao
6
2012
On improving MUS extraction algorithms. Zbl 1330.68273
Marques-Silva, Joao; Lynce, Ines
6
2011
A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Zbl 1181.90291
Liffiton, Mark; Mneimneh, Maher; Lynce, Inês; Andraus, Zaher; Marques-Silva, João; Sakallah, Karem
6
2009
Towards more effective unsatisfiability-based maximum satisfiability algorithms. Zbl 1138.68548
Marques-Silva, Joao; Manquinho, Vasco
6
2008
Efficient haplotype inference with pseudo-Boolean optimization. Zbl 1126.92035
Graça, Ana; Marques-Silva, João; Lynce, Inês; Oliveira, Arlindo L.
6
2007
Enumerating prime implicants of propositional formulae in conjunctive normal form. Zbl 1432.68327
Jabbour, Said; Marques-Silva, Joao; Sais, Lakhdar; Salhi, Yakoub
5
2014
Formula preprocessing in MUS extraction. Zbl 1381.68146
Belov, Anton; Järvisalo, Matti; Marques-Silva, Joao
5
2013
Boosting haplotype inference with local search. Zbl 1142.92030
Lynce, Inês; Marques-Silva, João; Prestwich, Steve
5
2008
Satisfiability-based algorithms for Boolean optimization. Zbl 1068.90081
Manquinho, Vasco M.; Marques-Silva, João P.
5
2004
An overview of backtrack search satisfiability algorithms. Zbl 1010.68069
Lynce, Inês; Marques-Silva, João P.
5
2003
PySAT: A Python toolkit for prototyping with SAT oracles. Zbl 06916321
Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao
4
2018
Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing. Zbl 06512583
Arif, M. Fareed; Mencía, Carlos; Marques-Silva, Joao
4
2015
Algorithms for computing minimal equivalent subformulas. Zbl 1405.68340
Belov, Anton; Janota, Mikoláš; Lynce, Inês; Marques-Silva, Joao
4
2014
On computing preferred MUSes and MCSes. Zbl 1423.68460
Marques-Silva, Joao; Previti, Alessandro
4
2014
On QBF proofs and preprocessing. Zbl 1407.68454
Janota, Mikoláš; Grigore, Radu; Marques-Silva, Joao
4
2013
SAT-based preprocessing for MaxSAT. Zbl 1406.68108
Belov, Anton; Morgado, António; Marques-Silva, Joao
4
2013
Quantified maximum satisfiability: a core-guided approach. Zbl 1390.68598
Ignatiev, Alexey; Janota, Mikoláš; Marques-Silva, Joao
4
2013
Empirical study of the anatomy of modern SAT solvers. Zbl 1330.68271
Katebi, Hadi; Sakallah, Karem A.; Marques-Silva, João P.
4
2011
Counterexample guided abstraction refinement algorithm for propositional circumscription. Zbl 1306.68190
Janota, Mikoláš; Grigore, Radu; Marques-Silva, Joao
4
2010
Random backtracking in backtrack search algorithms for satisfiability. Zbl 1121.68109
Lynce, I.; Marques-Silva, J.
4
2007
Efficient data structures for backtrack search SAT solvers. Zbl 1099.68025
Lynce, Inês; Marques-Silva, João
4
2005
A SAT-based approach to learn explainable decision sets. Zbl 06958127
Ignatiev, Alexey; Pereira, Filipe; Narodytska, Nina; Marques-Silva, Joao
3
2018
Propositional SAT solving. Zbl 1392.68380
Marques-Silva, Joao; Malik, Sharad
3
2018
Minimal sets on propositional formulae. Problems and reductions. Zbl 1419.68098
Marques-Silva, Joao; Janota, Mikoláš; Mencía, Carlos
3
2017
Efficient reasoning for inconsistent Horn formulae. Zbl 06658170
Marques-Silva, Joao; Ignatiev, Alexey; Mencía, Carlos; Peñaloza, Rafael
3
2016
BEACON: an efficient SAT-based tool for debugging \({\mathcal {EL}}{^+}\) ontologies. Zbl 06623532
Arif, M. Fareed; Mencía, Carlos; Ignatiev, Alexey; Manthey, Norbert; Peñaloza, Rafael; Marques-Silva, Joao
3
2016
MaxSAT-based encodings for Group MaxSAT. Zbl 1373.68377
Heras, Federico; Morgado, Antonio; Marques-Silva, Joao
3
2015
Computing maximal autarkies with few and simple oracle queries. Zbl 06512570
Kullmann, Oliver; Marques-Silva, Joao
3
2015
On efficient computation of variable MUSes. Zbl 1273.03047
Belov, Anton; Ivrii, Alexander; Matsliah, Arie; Marques-Silva, Joao
3
2012
Efficient and accurate haplotype inference by combining parsimony and pedigree information. Zbl 1256.92037
Graça, Ana; Lynce, Inês; Marques-Silva, João; Oliveira, Arlindo L.
3
2012
Haplotype inference with pseudo-Boolean optimization. Zbl 1215.92043
Graça, Ana; Marques-Silva, João; Lynce, Inês; Oliveira, Arlindo L.
3
2011
On computing backbones of propositional theories. Zbl 1211.68389
Marques-Silva, Joao; Janota, Mikoláš; Lynce, Inês
3
2010
Theory and applications of satisfiability testing – SAT 2007. 10th international conference, Lisbon, Portugal, May 28–31, 2007. Proceedings. Zbl 1120.68007
Marques-Silva, João (ed.); Sakallah, Karem A. (ed.)
3
2007
Towards provably complete stochastic search algorithms for satisfiability. Zbl 1053.68684
Lynce, Ines; Baptista, Luís; Marques-Silva, João
3
2001
Efficient symmetry breaking for SAT-based minimum DFA inference. Zbl 1425.68240
Zakirzyanov, Ilya; Morgado, Antonio; Ignatiev, Alexey; Ulyantsev, Vladimir; Marques-Silva, Joao
2
2019
MCS extraction with sublinear oracle queries. Zbl 06623521
Mencía, Carlos; Ignatiev, Alexey; Previti, Alessandro; Marques-Silva, Joao
2
2016
SAT-based formula simplification. Zbl 06512580
Ignatiev, Alexey; Previti, Alessandro; Marques-Silva, Joao
2
2015
On reducing maximum independent set to minimum satisfiability. Zbl 1423.68452
Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao
2
2014
MUS extraction using clausal proofs. Zbl 1423.68436
Belov, Anton; Heule, Marijn J. H.; Marques-Silva, Joao
2
2014
PackUp: tools for package upgradability solving. Zbl 1348.68228
Janota, Mikoláš; Lynce, Inês; Manquinho, Vasco; Marques-Silva, Joao
2
2012
TG-Pro: A SAT-based ATPG system. Zbl 1331.68204
Chen, Huan; Marques-Silva, Joao
2
2012
Anatomy and empirical evaluation of modern SAT solvers. Zbl 1258.68137
Sakallah, Karem A.; Marques-Silva, Joao
2
2011
Minimally unsatisfiable Boolean circuits. Zbl 1330.68268
Belov, Anton; Marques-Silva, Joao
2
2011
Combinatorial optimization solutions for the maximum quartet consistency problem. Zbl 1214.68364
Morgado, António; Marques-Silva, Joao
2
2010
Model checking with Boolean satisfiability. Zbl 1151.68031
Marques-Silva, Joao
2
2008
Improvements to the implementation of interpolant-based model checking. Zbl 1159.68330
Marques-Silva, João
2
2005
Stochastic systematic search algorithms for satisfiability. Zbl 0990.90554
Lynce, Inês; Baptista, Luís; Marques-Silva, João
2
2001
Assessing heuristic machine learning explanations with model counting. Zbl 1441.68211
Narodytska, Nina; Shrotri, Aditya; Meel, Kuldeep S.; Ignatiev, Alexey; Marques-Silva, Joao
1
2019
DRMaxSAT with MaxHS: first contact. Zbl 1441.68232
Morgado, Antonio; Ignatiev, Alexey; Bonet, Maria Luisa; Marques-Silva, Joao; Buss, Sam
1
2019
Formally verifying the solution to the Boolean Pythagorean triples problem. Zbl 07100460
Cruz-Filipe, Luís; Marques-Silva, Joao; Schneider-Kamp, Peter
1
2019
Computing with SAT oracles: past, present and future. Zbl 06932479
Marques-Silva, Joao
1
2018
On tackling the limits of resolution in SAT solving. Zbl 06807225
Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao
1
2017
Quantified maximum satisfiability. Zbl 1334.90075
Ignatiev, Alexey; Janota, Mikoláš; Marques-Silva, Joao
1
2016
Maximal falsifiability. Definitions, algorithms, and applications. Zbl 1407.68453
Ignatiev, Alexey; Morgado, Antonio; Planes, Jordi; Marques-Silva, Joao
1
2013
Interpolant learning and reuse in SAT-based model checking. Zbl 1277.68140
Marques-Silva, Joao
1
2007
On using cutting planes in pseudo-Boolean optimization. Zbl 1177.90297
Manquinho, Vasco M.; Marques-Silva, João
1
2006
On applying cutting planes in DLL-based algorithms for pseudo-Boolean optimization. Zbl 1128.68474
Manquinho, Vasco; Marques-Silva, João
1
2005
Heuristic-based backtracking for propositional satisfiability. Zbl 1205.68370
Bhalla, A.; Lynce, I.; de Sousa, J. T.; Marques-Silva, J.
1
2003
Improving SAT algorithms by using search pruning techniques. Zbl 1067.68650
Lynce, Inês; Marques-Silva, João
1
2001
Efficient symmetry breaking for SAT-based minimum DFA inference. Zbl 1425.68240
Zakirzyanov, Ilya; Morgado, Antonio; Ignatiev, Alexey; Ulyantsev, Vladimir; Marques-Silva, Joao
2
2019
Assessing heuristic machine learning explanations with model counting. Zbl 1441.68211
Narodytska, Nina; Shrotri, Aditya; Meel, Kuldeep S.; Ignatiev, Alexey; Marques-Silva, Joao
1
2019
DRMaxSAT with MaxHS: first contact. Zbl 1441.68232
Morgado, Antonio; Ignatiev, Alexey; Bonet, Maria Luisa; Marques-Silva, Joao; Buss, Sam
1
2019
Formally verifying the solution to the Boolean Pythagorean triples problem. Zbl 07100460
Cruz-Filipe, Luís; Marques-Silva, Joao; Schneider-Kamp, Peter
1
2019
PySAT: A Python toolkit for prototyping with SAT oracles. Zbl 06916321
Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao
4
2018
A SAT-based approach to learn explainable decision sets. Zbl 06958127
Ignatiev, Alexey; Pereira, Filipe; Narodytska, Nina; Marques-Silva, Joao
3
2018
Propositional SAT solving. Zbl 1392.68380
Marques-Silva, Joao; Malik, Sharad
3
2018
Computing with SAT oracles: past, present and future. Zbl 06932479
Marques-Silva, Joao
1
2018
Minimal sets on propositional formulae. Problems and reductions. Zbl 1419.68098
Marques-Silva, Joao; Janota, Mikoláš; Mencía, Carlos
3
2017
On tackling the limits of resolution in SAT solving. Zbl 06807225
Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao
1
2017
Fast, flexible MUS enumeration. Zbl 1334.90080
Liffiton, Mark H.; Previti, Alessandro; Malik, Ammar; Marques-Silva, Joao
13
2016
Solving QBF with counterexample guided refinement. Zbl 1351.68254
Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund
8
2016
On the query complexity of selecting minimal sets for monotone predicates. Zbl 1351.68117
Janota, Mikoláš; Marques-Silva, Joao
6
2016
Efficient reasoning for inconsistent Horn formulae. Zbl 06658170
Marques-Silva, Joao; Ignatiev, Alexey; Mencía, Carlos; Peñaloza, Rafael
3
2016
BEACON: an efficient SAT-based tool for debugging \({\mathcal {EL}}{^+}\) ontologies. Zbl 06623532
Arif, M. Fareed; Mencía, Carlos; Ignatiev, Alexey; Manthey, Norbert; Peñaloza, Rafael; Marques-Silva, Joao
3
2016
MCS extraction with sublinear oracle queries. Zbl 06623521
Mencía, Carlos; Ignatiev, Alexey; Previti, Alessandro; Marques-Silva, Joao
2
2016
Quantified maximum satisfiability. Zbl 1334.90075
Ignatiev, Alexey; Janota, Mikoláš; Marques-Silva, Joao
1
2016
Expansion-based QBF solving versus Q-resolution. Zbl 1309.68168
Janota, Mikoláš; Marques-Silva, Joao
19
2015
Algorithms for computing backbones of propositional formulae. Zbl 1373.68379
Janota, Mikoláš; Lynce, Inês; Marques-Silva, Joao
9
2015
Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing. Zbl 06512583
Arif, M. Fareed; Mencía, Carlos; Marques-Silva, Joao
4
2015
MaxSAT-based encodings for Group MaxSAT. Zbl 1373.68377
Heras, Federico; Morgado, Antonio; Marques-Silva, Joao
3
2015
Computing maximal autarkies with few and simple oracle queries. Zbl 06512570
Kullmann, Oliver; Marques-Silva, Joao
3
2015
SAT-based formula simplification. Zbl 06512580
Ignatiev, Alexey; Previti, Alessandro; Marques-Silva, Joao
2
2015
MUSer2: an efficient MUS extractor. Zbl 1322.68178
Belov, Anton; Marques-Silva, Joao
9
2014
Progression in maximum satisfiability. Zbl 1366.68266
Ignatiev, A.; Morgado, A.; Manquinho, V.; Lynce, I.; Marques-Silva, J.
6
2014
Enumerating prime implicants of propositional formulae in conjunctive normal form. Zbl 1432.68327
Jabbour, Said; Marques-Silva, Joao; Sais, Lakhdar; Salhi, Yakoub
5
2014
Algorithms for computing minimal equivalent subformulas. Zbl 1405.68340
Belov, Anton; Janota, Mikoláš; Lynce, Inês; Marques-Silva, Joao
4
2014
On computing preferred MUSes and MCSes. Zbl 1423.68460
Marques-Silva, Joao; Previti, Alessandro
4
2014
On reducing maximum independent set to minimum satisfiability. Zbl 1423.68452
Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao
2
2014
MUS extraction using clausal proofs. Zbl 1423.68436
Belov, Anton; Heule, Marijn J. H.; Marques-Silva, Joao
2
2014
Iterative and core-guided maxsat solving: a survey and assessment. Zbl 1317.90199
Morgado, Antonio; Heras, Federico; Liffiton, Mark; Planes, Jordi; Marques-Silva, Joao
19
2013
On propositional QBF expansions and Q-resolution. Zbl 1390.03017
Janota, Mikoláš; Marques-Silva, Joao
8
2013
Formula preprocessing in MUS extraction. Zbl 1381.68146
Belov, Anton; Järvisalo, Matti; Marques-Silva, Joao
5
2013
On QBF proofs and preprocessing. Zbl 1407.68454
Janota, Mikoláš; Grigore, Radu; Marques-Silva, Joao
4
2013
SAT-based preprocessing for MaxSAT. Zbl 1406.68108
Belov, Anton; Morgado, António; Marques-Silva, Joao
4
2013
Quantified maximum satisfiability: a core-guided approach. Zbl 1390.68598
Ignatiev, Alexey; Janota, Mikoláš; Marques-Silva, Joao
4
2013
Maximal falsifiability. Definitions, algorithms, and applications. Zbl 1407.68453
Ignatiev, Alexey; Morgado, Antonio; Planes, Jordi; Marques-Silva, Joao
1
2013
Solving QBF with counterexample guided refinement. Zbl 1273.68178
Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund
20
2012
Towards efficient MUS extraction. Zbl 1248.68450
Belov, Anton; Lynce, Inês; Marques-Silva, Joao
14
2012
Improvements to core-guided binary search for MaxSAT. Zbl 1273.68357
Morgado, Antonio; Heras, Federico; Marques-Silva, Joao
7
2012
Computing minimally unsatisfiable subformulas: state of the art and future directions. Zbl 1394.68359
Marques-Silva, Joao
6
2012
Knowledge compilation with empowerment. Zbl 1302.68248
Bordeaux, Lucas; Marques-Silva, Joao
6
2012
On efficient computation of variable MUSes. Zbl 1273.03047
Belov, Anton; Ivrii, Alexander; Matsliah, Arie; Marques-Silva, Joao
3
2012
Efficient and accurate haplotype inference by combining parsimony and pedigree information. Zbl 1256.92037
Graça, Ana; Lynce, Inês; Marques-Silva, João; Oliveira, Arlindo L.
3
2012
PackUp: tools for package upgradability solving. Zbl 1348.68228
Janota, Mikoláš; Lynce, Inês; Manquinho, Vasco; Marques-Silva, Joao
2
2012
TG-Pro: A SAT-based ATPG system. Zbl 1331.68204
Chen, Huan; Marques-Silva, Joao
2
2012
Abstraction-based algorithm for 2QBF. Zbl 1330.68115
Janota, Mikoláš; Marques-Silva, Joao
11
2011
Boolean lexicographic optimization: algorithms & applications. Zbl 1242.90199
Marques-Silva, Joao; Argelich, Josep; Graça, Ana; Lynce, Inês
8
2011
On improving MUS extraction algorithms. Zbl 1330.68273
Marques-Silva, Joao; Lynce, Ines
6
2011
Empirical study of the anatomy of modern SAT solvers. Zbl 1330.68271
Katebi, Hadi; Sakallah, Karem A.; Marques-Silva, João P.
4
2011
Haplotype inference with pseudo-Boolean optimization. Zbl 1215.92043
Graça, Ana; Marques-Silva, João; Lynce, Inês; Oliveira, Arlindo L.
3
2011
Anatomy and empirical evaluation of modern SAT solvers. Zbl 1258.68137
Sakallah, Karem A.; Marques-Silva, Joao
2
2011
Minimally unsatisfiable Boolean circuits. Zbl 1330.68268
Belov, Anton; Marques-Silva, Joao
2
2011
Counterexample guided abstraction refinement algorithm for propositional circumscription. Zbl 1306.68190
Janota, Mikoláš; Grigore, Radu; Marques-Silva, Joao
4
2010
On computing backbones of propositional theories. Zbl 1211.68389
Marques-Silva, Joao; Janota, Mikoláš; Lynce, Inês
3
2010
Combinatorial optimization solutions for the maximum quartet consistency problem. Zbl 1214.68364
Morgado, António; Marques-Silva, Joao
2
2010
Algorithms for weighted Boolean optimization. Zbl 1247.68258
Manquinho, Vasco; Marques-Silva, Joao; Planes, Jordi
20
2009
A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Zbl 1181.90291
Liffiton, Mark; Mneimneh, Maher; Lynce, Inês; Andraus, Zaher; Marques-Silva, João; Sakallah, Karem
6
2009
Towards more effective unsatisfiability-based maximum satisfiability algorithms. Zbl 1138.68548
Marques-Silva, Joao; Manquinho, Vasco
6
2008
Boosting haplotype inference with local search. Zbl 1142.92030
Lynce, Inês; Marques-Silva, João; Prestwich, Steve
5
2008
Model checking with Boolean satisfiability. Zbl 1151.68031
Marques-Silva, Joao
2
2008
Towards robust CNF encodings of cardinality constraints. Zbl 1145.68525
Marques-Silva, Joao; Lynce, Inês
8
2007
Efficient haplotype inference with pseudo-Boolean optimization. Zbl 1126.92035
Graça, Ana; Marques-Silva, João; Lynce, Inês; Oliveira, Arlindo L.
6
2007
Random backtracking in backtrack search algorithms for satisfiability. Zbl 1121.68109
Lynce, I.; Marques-Silva, J.
4
2007
Theory and applications of satisfiability testing – SAT 2007. 10th international conference, Lisbon, Portugal, May 28–31, 2007. Proceedings. Zbl 1120.68007
Marques-Silva, João (ed.); Sakallah, Karem A. (ed.)
3
2007
Interpolant learning and reuse in SAT-based model checking. Zbl 1277.68140
Marques-Silva, Joao
1
2007
Categorisation of clauses in conjunctive normal forms: minimally unsatisfiable sub-clause-sets and the lean kernel. Zbl 1187.68552
Kullmann, Oliver; Lynce, Inês; Marques-Silva, João
12
2006
On using cutting planes in pseudo-Boolean optimization. Zbl 1177.90297
Manquinho, Vasco M.; Marques-Silva, João
1
2006
A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. Zbl 1128.68477
Mneimneh, Maher; Lynce, Inês; Andraus, Zaher; Marques-Silva, João; Sakallah, Karem
8
2005
Efficient data structures for backtrack search SAT solvers. Zbl 1099.68025
Lynce, Inês; Marques-Silva, João
4
2005
Improvements to the implementation of interpolant-based model checking. Zbl 1159.68330
Marques-Silva, João
2
2005
On applying cutting planes in DLL-based algorithms for pseudo-Boolean optimization. Zbl 1128.68474
Manquinho, Vasco; Marques-Silva, João
1
2005
Satisfiability-based algorithms for Boolean optimization. Zbl 1068.90081
Manquinho, Vasco M.; Marques-Silva, João P.
5
2004
An overview of backtrack search satisfiability algorithms. Zbl 1010.68069
Lynce, Inês; Marques-Silva, João P.
5
2003
Heuristic-based backtracking for propositional satisfiability. Zbl 1205.68370
Bhalla, A.; Lynce, I.; de Sousa, J. T.; Marques-Silva, J.
1
2003
Towards provably complete stochastic search algorithms for satisfiability. Zbl 1053.68684
Lynce, Ines; Baptista, Luís; Marques-Silva, João
3
2001
Stochastic systematic search algorithms for satisfiability. Zbl 0990.90554
Lynce, Inês; Baptista, Luís; Marques-Silva, João
2
2001
Improving SAT algorithms by using search pruning techniques. Zbl 1067.68650
Lynce, Inês; Marques-Silva, João
1
2001
Using randomization and learning to solve hard real-world instances of satisfiability. Zbl 1044.68736
Baptista, Luís; Marques-Silva, João
11
2000
Algebraic simplification techniques for propositional satisfiability. Zbl 1044.68781
Marques-Silva, João
8
2000
GRASP: a search algorithm for propositional satisfiability. Zbl 1392.68388
Marques-Silva, João P.; Sakallah, Karem A.
86
1999
all top 5

Cited by 505 Authors

27 Marques-Silva, João P.
11 Beyersdorff, Olaf
10 Lynce, Inês
9 Biere, Armin
9 Janota, Mikoláš
7 Heule, Marijn J. H.
7 Järvisalo, Matti
7 Szeider, Stefan
6 Ansótegui, Carlos
6 Ignatyev, Alexey A.
6 Lonsing, Florian
6 Maratea, Marco
6 Mencía, Carlos
6 Nieuwenhuis, Robert
5 Chew, Leroy
5 Dodaro, Carmine
5 Gebser, Martin
5 Liffiton, Mark H.
5 Oliveras, Albert
5 Peñaloza, Rafael
5 Previti, Alessandro
5 Rodríguez-Carbonell, Enric
5 Seidl, Martina
5 Semenov, Aleksandr Anatol’evich
4 Blinkhorn, Joshua
4 Giunchiglia, Enrico
4 Kullmann, Oliver
4 Lauria, Massimo
4 Nordström, Jakob
4 Ricca, Francesco
4 Schaub, Torsten H.
3 Ábrahám, Erika
3 Alviano, Mario
3 Amendola, Giovanni
3 Cai, Shaowei
3 Egly, Uwe
3 Fichte, Johannes Klaus
3 Gabàs, Joel
3 Grégoire, Éric
3 Hinde, Luke
3 Ivrii, Alexander
3 Janhunen, Tomi
3 Kaufmann, Benjamin
3 Kiesl, Benjamin
3 Lagniez, Jean-Marie
3 Levy, Jordi
3 Mahajan, Meena
3 Manquinho, Vasco M.
3 Marquis, Pierre
3 Mazure, Bertrand
3 Piette, Cédric
3 Planes, Jordi
3 Ryvchin, Vadim
3 Sakallah, Karem A.
3 Şhukla, Anil K.
3 Silva Coelho, José
3 Slivovsky, Friedrich
3 Strichman, Ofer
3 Vanhoucke, Mario
3 Vardi, Moshe Y.
3 Wallner, Johannes Peter
2 Alves Rocha, Thiago
2 Argelich, Josep
2 Arif, M. Fareed
2 Asín, Roberto
2 Balabanov, Valeriy
2 Banbara, Mutsunori
2 Becker, Bernd
2 Belov, Anton
2 Berg, Jeremias
2 Bofill, Miquel
2 Bruni, Renato
2 Bryant, Randal E.
2 de Moura, Leonardo
2 Dechter, Rina
2 Deters, Morgan
2 Dvořák, Wolfgang
2 Goldberg, Eugene L.
2 Graça, Ana
2 Griggio, Alberto
2 Hamadi, Youssef
2 Jäger, Gerold
2 Jiang, Jie-Hong Roland
2 Jovanović, Dejan
2 Kremer, Gereon
2 Kučera, Petr
2 Kuncak, Viktor
2 Larrosa, Javier
2 Lierler, Yuliya
2 Luo, Chuan
2 Malik, Sharad
2 Marić, Filip
2 Martins Ferreira, Francicleber
2 Martins, Ana Teresa
2 Martins, Ruben
2 Otpuschennikov, Ilya V.
2 Peitl, Tomáš
2 Prestwich, Steven D.
2 Rabe, Markus N.
2 Reynolds, Andrew
...and 405 more Authors
all top 5

Cited in 63 Serials

33 Artificial Intelligence
19 Journal of Automated Reasoning
18 Constraints
11 Discrete Applied Mathematics
11 Theoretical Computer Science
10 Formal Methods in System Design
10 Theory and Practice of Logic Programming
9 Annals of Mathematics and Artificial Intelligence
5 Information Processing Letters
4 Journal of Symbolic Computation
4 Annals of Operations Research
4 The Journal of Artificial Intelligence Research (JAIR)
4 Logical Methods in Computer Science
3 Journal of Computer and System Sciences
3 SIAM Journal on Computing
3 Computers & Operations Research
3 European Journal of Operational Research
3 ACM Transactions on Computational Logic
3 Journal of Discrete Algorithms
2 Acta Informatica
2 Information and Computation
2 The Bulletin of Symbolic Logic
2 Journal of Heuristics
2 Discrete Optimization
2 Journal of Logical and Algebraic Methods in Programming
2 Prikladnaya Diskretnaya Matematika
1 Journal of the Franklin Institute
1 Mathematical Biosciences
1 Applied Mathematics and Computation
1 Fuzzy Sets and Systems
1 Information Sciences
1 Journal of Computational and Applied Mathematics
1 Journal of Optimization Theory and Applications
1 Mathematical Social Sciences
1 Annals of Pure and Applied Logic
1 Journal of Computer Science and Technology
1 Algorithmica
1 International Journal of Approximate Reasoning
1 Automation and Remote Control
1 Applicable Algebra in Engineering, Communication and Computing
1 Journal of the Egyptian Mathematical Society
1 Top
1 International Transactions in Operational Research
1 INFORMS Journal on Computing
1 Mathematical Problems in Engineering
1 Theory of Computing Systems
1 Journal of Combinatorial Optimization
1 Communications in Nonlinear Science and Numerical Simulation
1 International Journal of Applied Mathematics and Computer Science
1 Journal of Applied Mathematics
1 Journal of Machine Learning Research (JMLR)
1 OR Spectrum
1 Natural Computing
1 JMMA. Journal of Mathematical Modelling and Algorithms
1 ACM Journal of Experimental Algorithmics
1 Computational Management Science
1
1 Electronic Notes in Theoretical Computer Science
1 Mathematics in Computer Science
1 Optimization Letters
1 Acta Universitatis Sapientiae. Informatica
1 Theory of Computing
1 Statistics and Computing

Citations by Year