Bibliographies thématiques / Satisfiability theory / Articles de revues

Articles de revues sur le sujet « Satisfiability theory »

Pour voir les autres types de publications sur ce sujet consultez le lien suivant : Satisfiability theory.
Auteur : Grafiati
Publié le 11 mars 2023

Créez une référence correcte selon les styles APA, MLA, Chicago, Harvard et plusieurs autres

Choisissez une source :

Consultez les 50 meilleurs articles de revues pour votre recherche sur le sujet « Satisfiability theory ».

À côté de chaque source dans la liste de références il y a un bouton « Ajouter à la bibliographie ». Cliquez sur ce bouton, et nous générerons automatiquement la référence bibliographique pour la source choisie selon votre style de citation préféré : APA, MLA, Harvard, Vancouver, Chicago, etc.

Vous pouvez aussi télécharger le texte intégral de la publication scolaire au format pdf et consulter son résumé en ligne lorsque ces informations sont inclues dans les métadonnées.

Parcourez les articles de revues sur diverses disciplines et organisez correctement votre bibliographie.

1

Dixon, H. E., M. L. Ginsberg, E. M. Luks et A. J. Parkes. « Generalizing Boolean Satisfiability II : Theory ». Journal of Artificial Intelligence Research 22 (1 décembre 2004) : 481–534. http://dx.doi.org/10.1613/jair.1555.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
2

Michaliszyn, Jakub, Jan Otop et Piotr Witkowski. « Satisfiability versus Finite Satisfiability in Elementary Modal Logics ». Fundamenta Informaticae 163, no 2 (3 novembre 2018) : 165–88. http://dx.doi.org/10.3233/fi-2018-1736.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
3

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

Texte intégral
Styles 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, no 2 (juin 2022) : 264–65. http://dx.doi.org/10.1017/bsl.2022.2.

Texte intégral
Résumé :
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
Styles APA, Harvard, Vancouver, ISO, etc.
5

Alon, Noga, et Asaf Shapira. « Testing satisfiability ». Journal of Algorithms 47, no 2 (juillet 2003) : 87–103. http://dx.doi.org/10.1016/s0196-6774(03)00019-1.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
6

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

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
7

MOUHOUB, MALEK, et SAMIRA SADAOUI. « SOLVING INCREMENTAL SATISFIABILITY ». International Journal on Artificial Intelligence Tools 16, no 01 (février 2007) : 139–47. http://dx.doi.org/10.1142/s0218213007003254.

Texte intégral
Résumé :
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).
Styles APA, Harvard, Vancouver, ISO, etc.
8

Ignatiev, Alexey, Mikoláš Janota et Joao Marques-Silva. « Quantified maximum satisfiability ». Constraints 21, no 2 (24 mai 2015) : 277–302. http://dx.doi.org/10.1007/s10601-015-9195-9.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
9

Hooker, J. N., et V. Vinay. « Branching rules for satisfiability ». Journal of Automated Reasoning 15, no 3 (1995) : 359–83. http://dx.doi.org/10.1007/bf00881805.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
10

OMODEO, EUGENIO G., ALBERTO POLICRITI et ALEXANDRU I. TOMESCU. « Set-syllogistics meet combinatorics ». Mathematical Structures in Computer Science 27, no 2 (11 mai 2015) : 296–310. http://dx.doi.org/10.1017/s0960129515000122.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
11

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

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
12

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

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
13

Liangze Yin, Fei He, William N. N. Hung, Xiaoyu Song et Ming Gu. « Maxterm Covering for Satisfiability ». IEEE Transactions on Computers 61, no 3 (mars 2012) : 420–26. http://dx.doi.org/10.1109/tc.2010.270.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
14

Laumann, C. R., R. Moessner, A. Scarddichio et S. L. Sondhi. « Random quantum satisfiability ». Quantum Information and Computation 10, no 1&2 (janvier 2010) : 1–16. http://dx.doi.org/10.26421/qic10.1-2-1.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
15

CODISH, MICHAEL, VITALY LAGOON et PETER J. STUCKEY. « Logic programming with satisfiability ». Theory and Practice of Logic Programming 8, no 01 (25 mai 2007) : 121–28. http://dx.doi.org/10.1017/s1471068407003146.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
16

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

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
17

Pan, Guoqiang, et Moshe Y. Vardi. « Symbolic Techniques in Satisfiability Solving ». Journal of Automated Reasoning 35, no 1-3 (17 décembre 2005) : 25–50. http://dx.doi.org/10.1007/s10817-005-9009-7.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
18

Giunchiglia, Enrico, et Toby Walsh. « Satisfiability in the Year 2005 ». Journal of Automated Reasoning 35, no 1-3 (31 août 2006) : 1–2. http://dx.doi.org/10.1007/s10817-006-9041-2.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
19

Huang, Xiong, et Wei Li. « Onk-positive satisfiability problem ». Journal of Computer Science and Technology 14, no 4 (juillet 1999) : 309–13. http://dx.doi.org/10.1007/bf02948732.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
20

Cimatti, Alessandro, Sergio Mover et Stefano Tonetta. « SMT-Based Verification of Hybrid Systems ». Proceedings of the AAAI Conference on Artificial Intelligence 26, no 1 (20 septembre 2021) : 2100–2105. http://dx.doi.org/10.1609/aaai.v26i1.8442.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
21

LIERLER, YULIYA, et MIROSLAW TRUSZCZYNSKI. « Transition systems for model generators—A unifying approach ». Theory and Practice of Logic Programming 11, no 4-5 (juillet 2011) : 629–46. http://dx.doi.org/10.1017/s1471068411000214.

Texte intégral
Résumé :
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).
Styles APA, Harvard, Vancouver, ISO, etc.
22

Marques-Silva, Joao. « Model checking with Boolean Satisfiability ». Journal of Algorithms 63, no 1-3 (janvier 2008) : 3–16. http://dx.doi.org/10.1016/j.jalgor.2008.02.007.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
23

Bruni, Renato. « Solving peptide sequencing as satisfiability ». Computers & ; Mathematics with Applications 55, no 5 (mars 2008) : 912–23. http://dx.doi.org/10.1016/j.camwa.2006.12.094.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
24

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

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
25

LETOMBE, FLORIAN, et JOAO MARQUES-SILVA. « HYBRID INCREMENTAL ALGORITHMS FOR BOOLEAN SATISFIABILITY ». International Journal on Artificial Intelligence Tools 21, no 06 (décembre 2012) : 1250025. http://dx.doi.org/10.1142/s021821301250025x.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
26

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

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
27

Liang, Chen, Xiaofeng Wang, Lei Lu et Pengfei Niu. « A New Method for 3-Satisfiability Problem Solving Space Structure on Structural Entropy ». Symmetry 13, no 11 (22 octobre 2021) : 2005. http://dx.doi.org/10.3390/sym13112005.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
28

DUCK, GREGORY J. « SMCHR : Satisfiability modulo constraint handling rules ». Theory and Practice of Logic Programming 12, no 4-5 (juillet 2012) : 601–18. http://dx.doi.org/10.1017/s1471068412000208.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
29

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

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
30

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

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
31

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

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
32

Di Rosa, Emanuele, Enrico Giunchiglia et Marco Maratea. « Solving satisfiability problems with preferences ». Constraints 15, no 4 (3 juillet 2010) : 485–515. http://dx.doi.org/10.1007/s10601-010-9095-y.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
33

Ishtaiwi, Abdelraouf, et Qasem Abu Al-Haija. « Dynamic Initial Weight Assignment for MaxSAT ». Algorithms 14, no 4 (31 mars 2021) : 115. http://dx.doi.org/10.3390/a14040115.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
34

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

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
35

Pipatsrisawat, Knot, et Adnan Darwiche. « On Modern Clause-Learning Satisfiability Solvers ». Journal of Automated Reasoning 44, no 3 (6 novembre 2009) : 277–301. http://dx.doi.org/10.1007/s10817-009-9156-3.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
36

PITTEL, BORIS, et GREGORY B. SORKIN. « The Satisfiability Threshold fork-XORSAT ». Combinatorics, Probability and Computing 25, no 2 (31 juillet 2015) : 236–68. http://dx.doi.org/10.1017/s0963548315000097.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
37

Fortnow, Lance. « Time–Space Tradeoffs for Satisfiability ». Journal of Computer and System Sciences 60, no 2 (avril 2000) : 337–53. http://dx.doi.org/10.1006/jcss.1999.1671.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
38

Carapelle, Claudia, Alexander Kartzow et Markus Lohrey. « Satisfiability of ECTL⁎ with constraints ». Journal of Computer and System Sciences 82, no 5 (août 2016) : 826–55. http://dx.doi.org/10.1016/j.jcss.2016.02.002.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
39

Yannakakis, M. « On the Approximation of Maximum Satisfiability ». Journal of Algorithms 17, no 3 (novembre 1994) : 475–502. http://dx.doi.org/10.1006/jagm.1994.1045.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
40

Niedermeier, Rolf, et Peter Rossmanith. « New Upper Bounds for Maximum Satisfiability ». Journal of Algorithms 36, no 1 (juillet 2000) : 63–88. http://dx.doi.org/10.1006/jagm.2000.1075.

Texte intégral
Styles 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, no 5 (novembre 2001) : 385–99. http://dx.doi.org/10.1017/s0890060401155022.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
42

FERNÁNDEZ, MARIBEL. « AC Complement Problems : Satisfiability and Negation Elimination ». Journal of Symbolic Computation 22, no 1 (juillet 1996) : 49–82. http://dx.doi.org/10.1006/jsco.1996.0041.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
43

LIERLER, YULIYA, et BENJAMIN SUSMAN. « On relation between constraint answer set programming and satisfiability modulo theories ». Theory and Practice of Logic Programming 17, no 4 (28 juin 2017) : 559–90. http://dx.doi.org/10.1017/s1471068417000114.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
44

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

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
45

Hamadi, Youssef, Saïd Jabbour et Lakhdar Saïs. « Learning from conflicts in propositional satisfiability ». 4OR 10, no 1 (28 décembre 2011) : 15–32. http://dx.doi.org/10.1007/s10288-011-0191-7.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
46

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

Texte intégral
Styles 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 juin 2010) : 012011. http://dx.doi.org/10.1088/1742-6596/233/1/012011.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
48

Aloul, F. A., K. A. Sakallah et I. L. Markov. « Efficient symmetry breaking for Boolean satisfiability ». IEEE Transactions on Computers 55, no 5 (mai 2006) : 549–58. http://dx.doi.org/10.1109/tc.2006.75.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
49

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

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
50

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

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
Vous pouvez également être intéressé par les bibliographies sur le sujet « Satisfiability theory » pour d’autres types de sources :
Thèses Livres
Nous offrons des réductions sur tous les plans premium pour les auteurs dont les œuvres sont incluses dans des sélections littéraires thématiques. Contactez-nous pour obtenir un code promo unique!

Vers la bibliographie