Hot answers tagged

2

Hint:


2

In the case of 2SAT, resolving two clauses does not increase their width (the width of a clause is the number of literals appearing in it). This is not the case for 3SAT, where resolution could increase the width. For example, if we resolve $a \lor b \lor c$ and $\lnot a \lor d \lor e$, both of width 3, we get the clause $b \lor c \lor d \lor e$ of width 4. ...


2

No, you can't. If each clause has at least one positive literal, then, by assigning TRUE to all variables, one gets all clauses satisfied.


1

I've implemented my own CDCL solver (which is the main modern variant of DPLL), and I found that the hardest part by far was understanding and implementing the 1-UIP heuristic, which in my opinion is well-motivated but not very well-explained in the literature. If you want to see how fast and simple SAT solvers can be, check out Tinisat. It's only around 500 ...


1

If you're determined not to use the standard deterministic algorithm, the usual alternative is what's known as local search or stochastic search. The basic idea is that you start with a random bit pattern as a variable assignment, observe what's wrong with it in terms of unsatisfied clauses and try to improve it by flipping one or more variable assignments. ...


1

You can show a reduction in polynomial time from the standard 3-SAT problem where the number of variable occurrences are unrestricted to the specific version of 3-SAT with utmost three occurrences per variable in order to prove it's NP-Hard. This reduction is explained well in the classic paper by Craig A. Tovey in section-2. As @DavidRicherby explained, ...


Only top voted, non community-wiki answers of a minimum length are eligible