For some restricted classes of logical formulae, the satisfiability problem can be solved efficiently in polynomial time or even linear. One such class is that of Horn formulae, which consist only of Horn clauses with at most one positive literal. I've heard that it is possible to solve Horn SAT in linear time using graphs, but couldn't find any implementation of such solution. Now I'm really interested whether it is possible and if it is, how would algorithm look like?
1
There are 1 answers
Related Questions in ALGORITHM
- MCNP 6 - Doubts about cells
- Given partially sorted array of type x<y => first apperance of x comes before first of y, sort in average O(n)
- What is the algorithm behind math.gcd and why it is faster Euclidean algorithm?
- Purpose of last 2 while loops in the merge algorithm of merge sort sorting technique
- Dots and Boxes with apha-beta pruning
- What is the average and worst-case time complexity of my string searching algorithm?
- Building a School Schedule Generator
- TC problem 5-2:how to calculate the probability of the indicator random variable?
- LCA of a binary tree implemented in Python
- Identify the checksum algorithm
- Algorithm for finding a subset of nodes in a weighted connected graph such that the distance between any pair nodes are under a postive number?
- Creating an efficent and time-saving algorithm to find difference between greater than and lesser than combination
- Algorithm to find neighbours of point by distance with no repeats
- Asking code suggestions about data structure and algorithm
- Heap sort with multithreading
Related Questions in GRAPH
- Querying Office for National Statistics data using SPARQL
- Which mathematical algorithm is used for interpolation between datapoints in Smooth Line Chart of Echart?
- how can I use coordinates of path walked by multiple subjects
- Creating a Graph/Chart needing TWO secondary axis options for a combination of Clustered and Stacked Graph Columns
- How to stretch specific y axis intervals so the space between some values is larger than between others?
- out of order time points on multi line chart
- What does negative flow on a reverse arc of a graph in Boykov-Kolmogorov max flow algorithm mean?
- how to generate {8,3} regular graphs for large number of vertices
- Why can't I apply ModularityState from graph-tool on a graph in XML format?
- Update Node from OneTBB Library
- Find the smallest set of vertices in a graph such that you can still reach any point in the set when any single vertex is removed
- Graph Neural Network Custom Data
- FIFO-property in graphs
- How to display total count of bars for each group in Google Charts on the right side of the graph or in legend position
- Whats wrong on Graph API permission for selected site
Related Questions in SAT
- minimizing a CNF in python
- How to use the Z3 Solver to solve a natural deduction problem
- Are there tools available to convert SMT-LIB files to DIMACS CNF?
- MUS cores in Alloy UNSAT models
- Is there an algorithm to find the union and intersection of 2 given possible binary numbers
- How to Abstract "At Most One" Constraint Across Multiple Time Steps in a SAT Solver?
- Computational Learning Problem: 3-DNF Reduction
- Alloy6 allowing invalid state transitions
- Lion and Unicorn with Prolog SAT Solver
- "Check if a cycle of K nodes exists" reduction to SAT?
- pysmt: how to extract models uniformly at random?
- Specialized SAT solver (?)
- Reversing the CNF conversion after MAXSAT solve
- No output from Z3/SMT solver for weight balancing problem with nested quantifiers
- 3 partition np completeness
Related Questions in HORN
- Z3 returns unknown with HORN logic if I use a specific operation
- Using `Array` in the HORN logic in Spacer/Z3
- Horn SAT algorithm using graphs
- what's the meaning of "at-most" keyword in SMT-LIB language (extended version of Z3 FixedPoint)
- What are the equivalent horn clauses to these clauses?
- Issues using a simple jQuery script to grab one div height & make another div the same size
- SVG with transparency
- CNF vs Horn Satisfiability
- Is "~A=>B" a horn clause?
- Signing an unsigned assembly
- What is a real-world application for HORN?
Popular Questions
- How do I undo the most recent local commits in Git?
- How can I remove a specific item from an array in JavaScript?
- How do I delete a Git branch locally and remotely?
- Find all files containing a specific text (string) on Linux?
- How do I revert a Git repository to a previous commit?
- How do I create an HTML button that acts like a link?
- How do I check out a remote Git branch?
- How do I force "git pull" to overwrite local files?
- How do I list all files of a directory?
- How to check whether a string contains a substring in JavaScript?
- How do I redirect to another webpage?
- How can I iterate over rows in a Pandas DataFrame?
- How do I convert a String to an int in Java?
- Does Python have a string 'contains' substring method?
- How do I check if a string contains a specific word?
Popular Tags
Trending Questions
- UIImageView Frame Doesn't Reflect Constraints
- Is it possible to use adb commands to click on a view by finding its ID?
- How to create a new web character symbol recognizable by html/javascript?
- Why isn't my CSS3 animation smooth in Google Chrome (but very smooth on other browsers)?
- Heap Gives Page Fault
- Connect ffmpeg to Visual Studio 2008
- Both Object- and ValueAnimator jumps when Duration is set above API LvL 24
- How to avoid default initialization of objects in std::vector?
- second argument of the command line arguments in a format other than char** argv or char* argv[]
- How to improve efficiency of algorithm which generates next lexicographic permutation?
- Navigating to the another actvity app getting crash in android
- How to read the particular message format in android and store in sqlite database?
- Resetting inventory status after order is cancelled
- Efficiently compute powers of X in SSE/AVX
- Insert into an external database using ajax and php : POST 500 (Internal Server Error)
If you're familiar with Davis–Putnam–Logemann–Loveland, Horn clauses are a class of formulae that can be solved using one round of unit propagation, with no backtracking.
In graph terms, we do the obvious thing and set up a bipartite graph with variables on one side, clauses on the other, and edges to represent a variable appearing as a negative literal in a clause. We also have a work queue of clauses consisting of a single positive literal. While the work queue is not empty, pop any element, identify the node corresponding to the variable, and delete it and its neighbors. For each clause vertex that now has degree zero, one of two things happens. If that clause has a positive literal, then we add it to the work queue. Otherwise, we've proved that the formula is unsatisfiable. If we reach the end of the work queue without finding such a clause, then the formula is satisfiable, and one satisfying assignment is to set all variables that entered the work queue to true, and all others to false.