# Tag Info

15

The monotone version of X3SAT that your proof is based on has the nice property that setting a literal false in one clause will never cause the negation of that literal to be true in another, which means you can say The only way a conflict can occur is when all literals in a clause are set to false. and it will be true because forcing two literals false ...

9

There is some research in this area. In The Effect of Restarts on the Efficiency of Clause Learning Jinbo Huang shows empirically that restarts improve a solver's performance over suites of both satisfiable and unsatisfiable SAT instances. The theoretical justification for the speedup is that in CDCL solvers a restart allows the search to benefit from ...

5

Let me recap the proof. We are given a sparse NP-hard language $A$: for each length $n$, there are at most $n^c$ strings of length $n$ in $A$. For a satisfiable CNF $\varphi$, let $a(\varphi)$ be the lexicographically first satisfying assignment for $\varphi$. We consider the NP language $B$, which consists of all pairs $(\varphi,w)$ such that $\varphi$ is ...

5

TL;DR: They differ in their basic input and output. SAT and SMT solvers don't know what programs are; they are tools that answer yes or no questions about mathematical formulas. Symbolic execution, on the other hand, is a method of analyzing programs. Symbolic execution usually relies on SAT and SMT solvers, but not the other way around. SAT and SMT solvers ...

5

There are competitions for constraint satisfaction solvers. Some problems there can be readily translated to IP solvers as well. See e.g., MiniZinc challenge which has taken place yearly since 2008 or the XCSP competition.

5

There are no competitions targeting general integer programming or mixed integer programming, but there are (or were) benchmarks, such as the MIPLIB (linear) and the MINLPLIB (nonlinear). There are competitions for subsets (PB, SAT, max-SAT) and for constraint programming, as you and other answers pointed out. You can find many competitions (DIMACS ...

4

Your problem is known as Weighted-2-satisfiability, and is known to be NP-complete. The easiest way to see that is by reduction from Vertex Cover (exercise). Note that the link above is about whether there is a satisfying assignment having at most $k$ true variables. This is equivalent to your problem (exercise).

4

Yes. You can solve this in polynomial time. The same strategy as in Are SAT problems with at most one false clause NP-complete? works. Let $\varphi$ denote the CNF formula you care about, and $n$ the number of variables in $\varphi$. Let $A_{i,j}$ denote the number of truth assignments that do not satisfy clauses $i$ or $j$ of $\varphi$, let $A_i$ denote ...

4

Yes, a 3-SAT formula $\phi$ can be transformed into a 1-in-3 SAT formula $\phi'$ while preserving the number of satisfying assignments. To avoid ambiguities I will use "$\vee$" between literals of a 3-SAT clause, and commas between literals of a 1-in-3 SAT clause. Let me preliminarily show that, given two literals $a$ and $b$, we can simulate a new type of ...

4

The result you are trying to prove is known as Mahaney's theorem. It is covered by textbooks on complexity theory, and in many online lecture notes. The proof in Jonathan Katz' lecture notes indeed uses LEXSAT.

3

I think there is some confusion here. MAX-2-SAT is NP-Hard (and its decision version is NP-Complete), while 2-SAT is in P and hence also in NP. This means that 2-SAT is polynomial-time reducible to (the decision version of) MAX-2-SAT. The converse is not true unless P=NP. Let $\phi$ be a 2-SAT formula with $m$ clauses. If you really want to reduce an ...

3

For 3SAT, the number of variables is polynomially related to the number of clauses. (See the end for the justification.) Consequently, any algorithm for 3SAT whose running time is polynomial in the number of clauses would also be polynomial in the number of variables; and any algorithm for 3SAT whose running time is polynomial in the number of variables ...

3

I'll assume all of the equations take the form $x_i + \cdots + x_j = 0$ (i.e., always 0 on the right-hand side). Then, your problem is: given a boolean matrix $M$, find a $x$ such that $Mx=0$ (modulo 2) that minimizes the Hamming weight of $x$. I think this is equivalent to the problem of finding the minimum-weight codeword of a linear code. That problem ...

3

All the literals in a conflict clause are set false by definition, else there would be no conflict. So if the clause $\overline{b_1}\lor\overline{b_2}$ existed, one of those false literals would have caused that clause to go unit before we reached the current level, which in turn would have forced one of the $\overline{b_1}$ or $\overline{b_2}$ literals ...

3

The variant where $A=B$ is known as monotone not-all-equal 3-satisfiability, i.e., Monotone NAE3SAT. According to Wikipedia, it is NP-complete. It is not the same problem as Monotone-3-SAT.

3

QSAT with only 2 literals per clause was shown to be in P back in 1979. Since the $\Sigma_k$ and $\Pi_k$ versions of QSAT can be reduced to equisatisfiable problems with 3 literals per clause using only a slight modification the method used to transform a SAT instance to 3SAT (i.e. putting all the new variables in the innermost existential group), those ...

3

Yuval describes the general approach. Let the binary representation of the two numbers be $n_1,\dots,n_k$ and $m_1,\dots,m_k$, where $n_1$ is the most significant bit. Introduce fresh new boolean variables $t_1,\dots,t_k$. The intention is that these will indicate the common prefix of $n,m$. In particular, add the following clauses: $t_{i+1} \implies ... 3 With SAT, it can be challenging to predict what will be feasible and what won't. It's worth a try. I would suggest that, instead of MinSAT, you first try using binary search on$n=|\mathcal{S}|$, the number of sets you need. You can use an at-most-$n$-out-of-12376 constraint on your$X_S$variables. There are several techniques for encoding that in SAT, ... 3 Optimization with SAT is usually referred as MaxSAT instead of Min SAT. In particular, I suggest looking for solvers for "weighted partial MaxSAT", for example MaxHS and RC2. The problem size you have is fairly small in the context of modern MaxSAT-solvers, so yes it is worth trying. There are no guarantees that the solver will work efficiently, and it is ... 3 Given a CNF with$n$variables and$m$clauses, we denote by$A_i$the set of truth assignments that do not satisfy clause$i$. Then the number of satisfiable assignments is $$2^n-\left|\bigcup_{i=1}^m A_i\right|.$$ Since each assignment makes at most one clause false,$A_i$and$A_j$are disjoint for$i\neq j$. Also note$|A_i|=2^{n-n_i}$where$n_i$is ... 3 As far as I can tell the earliest mention of the procedure you outline, later described in the literature as variable elimination by clause distribution, was in the paper "ZRes: The old Davis-Putnam procedure meets ZBDD" by Philippe Chatalic and Laurent Simon. The procedure was described again, along with other formula simplification techniques, in "... 3 Such a reduction is described in Appendix B of Régis Barbanchon, On unique graph 3-colorability and parsimonious reductions in the plane. Barbanchon attributes it to previous work ([9] in the bibliography). Elsewhere, I have seen an attribution to Schaefer's celebrated paper in which he proves his famous dichotomy theorem, among else giving a reduction from ... 3 This sounds to me like the Knapsack problem where$z$is the weight of each item,$Z$is the capacity of the knapsack,$g$the value of the item, and$G$the value to be achieved. The problem is NP-complete but solvable, using dynamic programming, in pseudo-polynomial time$O(n \cdot W)$where$W = \max_{(z,g) \in R}(g)$. You can prove that the Knapsack ... 3 There was a Pseudo-Boolean solver competition from 2005-2012, but (as far as I can tell) nothing since then. Integer Linear Programming is a subset of Pseudo-Boolean programming. See the 2012 competition page for results and links to other competition results. 2 To show that Vertex Cover and 3SAT is "equivalent", you have to show that there is a 3SAT satisfaction if and only if there is a k vertex cover in the graph constructed in the reduction step. Assuming you are familiar with how the reduction is done, (if not ,refer to the document). Since you only asked about how this setup proves that if there exists a k-... 2 There are many ways to reduce CLIQUE to SAT. Probably the simplest is as follows. Suppose that we have a graph$G = (V,E)$, and interested in a$k$-clique. We will have$k|V|$variables$x_{iv}$, whose intended meaning is "the$i$th vertex of the clique is$v$". The constraints are: There is an$i$th vertex: for all$1 \leq i \leq k$,$\bigvee_{v \in V} x_{...

2

do we know for which $n_0$ these assumptions "kick in" in the case of $3-SAT$? Can we generate, or at least be confident of the existence of a relatively small formula ($< 200$), such that every algorithm requires $\sim2^{200}$ operations? $3-SAT$ is known to be solvable in time $O(1.321^n)$. Therefore, there is no instance that would force a $\Omega(2^... 2 Here is an$n^{O(k)}$-time SAT algorithm: try all (at most$n^k$) ways how to select one literal from each clause, and accept whenever the selection is such that it does not include any contradictory pair (i.e., a literal and its negation). So, if$k$is substantially smaller than$n$, you get a subexponential algorithm, and you should not be able to prove ... 2 Let me first give a concrete example of a formula$F(x,y)$such that$\forall x \exists y. F(x,y)$is true, but$\exists x \forall y. F(x,y)$is false. I'll then address the expansion of the universal quantifier in your question. Take$F(x,y)$to be a formula expressing the equality$x \oplus y = 1$, where$\oplus$denotes exclusive-or. We can explicitly ... 2 As confirmed independently in another answer, 2P2N-3SAT is already NP-complete. Another name for the fragment you are interested in is (3, B$k$)-SAT where "B" stands for Balanced and indicates that there are the same number of positive and negative occurences of the variables,$k\$ is the number of positive and the number of negative occurences, and the 3 ...

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