Search results for "satisfiability problem"

showing 7 items of 17 documents

Quantum Query Algorithms for Conjunctions

2010

Every Boolean function can be presented as a logical formula in conjunctive normal form. Fast algorithm for conjunction plays significant role in overall algorithm for computing arbitrary Boolean function. First, we present a quantum query algorithm for conjunction of two bits. Our algorithm uses one quantum query and correct result is obtained with a probability p = 4/5, that improves the previous result. Then, we present the main result - generalization of our approach to design efficient quantum algorithms for computing conjunction of two Boolean functions. Finally, we demonstrate another kind of an algorithm for conjunction of two bits, that has a correct answer probability p = 9/10. Th…

Product termTheoretical computer scienceParity functionAnd-inverter graphMaximum satisfiability problemQuantum phase estimation algorithmBoolean expressionQuantum algorithmBoolean functionAlgorithmMathematics
researchProduct

Unions of identifiable families of languages

1996

This paper deals with the satisfiability of requirements put on the identifiability of unions of language families. We consider identification in the limit from a text with bounds on mindchanges and anomalies. We show that, though these identification types are not closed under the set union, some of them still have features that resemble closedness. To formalize this, we generalize the notion of closedness. Then by establishing “how closed” these identification types are we solve the satisfiability problem.

Set (abstract data type)Discrete mathematicsIdentification (information)Limit (category theory)IdentifiabilityLanguage familyInductive reasoningBoolean satisfiability problemMathematical economicsSatisfiabilityMathematics
researchProduct

Sparse Sampling and Maximum Likelihood Estimation for Boolean Models

1991

A condition for practical independence of contact distribution functions in Boolean models is obtained. This result allows the authors to use maximum likelihcod methods, via sparse sampling, for estimating unknown parameters of an isotropic Boolean model. The second part of this paper is devoted to a simulation study of the proposed method. AMS classification: 60D05

Statistics and ProbabilityBiometricsBoolean modelIsotropySampling (statistics)General MedicineLikelihood-ratio testStatisticsMaximum satisfiability problemStatistics Probability and UncertaintyAlgorithmIndependence (probability theory)Standard Boolean modelMathematicsBiometrical Journal
researchProduct

Combining finite learning automata with GSAT for the satisfiability problem

2010

A large number of problems that occur in knowledge-representation, learning, very large scale integration technology (VLSI-design), and other areas of artificial intelligence, are essentially satisfiability problems. The satisfiability problem refers to the task of finding a satisfying assignment that makes a Boolean expression evaluate to True. The growing need for more efficient and scalable algorithms has led to the development of a large number of SAT solvers. This paper reports the first approach that combines finite learning automata with the greedy satisfiability algorithm (GSAT). In brief, we introduce a new algorithm that integrates finite learning automata and traditional GSAT use…

Theoretical computer scienceLearning automataComputer scienceRandom walkSatisfiabilitySet (abstract data type)Artificial IntelligenceControl and Systems EngineeringMaximum satisfiability problemBenchmark (computing)Combinatorial optimizationBoolean expressionElectrical and Electronic EngineeringBoolean satisfiability problemAlgorithmEngineering Applications of Artificial Intelligence
researchProduct

Solving Graph Coloring Problems Using Learning Automata

2008

The graph coloring problem (GCP) is a widely studied combinatorial optimization problem with numerous applications, including time tabling, frequency assignment, and register allocation. The growing need for more efficient algorithms has led to the development of several GCP solvers. In this paper, we introduce the first GCP solver that is based on Learning Automata (LA). We enhance traditional Random Walk with LA-based learning capability, encoding the GCP as a Boolean satisfiability problem (SAT). Extensive experiments demonstrate that the LA significantly improve the performance of RW, thus laying the foundation for novel LA-based solutions to the GCP.

Theoretical computer scienceLearning automataEncoding (memory)Frequency assignmentCombinatorial optimizationGraph coloringSolverBoolean satisfiability problemMathematicsRegister allocation
researchProduct

On the satisfiability problem for fragments of two-variable logic with one transitive relation

2019

Abstract We study the satisfiability problem for two-variable first-order logic over structures with one transitive relation. We show that the problem is decidable in 2-NExpTime for the fragment consisting of formulas where existential quantifiers are guarded by transitive atoms. As this fragment enjoys neither the finite model property nor the tree model property, to show decidability we introduce a novel model construction technique based on the infinite Ramsey theorem. We also point out why the technique is not sufficient to obtain decidability for the full two-variable logic with one transitive relation; hence, contrary to our previous claim, [FO$^2$ with one transitive relation is deci…

Transitive relationLogic010102 general mathematics0102 computer and information sciences01 natural sciencesTheoretical Computer ScienceCombinatoricsVariable (computer science)Arts and Humanities (miscellaneous)010201 computation theory & mathematicsHardware and Architecture0101 mathematicsBoolean satisfiability problemSoftwareMathematicsJournal of Logic and Computation
researchProduct

Some Computational Aspects of DISTANCE-SAT

2007

In many AI fields, one must face the problem of finding a solution that is as close as possible to a given configuration. This paper addresses this problem in a propositional framework. We introduce the decision problem distance-sat, which consists in determining whether a propositional formula admits a model that disagrees with a given partial interpretation on at most d variables. The complexity of distance-sat and of several restrictions of it are identified. Two algorithms based on the well-known Davis/Logemann/Loveland search procedure for the satisfiability problem sat are presented so as to solve distance-sat for CNF formulas. Their computational behaviors are compared with the ones …

[INFO.INFO-AI] Computer Science [cs]/Artificial Intelligence [cs.AI]Theoretical computer scienceComputational complexity theory0102 computer and information sciences02 engineering and technologyComputer Science::Computational Complexity01 natural sciences[INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI]#SATArtificial IntelligenceComputer Science::Logic in Computer ScienceDPLL algorithm0202 electrical engineering electronic engineering information engineeringComputingMilieux_MISCELLANEOUSMathematicsDecision problemFunction problemSatisfiabilityPropositional formulaTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESComputational Theory and Mathematics010201 computation theory & mathematics020201 artificial intelligence & image processingBoolean satisfiability problemAlgorithmSoftware
researchProduct