Log in

Relevant bibliographies by topics / Satisfiability theory / Journal articles

Journal articles on the topic 'Satisfiability theory'

To see the other types of publications on this topic, follow the link: Satisfiability theory.

Author: Grafiati

Published: 11 March 2023

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles

Select a source type:

Consult the top 50 journal articles for your research on the topic 'Satisfiability theory.'

Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.

You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.

Browse journal articles on a wide variety of disciplines and organise your bibliography correctly.

1

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

2

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

3

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

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 (June 2022): 264–65. http://dx.doi.org/10.1017/bsl.2022.2.

Full text

Abstract:

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

APA, Harvard, Vancouver, ISO, and other styles

5

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

6

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

7

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

Full text

Abstract:

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).

APA, Harvard, Vancouver, ISO, and other styles

8

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

9

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

10

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

11

Lynce, Inês, and 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.

Full text

APA, Harvard, Vancouver, ISO, and other styles

12

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

13

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

14

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

15

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

16

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

17

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

18

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

19

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

20

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

21

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

Full text

Abstract:

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).

APA, Harvard, Vancouver, ISO, and other styles

22

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

23

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

24

Pratt, Vaughan, and 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.

Full text

APA, Harvard, Vancouver, ISO, and other styles

25

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

26

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

27

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

28

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

29

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

30

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

31

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

32

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

33

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

34

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

35

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

36

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

37

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

38

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

39

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

40

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

41

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

42

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

43

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

44

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

45

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

46

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

47

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

48

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

49

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

50

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

We offer discounts on all premium plans for authors whose works are included in thematic literature selections. Contact us to get a unique promo code!