Acceder

Bibliografías temáticas / Satisfiability theory / Artículos de revistas

Artículos de revistas sobre el tema "Satisfiability theory"

Siga este enlace para ver otros tipos de publicaciones sobre el tema: Satisfiability theory.

Autor: Grafiati

Publicado: 11 de marzo de 2023

Crea una cita precisa en los estilos APA, MLA, Chicago, Harvard y otros

Elija tipo de fuente:

Consulte los 50 mejores artículos de revistas para su investigación sobre el tema "Satisfiability theory".

Junto a cada fuente en la lista de referencias hay un botón "Agregar a la bibliografía". Pulsa este botón, y generaremos automáticamente la referencia bibliográfica para la obra elegida en el estilo de cita que necesites: APA, MLA, Harvard, Vancouver, Chicago, etc.

También puede descargar el texto completo de la publicación académica en formato pdf y leer en línea su resumen siempre que esté disponible en los metadatos.

Explore artículos de revistas sobre una amplia variedad de disciplinas y organice su bibliografía correctamente.

1

Dixon, H. E., M. L. Ginsberg, E. M. Luks y A. J. Parkes. "Generalizing Boolean Satisfiability II: Theory". Journal of Artificial Intelligence Research 22 (1 de diciembre de 2004): 481–534. http://dx.doi.org/10.1613/jair.1555.

Texto completo

Resumen

This is the second of three planned papers describing ZAP, a satisfiability engine that substantially generalizes existing tools while retaining the performance characteristics of modern high performance solvers. The fundamental idea underlying ZAP is that many problems passed to such engines contain rich internal structure that is obscured by the Boolean representation used; our goal is to define a representation in which this structure is apparent and can easily be exploited to improve computational performance. This paper presents the theoretical basis for the ideas underlying ZAP, arguing that existing ideas in this area exploit a single, recurring structure in that multiple database axioms can be obtained by operating on a single axiom using a subgroup of the group of permutations on the literals in the problem. We argue that the group structure precisely captures the general structure at which earlier approaches hinted, and give numerous examples of its use. We go on to extend the Davis-Putnam-Logemann-Loveland inference procedure to this broader setting, and show that earlier computational improvements are either subsumed or left intact by the new method. The third paper in this series discusses ZAP's implementation and presents experimental performance results.

Los estilos APA, Harvard, Vancouver, ISO, etc.

2

Michaliszyn, Jakub, Jan Otop y Piotr Witkowski. "Satisfiability versus Finite Satisfiability in Elementary Modal Logics". Fundamenta Informaticae 163, n.º 2 (3 de noviembre de 2018): 165–88. http://dx.doi.org/10.3233/fi-2018-1736.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

3

Utomo, Putranto. "Satisfiability modulo theory and binary puzzle". Journal of Physics: Conference Series 855 (junio de 2017): 012057. http://dx.doi.org/10.1088/1742-6596/855/1/012057.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

4

Preto, Sandro Márcio da Silva. "Semantics modulo satisfiability with applications: function representation, probabilities and game theory". Bulletin of Symbolic Logic 28, n.º 2 (junio de 2022): 264–65. http://dx.doi.org/10.1017/bsl.2022.2.

Texto completo

Resumen

AbstractIn the context of propositional logics, we apply semantics modulo satisfiability—a restricted semantics which comprehends only valuations that satisfy some specific set of formulas—with the aim to efficiently solve some computational tasks. Three possible such applications are developed.We begin by studying the possibility of implicitly representing rational McNaughton functions in Łukasiewicz Infinitely-valued Logic through semantics modulo satisfiability. We theoretically investigate some approaches to such representation concept, called representation modulo satisfiability, and describe a polynomial algorithm that builds representations in the newly introduced system. An implementation of the algorithm, test results and ways to randomly generate rational McNaughton functions for testing are presented. Moreover, we propose an application of such representations to the formal verification of properties of neural networks by means of the reasoning framework of Łukasiewicz Infinitely-valued Logic.Then, we move to the investigation of the satisfiability of joint probabilistic assignments to formulas of Łukasiewicz Infinitely-valued Logic, which is known to be an NP-complete problem. We provide an exact decision algorithm derived from the combination of linear algebraic methods with semantics modulo satisfiability. Also, we provide an implementation for such algorithm for which the phenomenon of phase transition is empirically detected.Lastly, we study the game theory situation of observable games, which are games that are known to reach a Nash equilibrium, however, an external observer does not know what is the exact profile of actions that occur in a specific instance; thus, such observer assigns subjective probabilities to players actions. We study the decision problem of determining if a set of these probabilistic constraints is coherent by reducing it to the problems of satisfiability of probabilistic assignments to logical formulas both in Classical Propositional Logic and Łukasiewicz Infinitely-valued Logic depending on whether only pure equilibria or also mixed equilibria are allowed. Such reductions rely upon the properties of semantics modulo satisfiability. We provide complexity and algorithmic discussion for the coherence problem and, also, for the problem of computing maximal and minimal probabilistic constraints on actions that preserves coherence.Abstract prepared by Sandro Márcio da Silva Preto.E-mail: spreto@ime.usp.brURL:https://doi.org/10.11606/T.45.2021.tde-17062021-163257

Los estilos APA, Harvard, Vancouver, ISO, etc.

5

Alon, Noga y Asaf Shapira. "Testing satisfiability". Journal of Algorithms 47, n.º 2 (julio de 2003): 87–103. http://dx.doi.org/10.1016/s0196-6774(03)00019-1.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

6

Liao, Xiaojuan, Hui Zhang, Miyuki Koshimura, Rong Huang, Wenxin Yu y Fagen Li. "Modeling and Solving Scheduling in Overloaded Situations with Weighted Partial MaxSAT". Mathematical Problems in Engineering 2021 (16 de julio de 2021): 1–17. http://dx.doi.org/10.1155/2021/9615463.

Texto completo

Resumen

In real-time systems, where tasks have timing requirements, once the workload exceeds the system’s capacity, missed due dates may cause system overload. In this situation, finding an optimal scheduling that minimizes the cumulative values of late tasks is critical in both theory and practice. Recently, formalizing scheduling problems as a class of generalized problems, such as Satisfiability Modulo Theory (SMT) and Maximum Satisfiability (MaxSAT), has been receiving immense concern. Enlightened by the high efficiency of these satisfiability-based methods, this paper formulates the single-machine scheduling problem of minimizing the total weight of late tasks as a Weighted Partial Maximum (WPM) Satisfiability problem. In the formulation, scheduling features are encoded as rigidly enforced hard clauses and the scheduling objective is treated as a set of weighted soft ones. Then an off-the-shelf WPM solver is exploited to maximize the total weight of the satisfied soft clauses, provided that all the hard clauses are satisfied. Experimental results demonstrate that, compared with the existing satisfiability-based methods, the proposed method significantly improves the efficiency of identifying the optimal schedule. Moreover, we make minor changes to apply the WPM formulation to parallel-machine scheduling, showing that the proposed method is sufficiently flexible and well scalable.

Los estilos APA, Harvard, Vancouver, ISO, etc.

7

MOUHOUB, MALEK y SAMIRA SADAOUI. "SOLVING INCREMENTAL SATISFIABILITY". International Journal on Artificial Intelligence Tools 16, n.º 01 (febrero de 2007): 139–47. http://dx.doi.org/10.1142/s0218213007003254.

Texto completo

Resumen

Propositional satisfiability (SAT) problem is fundamental to the theory of NP-completeness. Indeed, using the concept of "polynomial-time reducibility" all NP-complete problems can be polynomially reduced to SAT. Thus, any new technique for satisfiability problems will lead to general approaches for thousands of hard combinatorial problems. In this paper, we introduce the incremental propositional satisfiability problem that consists of maintaining the satisfiability of a propositional formula anytime a conjunction of new clauses is added. More precisely, the goal here is to check whether a solution to a SAT problem continues to be a solution anytime a new set of clauses is added and if not, whether the solution can be modified efficiently to satisfy the old formula and the new clauses. We will study the applicability of systematic and approximation methods for solving incremental SAT problems. The systematic method is based on the branch and bound technique while the approximation methods rely on stochastic local search and genetic algorithms. Experimental tests, conducted on randomly generated SAT instances, demonstrate the efficiency in time of the approximation methods over the branch and bound algorithm. However these approximation methods do not always guarantee the completeness of the solution returned. We show that a method we propose that uses non systematic search in a limited form together with branch and bound has the best compromise, in practice, between time and quality of the solution returned (success ratio).

Los estilos APA, Harvard, Vancouver, ISO, etc.

8

Ignatiev, Alexey, Mikoláš Janota y Joao Marques-Silva. "Quantified maximum satisfiability". Constraints 21, n.º 2 (24 de mayo de 2015): 277–302. http://dx.doi.org/10.1007/s10601-015-9195-9.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

9

Hooker, J. N. y V. Vinay. "Branching rules for satisfiability". Journal of Automated Reasoning 15, n.º 3 (1995): 359–83. http://dx.doi.org/10.1007/bf00881805.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

10

OMODEO, EUGENIO G., ALBERTO POLICRITI y ALEXANDRU I. TOMESCU. "Set-syllogistics meet combinatorics". Mathematical Structures in Computer Science 27, n.º 2 (11 de mayo de 2015): 296–310. http://dx.doi.org/10.1017/s0960129515000122.

Texto completo

Resumen

This paper considers ∃*∀* prenex sentences of pure first-order predicate calculus with equality. This is the set of formulas which Ramsey's treated in a famous article of 1930. We demonstrate that the satisfiability problem and the problem of existence of arbitrarily large models for these formulas can be reduced to the satisfiability problem for ∃*∀* prenex sentences of Set Theory (in the relators ∈, =).We present two satisfiability-preserving (in a broad sense) translations Φ ↦ $\dot{\Phi}$ and Φ ↦ Φσ of ∃*∀* sentences from pure logic to well-founded Set Theory, so that if $\dot{\Phi}$ is satisfiable (in the domain of Set Theory) then so is Φ, and if Φσ is satisfiable (again, in the domain of Set Theory) then Φ can be satisfied in arbitrarily large finite structures of pure logic.It turns out that |$\dot{\Phi}$| = $\mathcal{O}$(|Φ|) and |Φσ| = $\mathcal{O}$(|Φ|2).Our main result makes use of the fact that ∃*∀* sentences, even though constituting a decidable fragment of Set Theory, offer ways to describe infinite sets. Such a possibility is exploited to glue together infinitely many models of increasing cardinalities of a given ∃*∀* logical formula, within a single pair of infinite sets.

Los estilos APA, Harvard, Vancouver, ISO, etc.

11

Lynce, Inês y Joao Marques-Silva. "Restoring CSP Satisfiability with MaxSAT". Fundamenta Informaticae 107, n.º 2-3 (2011): 249–66. http://dx.doi.org/10.3233/fi-2011-402.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

12

Davenport, James H., Matthew England, Alberto Griggio, Thomas Sturm y Cesare Tinelli. "Symbolic computation and satisfiability checking". Journal of Symbolic Computation 100 (septiembre de 2020): 1–10. http://dx.doi.org/10.1016/j.jsc.2019.07.017.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

13

Liangze Yin, Fei He, William N. N. Hung, Xiaoyu Song y Ming Gu. "Maxterm Covering for Satisfiability". IEEE Transactions on Computers 61, n.º 3 (marzo de 2012): 420–26. http://dx.doi.org/10.1109/tc.2010.270.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

14

Laumann, C. R., R. Moessner, A. Scarddichio y S. L. Sondhi. "Random quantum satisfiability". Quantum Information and Computation 10, n.º 1&2 (enero de 2010): 1–16. http://dx.doi.org/10.26421/qic10.1-2-1.

Texto completo

Resumen

Alongside the effort underway to build quantum computers, it is important to better understand which classes of problems they will find easy and which others even they will find intractable. We study random ensembles of the QMA$_1$-complete quantum satisfiability (QSAT) problem introduced by Bravyi \cite{Bravyi:2006p4315}. QSAT appropriately generalizes the NP-complete classical satisfiability (SAT) problem. We show that, as the density of clauses/projectors is varied, the ensembles exhibit quantum phase transitions between phases that are satisfiable and unsatisfiable. Remarkably, almost all instances of QSAT for \emph{any} hypergraph exhibit the same dimension of the satisfying manifold. This establishes the QSAT decision problem as equivalent to a, potentially new, graph theoretic problem and that the hardest typical instances are likely to be localized in a bounded range of clause density.

Los estilos APA, Harvard, Vancouver, ISO, etc.

15

CODISH, MICHAEL, VITALY LAGOON y PETER J. STUCKEY. "Logic programming with satisfiability". Theory and Practice of Logic Programming 8, n.º 01 (25 de mayo de 2007): 121–28. http://dx.doi.org/10.1017/s1471068407003146.

Texto completo

Resumen

AbstractThis paper presents a Prolog interface to the MiniSat satisfiability solver. Logic programming with satisfiability combines the strengths of the two paradigms: logic programming for encoding search problems into satisfiability on the one hand and efficient SAT solving on the other. This synergy between these two exposes a programming paradigm that we propose here as a logic programming pearl. To illustrate logic programming with SAT solving, we give an example Prolog program that solves instances of Partial MAXSAT.

Los estilos APA, Harvard, Vancouver, ISO, etc.

16

Dixon, H. E., M. L. Ginsberg, D. Hofer, E. M. Luks y A. J. Parkes. "Generalizing Boolean Satisfiability III: Implementation". Journal of Artificial Intelligence Research 23 (1 de abril de 2005): 441–531. http://dx.doi.org/10.1613/jair.1656.

Texto completo

Resumen

This is the third of three papers describing ZAP, a satisfiability engine that substantially generalizes existing tools while retaining the performance characteristics of modern high-performance solvers. The fundamental idea underlying ZAP is that many problems passed to such engines contain rich internal structure that is obscured by the Boolean representation used; our goal has been to define a representation in which this structure is apparent and can be exploited to improve computational performance. The first paper surveyed existing work that (knowingly or not) exploited problem structure to improve the performance of satisfiability engines, and the second paper showed that this structure could be understood in terms of groups of permutations acting on individual clauses in any particular Boolean theory. We conclude the series by discussing the techniques needed to implement our ideas, and by reporting on their performance on a variety of problem instances.

Los estilos APA, Harvard, Vancouver, ISO, etc.

17

Pan, Guoqiang y Moshe Y. Vardi. "Symbolic Techniques in Satisfiability Solving". Journal of Automated Reasoning 35, n.º 1-3 (17 de diciembre de 2005): 25–50. http://dx.doi.org/10.1007/s10817-005-9009-7.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

18

Giunchiglia, Enrico y Toby Walsh. "Satisfiability in the Year 2005". Journal of Automated Reasoning 35, n.º 1-3 (31 de agosto de 2006): 1–2. http://dx.doi.org/10.1007/s10817-006-9041-2.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

19

Huang, Xiong y Wei Li. "Onk-positive satisfiability problem". Journal of Computer Science and Technology 14, n.º 4 (julio de 1999): 309–13. http://dx.doi.org/10.1007/bf02948732.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

20

Cimatti, Alessandro, Sergio Mover y Stefano Tonetta. "SMT-Based Verification of Hybrid Systems". Proceedings of the AAAI Conference on Artificial Intelligence 26, n.º 1 (20 de septiembre de 2021): 2100–2105. http://dx.doi.org/10.1609/aaai.v26i1.8442.

Texto completo

Resumen

Hybrid automata networks (HAN) are a powerful formalism to model complex embedded systems. In this paper, we survey the recent advances in the application of Satisfiability Modulo Theories (SMT) to the analysis of HAN. SMT can be seen as an extended form of Boolean satisfiability (SAT), where literals are interpreted with respect to a background theory (e.g. linear arithmetic). HAN can be symbolically represented by means of SMT formulae, and analyzed by generalizing to the case of SMT the traditional model checking algorithms based on SAT.

Los estilos APA, Harvard, Vancouver, ISO, etc.

21

LIERLER, YULIYA y MIROSLAW TRUSZCZYNSKI. "Transition systems for model generators—A unifying approach". Theory and Practice of Logic Programming 11, n.º 4-5 (julio de 2011): 629–46. http://dx.doi.org/10.1017/s1471068411000214.

Texto completo

Resumen

AbstractA fundamental task for propositional logic is to compute models of propositional formulas. Programs developed for this task are called satisfiability solvers. We show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for solvers developed for two other propositional formalisms: logic programming under the answer-set semantics, and the logic PC(ID). We show that in each case the task of computing models can be seen as “satisfiability modulo answer-set programming,” where the goal is to find a model of a theory that also is an answer set of a certain program. The unifying perspective we develop shows, in particular, that solvers clasp and minisat(id) are closely related despite being developed for different formalisms, one for answer-set programming and the latter for the logic PC(ID).

Los estilos APA, Harvard, Vancouver, ISO, etc.

22

Marques-Silva, Joao. "Model checking with Boolean Satisfiability". Journal of Algorithms 63, n.º 1-3 (enero de 2008): 3–16. http://dx.doi.org/10.1016/j.jalgor.2008.02.007.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

23

Bruni, Renato. "Solving peptide sequencing as satisfiability". Computers & Mathematics with Applications 55, n.º 5 (marzo de 2008): 912–23. http://dx.doi.org/10.1016/j.camwa.2006.12.094.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

24

Pratt, Vaughan y Jerzy Tiuryn. "Satisfiability of Inequalities in a Poset". Fundamenta Informaticae 28, n.º 1,2 (1996): 165–82. http://dx.doi.org/10.3233/fi-1996-281211.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

25

LETOMBE, FLORIAN y JOAO MARQUES-SILVA. "HYBRID INCREMENTAL ALGORITHMS FOR BOOLEAN SATISFIABILITY". International Journal on Artificial Intelligence Tools 21, n.º 06 (diciembre de 2012): 1250025. http://dx.doi.org/10.1142/s021821301250025x.

Texto completo

Resumen

Boolean Satisfiability (SAT) solvers have been successfully applied to a wide range of practical applications, including hardware model checking, software model finding, equivalence checking, and planning, among many others. SAT solvers are also the building block of more sophisticated decision procedures, including Satisfiability Modulo Theory (SMT) solvers. The large number of applications of SAT yields ever more challenging problem instances, and motivate the development of more efficient algorithms. Recent work studied hybrid approaches for SAT, which involves integrating incomplete and complete SAT solvers. This paper proposes a number of improvements to hybrid SAT solvers. Experimental results demonstrate that the proposed optimizations are effective. The resulting algorithms in general perform better and, more importantly, are significantly more robust.

Los estilos APA, Harvard, Vancouver, ISO, etc.

26

Cimatti, A., A. Griggio y R. Sebastiani. "Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories". Journal of Artificial Intelligence Research 40 (14 de abril de 2011): 701–28. http://dx.doi.org/10.1613/jair.3196.

Texto completo

Resumen

The problem of finding small unsatisfiable cores for SAT formulas has recently received a lot of interest, mostly for its applications in formal verification. However, propositional logic is often not expressive enough for representing many interesting verification problems, which can be more naturally addressed in the framework of Satisfiability Modulo Theories, SMT. Surprisingly, the problem of finding unsatisfiable cores in SMT has received very little attention in the literature. In this paper we present a novel approach to this problem, called the Lemma-Lifting approach. The main idea is to combine an SMT solver with an external propositional core extractor. The SMT solver produces the theory lemmas found during the search, dynamically lifting the suitable amount of theory information to the Boolean level. The core extractor is then called on the Boolean abstraction of the original SMT problem and of the theory lemmas. This results in an unsatisfiable core for the original SMT problem, once the remaining theory lemmas are removed. The approach is conceptually interesting, and has several advantages in practice. In fact, it is extremely simple to implement and to update, and it can be interfaced with every propositional core extractor in a plug-and-play manner, so as to benefit for free of all unsat-core reduction techniques which have been or will be made available. We have evaluated our algorithm with a very extensive empirical test on SMT-LIB benchmarks, which confirms the validity and potential of this approach.

Los estilos APA, Harvard, Vancouver, ISO, etc.

27

Liang, Chen, Xiaofeng Wang, Lei Lu y Pengfei Niu. "A New Method for 3-Satisfiability Problem Solving Space Structure on Structural Entropy". Symmetry 13, n.º 11 (22 de octubre de 2021): 2005. http://dx.doi.org/10.3390/sym13112005.

Texto completo

Resumen

Analyzing the solution space structure and evolution of 3-satisfiability (3-SAT) problem is an important way to study the difficulty of the solving satisfiability (SAT) problem. However, there is no unified analysis model for the spatial structure and evolution of solutions under different constraint densities. The analysis of different phase transition points and solution regions is based on different metric analysis models. The solution space of 3-SAT problem is obtained by planting strategy and belief propagation. According to the distribution of the influence of frozen variables on the solution, a label propagation algorithm based on planting strategy is proposed, is used to find the solution cluster, and then the structure entropy is used to measure its structure information. The structure entropy analysis model of 3-SAT problem solution space is established, and the unified analysis framework of solution space evolution and satisfiability phase transition is given. The experimental results show that the model is effective and can accurately analyze the evolution process of solution space and satisfiability phase transition, and verify the accuracy of interference phase transition point threshold predicted by long-range frustration theory.

Los estilos APA, Harvard, Vancouver, ISO, etc.

28

DUCK, GREGORY J. "SMCHR: Satisfiability modulo constraint handling rules". Theory and Practice of Logic Programming 12, n.º 4-5 (julio de 2012): 601–18. http://dx.doi.org/10.1017/s1471068412000208.

Texto completo

Resumen

AbstractConstraint Handling Rules (CHRs) are a high-level rule-based programming language for specification and implementation of constraint solvers. CHR manipulates a global store representing a flat conjunction of constraints. By default, CHR does not support goals with a more complex propositional structure including disjunction, negation, etc., or CHR relies on the host system to provide such features. In this paper we introduce Satisfiability Modulo Constraint Handling Rules (SMCHR): a tight integration of CHR with a modern Boolean Satisfiability (SAT) solver for quantifier-free formulae with an arbitrary propositional structure. SMCHR is essentially a Satisfiability Modulo Theories (SMT) solver where the theory T is implemented in CHR. The execution algorithm of SMCHR is based on lazy clause generation, where a new clause for the SAT solver is generated whenever a rule is applied. We shall also explore the practical aspects of building an SMCHR system, including extending a “built-in” constraint solver supporting equality with unification and justifications.

Los estilos APA, Harvard, Vancouver, ISO, etc.

29

Diedrich, Alexander, Alexander Maier y Oliver Niggemann. "Model-Based Diagnosis of Hybrid Systems Using Satisfiability Modulo Theory". Proceedings of the AAAI Conference on Artificial Intelligence 33 (17 de julio de 2019): 1452–59. http://dx.doi.org/10.1609/aaai.v33i01.33011452.

Texto completo

Resumen

Currently, detecting and isolating faults in hybrid systems is often done manually with the help of human operators. In this paper we present a novel model-based diagnosis approach for automatically diagnosing hybrid systems. The approach has two parts: First, modelling dynamic system behaviour is done through well-known state space models using differential equations. Second, from the state space models we calculate Boolean residuals through an observer-pattern. The novelty lies in implementing the observer pattern through the use of a symbolic system description specified in satisfiability theory modulo linear arithmetic. With this, we create a static situation for the diagnosis algorithm and decouple modelling and diagnosis. Evaluating the system description generates one Boolean residual for each component. These residuals constitute the fault symptoms. To find the minimum cardinality diagnosis from these symptoms we employ Reiter’s diagnosis lattice.For the experimental evaluation we use a simulation of the Tennessee Eastman process and a simulation of a four-tank model. We show that the presented approach is able to identify all injected faults.

Los estilos APA, Harvard, Vancouver, ISO, etc.

30

Bonacina, Maria Paola, Stéphane Graham-Lengrand y Natarajan Shankar. "Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness". Journal of Automated Reasoning 64, n.º 3 (4 de enero de 2019): 579–609. http://dx.doi.org/10.1007/s10817-018-09510-y.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

31

Cantone, Domenico, Andrea De Domenico, Pietro Maugeri y Eugenio G. Omodeo. "Complexity Assessments for Decidable Fragments of Set Theory. I: A Taxonomy for the Boolean Case*". Fundamenta Informaticae 181, n.º 1 (30 de junio de 2021): 37–69. http://dx.doi.org/10.3233/fi-2021-2050.

Texto completo

Resumen

We report on an investigation aimed at identifying small fragments of set theory (typically, sublanguages of Multi-Level Syllogistic) endowed with polynomial-time satisfiability decision tests, potentially useful for automated proof verification. Leaving out of consideration the membership relator ∈ for the time being, in this paper we provide a complete taxonomy of the polynomial and the NP-complete fragments involving, besides variables intended to range over the von Neumann set-universe, the Boolean operators ∪ ∩ \, the Boolean relators ⊆, ⊈,=, ≠, and the predicates ‘• = Ø’ and ‘Disj(•, •)’, meaning ‘the argument set is empty’ and ‘the arguments are disjoint sets’, along with their opposites ‘• ≠ Ø and ‘¬Disj(•, •)’. We also examine in detail how to test for satisfiability the formulae of six sample fragments: three sample problems are shown to be NP-complete, two to admit quadratic-time decision algorithms, and one to be solvable in linear time.

Los estilos APA, Harvard, Vancouver, ISO, etc.

32

Di Rosa, Emanuele, Enrico Giunchiglia y Marco Maratea. "Solving satisfiability problems with preferences". Constraints 15, n.º 4 (3 de julio de 2010): 485–515. http://dx.doi.org/10.1007/s10601-010-9095-y.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

33

Ishtaiwi, Abdelraouf y Qasem Abu Al-Haija. "Dynamic Initial Weight Assignment for MaxSAT". Algorithms 14, n.º 4 (31 de marzo de 2021): 115. http://dx.doi.org/10.3390/a14040115.

Texto completo

Resumen

The Maximum Satisfiability (Maximum Satisfiability (MaxSAT)) approach is the choice, and perhaps the only one, to deal with most real-world problems as most of them are unsatisfiable. Thus, the search for a complete and consistent solution to a real-world problem is impractical due to computational and time constraints. As a result, MaxSAT problems and solving techniques are of exceptional interest in the domain of Satisfiability (Satisfiability (SAT)). Our research experimentally investigated the performance gains of extending the most recently developed SAT dynamic Initial Weight assignment technique (InitWeight) to handle the MaxSAT problems. Specifically, we first investigated the performance gains of dynamically assigning the initial weights in the Divide and Distribute Fixed Weights solver (DDFW+Initial Weight for Maximum Satisfiability (DDFW+InitMaxSAT)) over Divide and Distribute Fixed Weights solver (DDFW) when applied to solve a wide range of well-known unweighted MaxSAT problems obtained from DIMACS. Secondly, we compared DDFW+InitMaxSAT’s performance against three known state-of-the-art SAT solving techniques: YalSAT, ProbSAT, and Sparrow. We showed that the assignment of dynamic initial weights increased the performance of DDFW+InitMaxSAT against DDFW by an order of magnitude on the majority of problems and performed similarly otherwise. Furthermore, we showed that the performance of DDFW+InitMaxSAT was superior to the other state-of-the-art algorithms. Eventually, we showed that the InitWeight technique could be extended to handling partial MaxSAT with minor modifications.

Los estilos APA, Harvard, Vancouver, ISO, etc.

34

Niemetz, Aina, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett y Cesare Tinelli. "Towards Satisfiability Modulo Parametric Bit-vectors". Journal of Automated Reasoning 65, n.º 7 (18 de junio de 2021): 1001–25. http://dx.doi.org/10.1007/s10817-021-09598-9.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

35

Pipatsrisawat, Knot y Adnan Darwiche. "On Modern Clause-Learning Satisfiability Solvers". Journal of Automated Reasoning 44, n.º 3 (6 de noviembre de 2009): 277–301. http://dx.doi.org/10.1007/s10817-009-9156-3.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

36

PITTEL, BORIS y GREGORY B. SORKIN. "The Satisfiability Threshold fork-XORSAT". Combinatorics, Probability and Computing 25, n.º 2 (31 de julio de 2015): 236–68. http://dx.doi.org/10.1017/s0963548315000097.

Texto completo

Resumen

We consider ‘unconstrained’ randomk-XORSAT, which is a uniformly random system ofmlinear non-homogeneous equations in$\mathbb{F}$2overnvariables, each equation containingk⩾ 3 variables, and also consider a ‘constrained’ model where every variable appears in at least two equations. Dubois and Mandler proved thatm/n= 1 is a sharp threshold for satisfiability of constrained 3-XORSAT, and analysed the 2-core of a random 3-uniform hypergraph to extend this result to find the threshold for unconstrained 3-XORSAT.We show thatm/n= 1 remains a sharp threshold for satisfiability of constrainedk-XORSAT for everyk⩾ 3, and we use standard results on the 2-core of a randomk-uniform hypergraph to extend this result to find the threshold for unconstrainedk-XORSAT. For constrainedk-XORSAT we narrow the phase transition window, showing thatm − n→ −∞ implies almost-sure satisfiability, whilem − n→ +∞ implies almost-sure unsatisfiability.

Los estilos APA, Harvard, Vancouver, ISO, etc.

37

Fortnow, Lance. "Time–Space Tradeoffs for Satisfiability". Journal of Computer and System Sciences 60, n.º 2 (abril de 2000): 337–53. http://dx.doi.org/10.1006/jcss.1999.1671.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

38

Carapelle, Claudia, Alexander Kartzow y Markus Lohrey. "Satisfiability of ECTL⁎ with constraints". Journal of Computer and System Sciences 82, n.º 5 (agosto de 2016): 826–55. http://dx.doi.org/10.1016/j.jcss.2016.02.002.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

39

Yannakakis, M. "On the Approximation of Maximum Satisfiability". Journal of Algorithms 17, n.º 3 (noviembre de 1994): 475–502. http://dx.doi.org/10.1006/jagm.1994.1045.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

40

Niedermeier, Rolf y Peter Rossmanith. "New Upper Bounds for Maximum Satisfiability". Journal of Algorithms 36, n.º 1 (julio de 2000): 63–88. http://dx.doi.org/10.1006/jagm.2000.1075.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

41

BRAHA, DAN. "Design-as-satisfiability: A new approach to automated synthesis". Artificial Intelligence for Engineering Design, Analysis and Manufacturing 15, n.º 5 (noviembre de 2001): 385–99. http://dx.doi.org/10.1017/s0890060401155022.

Texto completo

Resumen

This article addresses computational synthesis systems that attempt to find a structural description that matches a set of initial functional requirements and design constraints with a finite sequence of production rules. It has been previously shown by the author that it is computationally difficult to identify a sequence of production rules that can lead to a satisficing design solution. As a result, computational synthesis, particularly with large volumes of selection information, requires effective design search procedures. Many computational synthesis systems utilize transformational search strategies. However, such search strategies are inefficient due to the combinatorial nature of the problem. In this article, the problem is approached using a completely different paradigm. The new approach encodes a design search problem as a Boolean (propositional) satisfiability problem, such that from every satisfying Boolean-valued truth assignment to the corresponding Boolean expression we efficiently can derive a solution to the original synthesis problem (along with its finite sequence of production rules). A major advantage of the proposed approach is the possibility of utilizing recently developed powerful randomized search algorithms for solving Boolean satisfiability problems, which considerably outperform the most widely used satisfiability algorithms. The new design-as-satisfiability technique provides a flexible framework for stating a variety of design constraints, and also represents properly the theory behind modern constraint-based design systems.

Los estilos APA, Harvard, Vancouver, ISO, etc.

42

FERNÁNDEZ, MARIBEL. "AC Complement Problems: Satisfiability and Negation Elimination". Journal of Symbolic Computation 22, n.º 1 (julio de 1996): 49–82. http://dx.doi.org/10.1006/jsco.1996.0041.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

43

LIERLER, YULIYA y BENJAMIN SUSMAN. "On relation between constraint answer set programming and satisfiability modulo theories". Theory and Practice of Logic Programming 17, n.º 4 (28 de junio de 2017): 559–90. http://dx.doi.org/10.1017/s1471068417000114.

Texto completo

Resumen

AbstractConstraint answer set programming is a promising research direction that integrates answer set programming with constraint processing. It is often informally related to the field of satisfiability modulo theories. Yet, the exact formal link is obscured as the terminology and concepts used in these two research areas differ. In this paper, we connect these two research areas by uncovering the precise formal relation between them. We believe that this work will boost the cross-fertilization of the theoretical foundations and the existing solving methods in both areas. As a step in this direction, we provide a translation from constraint answer set programs with integer linear constraints to satisfiability modulo linear integer arithmetic that paves the way to utilizing modern satisfiability modulo theories solvers for computing answer sets of constraint answer set programs.

Los estilos APA, Harvard, Vancouver, ISO, etc.

44

DE ANGELIS, EMANUELE, FABIO FIORAVANTI, ALBERTO PETTOROSSI y MAURIZIO PROIETTI. "Solving Horn Clauses on Inductive Data Types Without Induction". Theory and Practice of Logic Programming 18, n.º 3-4 (julio de 2018): 452–69. http://dx.doi.org/10.1017/s1471068418000157.

Texto completo

Resumen

AbstractWe address the problem of verifying the satisfiability of Constrained Horn Clauses (CHCs) based on theories of inductively defined data structures, such as lists and trees. We propose a transformation technique whose objective is the removal of these data structures from CHCs, hence reducing their satisfiability to a satisfiability problem for CHCs on integers and booleans. We propose a transformation algorithm and identify a class of clauses where it always succeeds. We also consider an extension of that algorithm, which combines clause transformation with reasoning on integer constraints. Via an experimental evaluation we show that our technique greatly improves the effectiveness of applying the Z3 solver to CHCs. We also show that our verification technique based on CHC transformation followed by CHC solving, is competitive with respect to CHC solvers extended with induction.

Los estilos APA, Harvard, Vancouver, ISO, etc.

45

Hamadi, Youssef, Saïd Jabbour y Lakhdar Saïs. "Learning from conflicts in propositional satisfiability". 4OR 10, n.º 1 (28 de diciembre de 2011): 15–32. http://dx.doi.org/10.1007/s10288-011-0191-7.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

46

Cantone, Domenico, Alfio Giarlotta y Stephen Watson. "The Satisfiability Problem for Boolean Set Theory with a Choice Correspondence". Electronic Proceedings in Theoretical Computer Science 256 (6 de septiembre de 2017): 61–75. http://dx.doi.org/10.4204/eptcs.256.5.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

47

Zhou, Haijun. "Solution space heterogeneity of the randomK-satisfiability problem: Theory and simulations". Journal of Physics: Conference Series 233 (1 de junio de 2010): 012011. http://dx.doi.org/10.1088/1742-6596/233/1/012011.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

48

Aloul, F. A., K. A. Sakallah y I. L. Markov. "Efficient symmetry breaking for Boolean satisfiability". IEEE Transactions on Computers 55, n.º 5 (mayo de 2006): 549–58. http://dx.doi.org/10.1109/tc.2006.75.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

49

Ghilardi, Silvio. "Model-Theoretic Methods in Combined Constraint Satisfiability". Journal of Automated Reasoning 33, n.º 3-4 (octubre de 2004): 221–49. http://dx.doi.org/10.1007/s10817-004-6241-5.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

50

Bhalla, Ateet, Inês Lynce, José T. de Sousa y João Marques-Silva. "Heuristic-Based Backtracking Relaxation for Propositional Satisfiability". Journal of Automated Reasoning 35, n.º 1-3 (octubre de 2005): 3–24. http://dx.doi.org/10.1007/s10817-005-9005-y.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

Ofrecemos descuentos en todos los planes premium para autores cuyas obras están incluidas en selecciones literarias temáticas. ¡Contáctenos para obtener un código promocional único!