Search results for "Satisfiability"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
12	Rémi Brochenin, Stéphane Demri, Étienne Lozes	Reasoning About Sequences of Memory States.	LFCS	2007	DBLP DOI BibTeX RDF
12	Henrik Björklund, Wim Martens, Thomas Schwentick	Conjunctive Query Containment over Trees.	DBPL	2007	DBLP DOI BibTeX RDF
12	Enrico Giunchiglia, Marco Maratea	SAT-Based Planning with Minimal-#actions Plans and "soft" Goals.	AI*IA	2007	DBLP DOI BibTeX RDF
12	Roberto Sebastiani	From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain.	FroCoS	2007	DBLP DOI BibTeX RDF
12	Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli	Noetherianity and Combination Problems.	FroCoS	2007	DBLP DOI BibTeX RDF
12	Fabio Martinelli, Ilaria Matteucci	Synthesis of Web Services Orchestrators in a Timed Setting.	WS-FM	2007	DBLP DOI BibTeX RDF
12	Ryan Williams 0001	Inductive Time-Space Lower Bounds for Sat and Related Problems.	Comput. Complex.	2006	DBLP DOI BibTeX RDF	68Q17, Subject classification
12	Pierre Genevès, Nabil Layaïda	A system for the static analysis of XPath.	ACM Trans. Inf. Syst.	2006	DBLP DOI BibTeX RDF	XML, query, logic, XPath, equivalence, Containment
12	Paola Festa, Panos M. Pardalos, Leonidas S. Pitsoulis, Mauricio G. C. Resende	GRASP with path relinking for the weighted MAXSAT problem.	ACM J. Exp. Algorithmics	2006	DBLP DOI BibTeX RDF	time-to-target plots, performance, Algorithms, heuristics, experimentation, GRASP, path relinking
12	Rajeev Joshi, Greg Nelson, Yunhong Zhou	Denali: A practical algorithm for generating optimal code.	ACM Trans. Program. Lang. Syst.	2006	DBLP DOI BibTeX RDF	practical optimal code generation, Compilation, code generation
12	Martin Sachenbacher, Brian C. Williams	Conflict-Directed A* Search for Soft Constraints.	CPAIOR	2006	DBLP DOI BibTeX RDF
12	Dimitri Theodoratos, Stefanos Souldatos, Theodore Dalamagas 0001, Pawel Placek, Timos K. Sellis	Heuristic containment check of partial tree-pattern queries in the presence of index graphs.	CIKM	2006	DBLP DOI BibTeX RDF	partial tree-pattern query, query containment, tree-structured data
12	Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani	To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF ÈT).	LPAR	2006	DBLP DOI BibTeX RDF
12	Laura Bozzelli, Régis Gascon	Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints.	LPAR	2006	DBLP DOI BibTeX RDF
12	Grigore Rosu, Saddek Bensalem	Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis.	CAV	2006	DBLP DOI BibTeX RDF
12	Alessandro Armando, Jacopo Mantovani, Lorenzo Platania	Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers.	SPIN	2006	DBLP DOI BibTeX RDF
12	Mira Balaban, Azzam Maraee	Consistency of UML Class Diagrams with Hierarchy Constraints.	NGITS	2006	DBLP DOI BibTeX RDF
12	Rafiq Muhammad 0006, Peter J. Stuckey	A Stochastic Non-CNF SAT Solver.	PRICAI	2006	DBLP DOI BibTeX RDF
12	Vladimir V. Rybakov	Linear Temporal Logic with Until and Before on Integer Numbers, Deciding Algorithms.	CSR	2006	DBLP DOI BibTeX RDF	consecutions, admissible rules, algorithms, inference rules, linear temporal logic, logic in computer science, logical consequence
12	Stéphane Demri, Denis Lugiez	Presburger Modal Logic Is PSPACE-Complete.	IJCAR	2006	DBLP DOI BibTeX RDF
12	Alessandro Cimatti, Roberto Sebastiani	Building Efficient Decision Procedures on Top of SAT Solvers.	SFM	2006	DBLP DOI BibTeX RDF
12	Evgeny Dantsin, Edward A. Hirsch, Alexander Wolpert	Clause Shortening Combined with Pruning Yields a New Upper Bound for Deterministic SAT Algorithms.	CIAC	2006	DBLP DOI BibTeX RDF
12	Alexander Metzner, Christian Herde	RTSAT-- An Optimal and Efficient Approach to the Task Allocation Problem in Distributed Architectures.	RTSS	2006	DBLP DOI BibTeX RDF
12	Joël Ouaknine, James Worrell 0001	Safety Metric Temporal Logic Is Fully Decidable.	TACAS	2006	DBLP DOI BibTeX RDF
12	Fadi A. Aloul, Assim Sagahyroon	Estimation of the weighted maximum switching activity in combinational CMOS circuits.	ISCAS	2006	DBLP DOI BibTeX RDF
12	Aline Paes, Filip Zelezný, Gerson Zaverucha, C. David Page Jr., Ashwin Srinivasan 0001	ILP Through Propositionalization and Stochastic k-Term DNF Learning.	ILP	2006	DBLP DOI BibTeX RDF
12	Éric Grégoire, Bertrand Mazure, Cédric Piette	Tracking MUSes and Strict Inconsistent Covers.	FMCAD	2006	DBLP DOI BibTeX RDF
12	Hyondeuk Kim, Fabio Somenzi	Finite Instantiations for Integer Difference Logic.	FMCAD	2006	DBLP DOI BibTeX RDF
12	Javier Álvez, Paqui Lucio	Equational Constraint Solving Via a Restricted Form of Universal Quantification.	FoIKS	2006	DBLP DOI BibTeX RDF	constraint satisfaction, equality, solver, answer, term algebra
12	Ranko Lazic 0001	Safely Freezing LTL.	FSTTCS	2006	DBLP DOI BibTeX RDF
12	Wiebe van der Hoek, Alessio Lomuscio, Michael J. Wooldridge	On the complexity of practical ATL model checking.	AAMAS	2006	DBLP DOI BibTeX RDF	verification, complexity, cooperation, logic
12	Rajeev Alur, P. Madhusudan, Wonhong Nam	Symbolic computational techniques for solving games.	Int. J. Softw. Tools Technol. Transf.	2005	DBLP DOI BibTeX RDF	QBF solving, Games, Formal verification, Symbolic model checking, Bounded model checking
12	Johan van Benthem	Guards, Bounds, and Generalized Semantics.	J. Log. Lang. Inf.	2005	DBLP DOI BibTeX RDF
12	Stéphane Demri, Hans de Nivelle	Deciding Regular Grammar Logics with Converse Through First-Order Logic.	J. Log. Lang. Inf.	2005	DBLP DOI BibTeX RDF	relational translation, 2-variable fragment, guarded fragment, modal and temporal logics
12	Ian Pratt-Hartmann	Complexity of the Two-Variable Fragment with Counting Quantifiers.	J. Log. Lang. Inf.	2005	DBLP DOI BibTeX RDF	Abstract two-variable fragment, counting quantifiers, complexity, logic
12	Andreas Meier 0002, Volker Sorge	Applying SAT Solving in Classification of Finite Algebras.	J. Autom. Reason.	2005	DBLP DOI BibTeX RDF	application of SAT, finite algebra, mathematics
12	Allen Van Gelder	Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning.	LPAR	2005	DBLP DOI BibTeX RDF
12	Mikhail Sheremet, Dmitry Tishkovsky, Frank Wolter, Michael Zakharyaschev	Comparative Similarity, Tree Automata, and Diophantine Equations.	LPAR	2005	DBLP DOI BibTeX RDF
12	Dalila Boughaci, Habiba Drias	Efficient and Experimental Meta-heuristics for MAX-SAT Problems.	WEA	2005	DBLP DOI BibTeX RDF
12	Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah	Dynamic symmetry-breaking for improved Boolean optimization.	ASP-DAC	2005	DBLP DOI BibTeX RDF
12	Martin Allen	Complexity results for logics of local reasoning and inconsistent belief.	TARK	2005	DBLP BibTeX RDF
12	Zaiyue Zhang, Yuefei Sui, Cungen Cao 0001	Description of Fuzzy First-Order Modal Logic Based on Constant Domain Semantics.	RSFDGrC (1)	2005	DBLP DOI BibTeX RDF	fuzzy reasoning system, rough set, modal logic
12	Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz 0001, Roberto Sebastiani	The MathSAT 3 System.	CADE	2005	DBLP DOI BibTeX RDF
12	Loganathan Lingappan, Niraj K. Jha	Unsatisfiability Based Efficient Design for Testability Solution for Register-Transfer Level Circuits.	VTS	2005	DBLP DOI BibTeX RDF
12	Emanuel Kieronski	Results on the Guarded Fragment with Equivalence or Transitive Relations.	CSL	2005	DBLP DOI BibTeX RDF
12	Balder ten Cate, Massimo Franceschet	On the Complexity of Hybrid Logics with Binders.	CSL	2005	DBLP DOI BibTeX RDF
12	Mohamed El-bachir Menai, Mohamed Batouche	A Backbone-Based Co-evolutionary Heuristic for Partial MAX-SAT.	Artificial Evolution	2005	DBLP DOI BibTeX RDF
12	Gi-Joon Nam, Fadi A. Aloul, Karem A. Sakallah, Rob A. Rutenbar	A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints.	IEEE Trans. Computers	2004	DBLP DOI BibTeX RDF
12	Jennifer L. Wong, Gang Qu 0001, Miodrag Potkonjak	Optimization-intensive watermarking techniques for decision problems.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	2004	DBLP DOI BibTeX RDF
12	Lefteris M. Kirousis, Phokion G. Kolaitis	A Dichotomy in the Complexity of Propositional Circumscription.	Theory Comput. Syst.	2004	DBLP DOI BibTeX RDF
12	Agostino Dovier, Carla Piazza, Enrico Pontelli	Disunification in ACI1 Theories.	Constraints An Int. J.	2004	DBLP DOI BibTeX RDF	disunification, ACI, complexity, sets, equational theories, CLP
12	Ian Pratt-Hartmann	Fragments of Language.	J. Log. Lang. Inf.	2004	DBLP DOI BibTeX RDF	decidable fragments, computational complexity, semantics, logic
12	Calogero G. Zarba, Domenico Cantone, Jacob T. Schwartz	A Decision Procedure for a Sublanguage of Set Theory Involving Monotone, Additive, and Multiplicative Functions, I: The Two-Level Case.	J. Autom. Reason.	2004	DBLP DOI BibTeX RDF	Nelson-Oppen procedure, set theory, decision procedure
12	Dalila Boughaci, Habiba Drias	Solving weighted Max-Sat optimization problems using a Taboo Scatter Search metaheuristic.	SAC	2004	DBLP DOI BibTeX RDF	Max-W-Sat, Solution combination method, SAT, Scatter search, Hybrid metaheuristic, Taboo Search
12	Yinglong Ma, Jun Wei 0001, Beihong Jin, Shaohua Liu	A Formal Framework for Ontology Integration Based on a Default Extension to DDL.	ICTAC	2004	DBLP DOI BibTeX RDF	distributed description logics, default extension, Tableau algorithm, Ontology integration, semantic query
12	Carles Farré, Ernest Teniente, Toni Urpí	A New Approach for Checking Schema Validation Properties.	DEXA	2004	DBLP DOI BibTeX RDF
12	Stéphane Demri	LTL over Integer Periodicity Constraints: (Extended Abstract).	FoSSaCS	2004	DBLP DOI BibTeX RDF
12	Yinglong Ma, Jun Wei 0001	A Default Extension to Distributed Description Logics.	IAT	2004	DBLP DOI BibTeX RDF
12	Carlos Ansótegui, Ramón Béjar, Alba Cabiscol, Felip Manyà	The Interface between P and NP in Signed CNF Formulas.	ISMVL	2004	DBLP DOI BibTeX RDF
12	Alessandro Artale	Reasoning on Temporal Conceptual Schemas with Dynamic Constraints.	TIME	2004	DBLP DOI BibTeX RDF
12	Yevgeny Kazakov	A Polynomial Translation from the Two-Variable Guarded Fragment with Number Restrictions to the Guarded Fragment.	JELIA	2004	DBLP DOI BibTeX RDF
12	Bart Selman	Algorithmic Adventures at the Interface of Computer Science, Statistical Physics, and Combinatorics.	CP	2004	DBLP DOI BibTeX RDF
12	Alessandro Cimatti, Marco Roveri, Daniel Sheridan	Bounded Verification of Past LTL.	FMCAD	2004	DBLP DOI BibTeX RDF
12	Volker Diekert, Paul Gastin	Pure Future Local Temporal Logics Are Expressively Complete for Mazurkiewicz Traces.	LATIN	2004	DBLP DOI BibTeX RDF	concurrency, Temporal logics, Mazurkiewicz traces
12	David Déharbe, Abdessamad Imine, Silvio Ranise	Abstraction-Driven Verification of Array Programs.	AISC	2004	DBLP DOI BibTeX RDF
12	Xiaoyu Song, William N. N. Hung, Alan Mishchenko, Malgorzata Chrzanowska-Jeske, Andrew A. Kennings, Alan J. Coppola	Board-level multiterminal net assignment for the partial cross-bar architecture.	IEEE Trans. Very Large Scale Integr. Syst.	2003	DBLP DOI BibTeX RDF
12	Anuj Goel, Khurram Sajid, Hai Zhou 0001, Adnan Aziz, Vigyan Singhal	BDD Based Procedures for a Theory of Equality with Uninterpreted Functions.	Formal Methods Syst. Des.	2003	DBLP DOI BibTeX RDF	logic of equality, BDDs, uninterpreted functions
12	Alessandro Armando, Luca Compagna, Pierre Ganty	SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis.	FME	2003	DBLP DOI BibTeX RDF	SAT encodings, security protocols, bounded model-checking, SAT-solvers
12	Helmut Seidl, Thomas Schwentick, Anca Muscholl	Numerical document queries.	PODS	2003	DBLP DOI BibTeX RDF	querying XML documents, XML, automata, monadic second order logic, Presburger arithmetic
12	Jean-Claude Fernandez, Laurent Mounier, Cyril Pachon	Property Oriented Test Case Generation.	FATES	2003	DBLP DOI BibTeX RDF
12	K. Subramani 0001	On Clausal Equivalence and Hull Inclusion.	ICTCS	2003	DBLP DOI BibTeX RDF
12	Jan Hladik, Ulrike Sattler	A Translation of Looping Alternating Automata into Description Logics.	CADE	2003	DBLP DOI BibTeX RDF
12	Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar	On the Universal and Existential Fragments of the µ-Calculus.	TACAS	2003	DBLP DOI BibTeX RDF
12	Massimo Franceschet, Maarten de Rijke, Bernd-Holger Schlingloff	Hybrid Logics on Linear Structures: Expressivity and Complexity.	TIME	2003	DBLP DOI BibTeX RDF
12	Tim French 0002	Quantified Propositional Temporal Logic with Repeating States.	TIME	2003	DBLP DOI BibTeX RDF
12	Lengning Liu, Miroslaw Truszczynski	Local-Search Techniques for Propositional Logic Extended with Cardinality Constraints.	CP	2003	DBLP DOI BibTeX RDF
12	Tim French 0002	Decidability of Propositionally Quantified Logics of Knowledge.	Australian Conference on Artificial Intelligence	2003	DBLP DOI BibTeX RDF
12	Emil Gizdarski, Hideo Fujiwara	SPIRIT: a highly robust combinational test generation algorithm.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	2002	DBLP DOI BibTeX RDF
12	Colin Cooper, Alan M. Frieze, Gregory B. Sorkin	A note on random 2-SAT with prescribed literal degrees.	SODA	2002	DBLP BibTeX RDF
12	Yannis Dimopoulos, Andreas Sideris	Towards Local Search for Answer Sets.	ICLP	2002	DBLP DOI BibTeX RDF
12	Carlos Areces, Juan Heguiabehere	HyLoRes 1.0: Direct Resolution for Hybrid Logics.	CADE	2002	DBLP DOI BibTeX RDF
12	Jan Hladik	Implementation and Optimisation of a Tableau Algorithm for the Guarded Fragment.	TABLEAUX	2002	DBLP DOI BibTeX RDF
12	Calogero G. Zarba	A Tableau Calculus for Combining Non-disjoint Theories.	TABLEAUX	2002	DBLP DOI BibTeX RDF
12	Marta Cialdea Mayer, Carla Limongelli	Linear Time Logic, Conditioned Models, and Planning with Incomplete Knowledge.	TABLEAUX	2002	DBLP DOI BibTeX RDF
12	Inman P. de Guzmán, Manuel Ojeda-Aciego, Agustín Valverde	Restricted Delta-Trees in Multiple-Valued Logics.	AIMSA	2002	DBLP DOI BibTeX RDF	Knowledge Representation, Automated Reasoning
12	Robert Seater, David Wonnacott	Efficient Manipulation of Disequalities During Dependence Analysis.	LCPC	2002	DBLP DOI BibTeX RDF
12	Carlos Ansótegui, Felip Manyà	Bridging the Gap between SAT and CSP.	CP	2002	DBLP DOI BibTeX RDF
12	Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani	Bounded Model Checking for Timed Systems.	FORTE	2002	DBLP DOI BibTeX RDF
12	Vijay Ganesh, Sergey Berezin, David L. Dill	Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods.	FMCAD	2002	DBLP DOI BibTeX RDF
12	Michael Molloy 0001	Models and thresholds for random constraint satisfaction problems.	STOC	2002	DBLP DOI BibTeX RDF	sharp thresholds
12	Inman P. de Guzmán, Manuel Ojeda-Aciego, Agustín Valverde	Restricted Delta-Trees and Reduction Theorems in Multiple-Valued Logics.	IBERAMIA	2002	DBLP DOI BibTeX RDF
12	Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna	A proof engine approach to solving combinational design automation problems.	DAC	2002	DBLP DOI BibTeX RDF
12	Olena Kravchuk, Wayne J. Pullan, John Thornton 0001, Abdul Sattar 0001	An Investigation of Variable Relationships in 3-SAT Problems.	Australian Joint Conference on Artificial Intelligence	2002	DBLP DOI BibTeX RDF	Search, Constraints
12	Volker Diekert, Paul Gastin	Local Temporal Logic is Expressively Complete for Cograph Dependence Alphabets.	LPAR	2001	DBLP DOI BibTeX RDF	concurrency, Temporal logics, Mazurkiewicz traces
12	Fady Copty, Limor Fix, Ranan Fraer, Enrico Giunchiglia, Gila Kamhi, Armando Tacchella, Moshe Y. Vardi	Benefits of Bounded Model Checking at an Industrial Setting.	CAV	2001	DBLP DOI BibTeX RDF
12	Yoav Rodeh, Ofer Strichman	Finite Instantiations in Equivalence Logic with Uninterpreted Functions.	CAV	2001	DBLP DOI BibTeX RDF
12	Daniel Kirsten	Alternating Tree Automata and Parity Games.	Automata, Logics, and Infinite Games	2001	DBLP DOI BibTeX RDF
12	Klaus Reinhardt	The Complexity of Translating Logic to Finite Automata.	Automata, Logics, and Infinite Games	2001	DBLP DOI BibTeX RDF
12	Anatoli Degtyarev, Michael Fisher 0001	Towards First-Order Temporal Resolution.	KI/ÖGAI	2001	DBLP DOI BibTeX RDF
12	Carsten Lutz, Ulrike Sattler, Frank Wolter	Modal Logic and the Two-Variable Fragment.	CSL	2001	DBLP DOI BibTeX RDF