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 best solutions below
Related Questions in ALGORITHM
- Two different numbers in an array which their sum equals to a given value
- Given two arrays of positive numbers, re-arrange them to form a resulting array, resulting array contains the elements in the same given sequence
- Time complexity of the algorithm?
- Find a MST in O(V+E) Time in a Graph
- Why k and l for LSH used for approximate nearest neighbours?
- How to count the number of ways of choosing of k equal substrings from a List L(the list of All Substrings)
- Issues with reversing the linkedlist
- Finding first non-repeating number in integer array
- Finding average of an array
- How to check for duplicates with less time in a list over 9000 elements by python
- How to pick a number based on probability?
- Insertion Sort help in javascript -- Khan Academy
- Developing a Checkers (Draughts) engine, how to begin?
- Can Bellman-Ford algorithm be used to find shorthest path on a graph with only positive edges?
- What is the function for the KMP Failure Algorithm?
Related Questions in GRAPH
- Find a MST in O(V+E) Time in a Graph
- Using chart and tooltip
- What clustering algorithms can I consider for graph?
- Clustering on Graph (using Boost Graph Library)
- How to set a domain on an axis and have the axis intervals not constant or take up different amount of interval spaces using d3
- sort graph by distance to end nodes
- Construct and label a uniform graph in NetworkX using dictionaries?
- Plot: Add legend that overlay several Frames
- Labelling nodes in networkx
- Plotting a data frame in R
- How does boost::subgraph work? Can we use filtered graph?
- How do I make a decaying oscilating function in python?
- Deserialize tree given inorder format?
- Having issues with D3 scale and data binding
- ArangoDB graph operations via REST API
Related Questions in SAT
- SAT-Solving: DPLL vs.?
- Adding clauses directly to the z3 solver
- Optimize SAT constraints of puzzle from DNF
- partial assignments in Z3
- Choco Sat Formulation
- Yosys instruction "sat -dump_cnf "
- How to download sat file with angular and C#
- Optimize event seat assignments with Corona restrictions
- Finding a path through vertices in a graph with SAT Solving in Python
- 3-OCC-MAX SAT np-complete?
- Is MAX 3 SAT NP-complete or co-NP-complete?
- How many satisfying assignments are there in a set of 3-CNF clauses where no clause share the same variable?
- How can I express scheduling problems in minisat?
- "Check if a cycle of K nodes exists" reduction to SAT?
- Alloy6 allowing invalid state transitions
Related Questions in HORN
- Is "~A=>B" a horn clause?
- Horn SAT algorithm using graphs
- Signing an unsigned assembly
- What are the equivalent horn clauses to these clauses?
- What is a real-world application for HORN?
- Z3 returns unknown with HORN logic if I use a specific operation
- CNF vs Horn Satisfiability
- SVG with transparency
- Issues using a simple jQuery script to grab one div height & make another div the same size
- what's the meaning of "at-most" keyword in SMT-LIB language (extended version of Z3 FixedPoint)
- Using `Array` in the HORN logic in Spacer/Z3
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)
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?
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.