Xavier Labouze
  • Member for 10 years, 5 months
  • Last seen more than a month ago
About Inverse 3-SAT
3 votes

Answer : Yes (even if $I$ is a subset of some model of $\phi$) Let $R_{|I}$ the set of clauses that derive from $F_{\phi} \cup F_{\phi|I}$ by all possible 3-limited resolutions and subsumptions ($R_{|...

View answer
Unique $k$-SAT benchmarks
2 votes

You can easily generate directly Unique SAT formulas with reasonable size $(|F|<n+2^k)$ Let $m$ be the unique model - say $m$ contains only "0"s (rename the variables later if needed). Let $F$ a $...

View answer
Complexity of the $(3,2)_s$ SAT problem?
2 votes

Here is a paper by Porshen and Speckenmayer : Satisfiability of mixed Horn formulas which shows that even when $F_3$ is Horn, the problem of deciding the satisfiability of $F_3 \wedge F_2$ is NP-...

View answer
Surveys in other languages than English
1 votes

To open the list, here is a survey on SAT in French by Cristina Bazgan: Optimisation Combinatoire : problèmes paradigmatiques et nouvelles problématiques, Hermes, ed. Vangelis Paschos, pp. 21-50, ...

View answer
A variant of Critical SAT in DP
-1 votes

May I propose an answer to my own question thanks to your comments : the variant of Critical SAT is in P. Let us call "Problem 1" the variant of Critical SAT : Given a 3-CNF expression $F$, is it ...

View answer