CNF vs Horn Satisfiability
I know that it's easier to prove if a horn-formula is satisfiable. My Question is: Why is it easier with a horn formula rather than a normal CNF?
Solution
Presence or absence of Horn satisfiability can be shown in linear time. Here is a good introduction with some examples. The solution can be found by unit propagation without backtracking.
Pseudocode from a UC Berkeley lecture note:
Satisfiability for general CNF expressions is a classic NP-complete problem. No polynomial time algorithms are known for CNF satisfiability (except if P=NP).
- Example of unique 3sat solution
- Algorithms with superexponential runtime?
- SAT can be verified in polynomial time, by a conversion to CNF, then verifying the SAT of the CNF in polynomial. What is wrong with this argument?
- How can I perform validity of ∃∀.φ, if I use quantifier elimination for ∀.φ and get φ'? I hypothetise ∃φ' solves satisfiability, not validity
- Is minimization of boolean expressions NP-Complete?
- Specifying modular arithmetic conditions in Z3
- z3 solver using Sympy symbols
- What does a model mean in a universally quantified formula? Is it a function?
- In Z3, I cannot understand result of quantifier elimination of Exists y. Forall x. (x>=2) => ((y>1) /\ (y<=x))
- Some questions about dReal: delta-satisfiability, parameter with 0.0, doing the same in Z3 and obtaining sat/unsat result
- Derivation in the Resolution Proof System
- Dimacs cnf expression not satisfiable, why?
- Generating DIMACS CNF file using bc2cnf is missing AND
- How to use soft constraints in Z3-Python to express 'abstract' biases in SAT search: such as 'I prefer half of the literals to be true and half false'
- How to bias Z3's (Python) SAT solving towards a criteria, such as 'preferring' to have more negated literals
- Some questions about incremental SAT in Z3: can it be deactivated? Which techniques are used inside?
- Z3-Python as SAT solver does not give right results
- Calling Z3 as black box from Ocaml
- Bounding number of allowable True/False in Z3
- Produce multiple models for CVC4 SMT queries
- Is satisfiability related to a set of sentences of a single sentence?
- finding max of the numbers in z3 using SMTLIB2
- Incremental weakening Maxsat
- Linear Sat Unsat vs Linear Unsat Sat
- Why is MAX-SAT a generalisation of the SAT problem?
- Checking satisfiability of First Order Formula using Z3
- Tool/Language to check Satisfiability of First order logic?
- Make a constraint more difficult to solve for a constraint solver?
- Dpll, SAT (satisfability) problem, Need DPLL Function or Procedure?
- CNF vs Horn Satisfiability