Questions tagged [satisfiability]

Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.

Filter by
Sorted by
Tagged with
-1 votes
0 answers
14 views

Clique to SAT example explanation

We are at college trying to implement the reduction of the clique problem to a SAT problem but I dont quite get the examples of the slides if someone can give me a not so technical explanation of what'...
user164639's user avatar
1 vote
2 answers
57 views

Complexity of satisfiability for relational logic on the booleans

I know that propositional satisfiability is NP-complete and that if I add first-order quantifiers I get the complete problems for the polynomial hierarchy and PSPACE. What happens if my formulas are ...
user1868607's user avatar
  • 2,184
1 vote
0 answers
48 views

How to find the learned clause from a UIP cut

I would guess that this question is going to make some people wonder how I haven't already found a solution looking through papers -- but I do not see a clear algorithm. In implementing CDCL, I read ...
Jack Sack's user avatar
0 votes
1 answer
17 views

How does the sumcheck protocol help solving the #SAT (circuit satisfiability) problem?

I am going through Justin Thaler's book - https://people.cs.georgetown.edu/jthaler/ProofsArgsAndZK.pdf - "Proofs, Arguments, and Zero-Knowledge" He presents the Sumcheck protocol & then ...
user93353's user avatar
  • 125
0 votes
0 answers
27 views

Number of clauses in SAT problems

I was going through the proof that DNF-SAT can be solved in polynomial time. The strategy was to go through all clauses, find a clause that doesn't contain both x and x' for any variable x and then ...
Aditya's user avatar
  • 1
1 vote
1 answer
82 views

Specialized SAT solver (?)

(Context) Given two byte arrays of length 16, say $L$ and $H$, one can define a mapping $M$ from the set of all bytes to itself in the following way. If $0 \le b \lt 256$ is a byte, let $\text{lo}(b)$ ...
fuzzypixelz's user avatar
0 votes
0 answers
31 views

Does the following down-voted answer not answer the question "Why does Schaefer's theorem not prove that P=NP?"?

Does the following highly down-voted answer not answer the question "Why does Schaefer's theorem not prove that P=NP?"? If not, why not? Marek, V. Wiktor. Introduction to Mathematics of ...
Geremia's user avatar
  • 148
0 votes
2 answers
59 views

Can any SAT problem be converted to a system of linear equations over $\mathbf{Z}_2$?

Can any SAT problem be converted into one with only affine formulas? Handbook of Satisfiability p. 672: Affine formulas. A linear equation over the two-element field is an expression of the form $x_1 ...
Geremia's user avatar
  • 148
0 votes
3 answers
82 views

Is there a 2SAT encoding for a NAND gate

I am trying to encode some circuit checking algorithms, but encountered difficulty creating a 2SAT representation for a NAND circuit. Is there a proof that this is not possible?
Hovercraft2's user avatar
1 vote
1 answer
66 views

A Fast Linear-Arithmetic Solver: How can Gaussian elimination be used to simplify matrix A?

I am working on an LRA Theory solver for SymPy, an open source python library for symbolic computations. You can find my work here. Currently I'm trying to optimize it to run faster. My implementation ...
Tilo RC's user avatar
  • 11
0 votes
0 answers
13 views

Reference request for Unit Clause Based SAT Reduction Rules

I tested my XSAT solver using the 4 pigeons in 3 holes problem converted to XSAT. The pigeon hole instance I give below had 108 variables and 88 clauses after being converted to monotone XSAT. My ...
Russell Easterly's user avatar
0 votes
0 answers
16 views

Reduction of $3SAT$ to $2P2N-3SAT$ (without trivial clauses)

Given an instance of $3SAT$ the objective is to reduce it directly to $2P2N-3SAT$ without the reduction having any 'trivial' clauses. The trivial clauses can be where the same variable in a clause is ...
J.Doe's user avatar
  • 753
4 votes
2 answers
87 views

Finding a vector of maximum Hamming distance from a subspace of $(\mathbb{Z}/2\mathbb{Z})^n$

Let $W$ be a linear subspace of the vector space $V = (\mathbb{Z}/2\mathbb{Z})^n$. Let $k = \dim(W)$. For $v \in V$, define the distance from $v$ to $W$ to be $d(v,W):=\min_{w\in W} d(v,w)$ where $d(...
Ben's user avatar
  • 141
0 votes
1 answer
43 views

Is it an open problem if CDCL algorithms violate SETH?

Strong Exponential Time Hypothesis states that general SAT, where clauses are not limited in length, can't be solved in time $o(2^n)$. It's proven that DPLL algorithm requires $\Omega(2^n)$ time in ...
rus9384's user avatar
  • 1,429
-1 votes
1 answer
36 views

Schaefer's dichotomy theorem and limits on the formula length

Schaefer's dichotomy theorem ensures than when a constraint satisfiability problem satisfies certain conditions, the problem is either in $\mathsf P$ or is $\mathsf{NP}$-hard. Suppose the following ...
rus9384's user avatar
  • 1,429
1 vote
0 answers
30 views

Shortest unsatisfiable 3-CNF that can't be refuted with narrow resolution?

Proof width (the size of the largest clause in a proof) plays an important part in refuting an unsatisfiable formula. If a formula has a bounded-width resolution proof of its unsatisfiability, then ...
Soha's user avatar
  • 25
0 votes
0 answers
67 views

if it were shown that every algorithm that solves SAT must have complexity Ω(n^(log n)) then P≠NP?

Shouldn't this statement be false? To be true the implication should be P=NP or am I wrong? I can't find a formal proof
PatrickBateman's user avatar
0 votes
0 answers
16 views

Complexity Class of the Problem: Existence of Unsatisfying Interpretations in Boolean Formulas

What is the complexity class of the problem if there exist two different interpretations that do not satisfy a given Boolean formula? I believe the problem of existence of an interpretation that does ...
Lupital's user avatar
0 votes
1 answer
487 views

Complexity of a variant of #Positive-2-SAT

#Positive-2SAT is the problem of counting the number of satisfying assignments to a given Positive 2-CNF formula i.e 2-CNF formulas in which each literal is a positive occurrence of a variable. The ...
Anuj's user avatar
  • 33
1 vote
1 answer
72 views

Why is conjunctive normal form (CNF) "better" for SAT than disjunctive normal form (DNF)?

When hand-manipulating algebra DNF (sum of products) is easier than CNF (product of sums). Possibly because factoring is more difficult than expanding. So why is it the opposite for computational ...
Stand with Gaza's user avatar
0 votes
1 answer
43 views

Should I remove equivalent variables in a CNF file to be used by a SAT solver?

My CNF file ends with many pairs of clauses that represent that two variables are equivalent (eg: -3 7, 3 -7, 5 -11, -5 11, etc.). Do most SAT solvers automatically pre-process these and replace every ...
Lewis Baxter's user avatar
0 votes
1 answer
40 views

How to solve boolean SAT with equality constraints

Say I have boolean formula in form of a CNF(x1,x2,...) with $x_i$ being boolean variables. Testing the satisfiability of the CNF is the SAT problem, i.e. determine ...
Andreas H.'s user avatar
0 votes
0 answers
67 views

Finding a Polynomial Time algorithm for the 3-SAT Problem

Let us consider m clauses containing 3 variables each i.e. A1,A2,A3...Am . Let the total literals in consideration be n. Then each clause : Ai = (xr $\lor$ xs $\lor$ xt) where 1 $\le$ r,s,t $\le$n and ...
Pathlessbark8's user avatar
-1 votes
1 answer
78 views

SAT polynomial time

Hi I understood it is not currently possible to solve SAT in polynomial time. Does this mean we can not currently solve an expression with n different boolean variables or with m different symbols in ...
Jip Helsen's user avatar
1 vote
1 answer
93 views

Boolean constraints for a connected component of a graph

Suppose I have an undirected graph $G=(V,E)$, and boolean variables $x_v$ (one for each vertex $v \in V$). These variables select a subset $S \subseteq V$ of vertices, namely the vertices $S=\{v \mid ...
D.W.'s user avatar
  • 156k
1 vote
1 answer
62 views

Encoding SAT EqualsK Constraint with Two Possible Values

I am wondering about a way to CNF encode an EqualsK constraint with two possible values. In other words, I want to solve for the equation: $$ (\sum_{i=1}^n x_i = A) \lor (\sum_{i=1}^n x_i = B) $$ ...
Tim Bersama's user avatar
1 vote
1 answer
43 views

Can you transform 3sat (or equivalent) into another satisfiability problem that increases the ratio of solutions to non-solutions

Say I have f(x1,x2,x3,...) where the output is either 0 for all inputs (unsatisfiable) or a variable boolean output of 0 or 1 depending on the input (satisfiable). Let's not consider functions that ...
Benedict Bien's user avatar
0 votes
0 answers
56 views

Why weakening rule doesn't increase the size of resolution refutation?

I am studying the complexity of SAT resolution refutation. There is a useful tool named weakening rule The weakening rule: B -->B ∨ C says that from a clause B we can derive the weaker clause B ∨ ...
Jxb's user avatar
  • 318
0 votes
1 answer
55 views

SAT with every variable occuring exactly once

With the Circuit-SAT problem, I often see the "split" gate (I don't know the official name of it). This gate has a truth table of: $$ \begin{array}{|c |c c|} 0 & 0 & 0\\ 1 & 1 &...
Loic Stoic's user avatar
0 votes
1 answer
44 views

What's the relation between DPLL and BDDs?

BDDs are a way of representing Boolean formulas. DPLL is an algorithm to determine satisfiability of Boolean formulas. My understanding is that the two are used for SAT solving. How are they combined?
user1868607's user avatar
  • 2,184
0 votes
0 answers
41 views

If $\overline{3SAT}\in BP\cdot NP$ then $PH=\Sigma_3^P$

I have the problem If $\overline{3SAT}\in BP\cdot NP$ then $PH=\Sigma_3^P$ To solve this I am using a result $BP\cdot NP\subset NP/poly$ which I can prove (not doing here). I have two solutions but ...
Soham Chatterjee's user avatar
0 votes
1 answer
68 views

Time complexity to convert a truth table to a boolean circuit

The SAT problem is often explained in terms of truth tables. Given some random boolean circuit, calculate its truth table; does there exist an output of $1$ in the truth table? But how about going the ...
Loic Stoic's user avatar
4 votes
0 answers
45 views

Benchmark of SAT solvers on random k-SAT instances at satisfiability threshold

I am looking for a solid reference (peer-reviewed publication) on the design and/or benchmarking of SAT solvers for random k-SAT ($4 \leq k \leq 8$) operating at satisfiability threshold. The majority ...
sbbn's user avatar
  • 41
0 votes
0 answers
10 views

Do you resolve all clauses in the processed bucket in the Davis-Putnam algorithm?

I'm reading the description and example of Davis-Putnam on page 102 of the Handbook of Satisfiability and I'm confused by the example they use. To start with, they fill the following buckets $C: \{\...
azani's user avatar
  • 101
0 votes
0 answers
12 views

Would proving that finding a satisfiable input is intractable prove that SAT is intractable? [duplicate]

With the SAT problem, there is a corresponding search variant. Given an arbitrary boolean expression, find a given input such that the output of the boolean expression is $1$. To my knowledge, this ...
Loic Stoic's user avatar
0 votes
0 answers
48 views

Is this a valid method to merge clauses in CNF formulas?

Assume $$C_1 = (x_1 \lor x_2 \lor \lnot x_3)\hspace{0.2cm} C_2 = (x_4 \lor x_5 \lor x_3) \hspace{0.2cm} C_3 = (x_3 \lor x_5 \lor x_6)$$ Let $$ \phi_1 = C_1 \land C_2 \land C_3$$ and $$ \phi_2 = (x_1 \...
C Marius's user avatar
  • 185
2 votes
0 answers
46 views

Modified DPLL for 3-SAT by reducing to 2-SAT

In Boolean Satisfiability of CNF formulae we have $k$-SAT where each clause has at most $k$ literals. It is well known that $k$-SAT is polynomial time reducible to $3$-SAT. It is also well known that $...
vvg's user avatar
  • 135
0 votes
1 answer
37 views

the size of nice tree decomposition

Recently, I am reading paper An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances, which use tree decomposition to give an upper bound for SAT resolution refutation. For a ...
Jxb's user avatar
  • 318
0 votes
1 answer
37 views

Complexity of this variant of the Monotone(+,2−) -SAT problem?

In this post,Monotone$(+, 2^-)$-SAT problem is defined as follows: Given a monotone CNF formula $F^+$, where each variable appears exactly once (as a positive literal), and a monotone 2-CNF formula $...
Anuj's user avatar
  • 33
1 vote
1 answer
61 views

Is Horn-SAT with XOR-relations NP-complete?

I was wondering if the combination of Horn-SAT and XOR-SAT is solvable in polynomial time or not. It seems they can be solved in polynomial time as both are in class P and also that Horn-SAT is P-...
Anuj's user avatar
  • 33
1 vote
1 answer
19 views

Are the indices of variables in the formula variable?

Let $L$ be an arbitrary language in $\Sigma_3$. Thus it can be written that $x \in L \Leftrightarrow \exists y^{p(|x|)} \forall z^{p(|x|)} \exists w^{p(|x|)} \langle x,y,z,w \rangle \in B$ where $p(\...
advocateofnone's user avatar
1 vote
1 answer
50 views

Encoding "all-except" constraints in CNF

I am looking for an efficient CNF encoding of the following situation: I have sets of boolean literals $A = \{ a_1, \ldots, a_m \}$, $B = \{ b_1,\ldots, b_n \}$ and subsets $B_1, \ldots, B_m$, where ...
Markus's user avatar
  • 166
1 vote
0 answers
54 views

Restricted Planar 3-SAT NP-hard

As we all know, 3-SAT is NP-hard. Two of the less known results are that Planar 3-SAT is NP-hard and also a 'restricted' 3-SAT, where any literal appears in at most two clauses turns out to be NP-hard....
Freshman's Dream's user avatar
1 vote
1 answer
66 views

Understanding the Strong Exponential Time Hypothesis

Let $n$ be the number of variables in the input formula and $m$ the number of clauses. Define $s_k = \inf\{\delta : k\text{-SAT can be solved in } 2^{\delta n} \text{ time}\}$. The strong exponential ...
Soha's user avatar
  • 25
2 votes
0 answers
36 views

Problems with proof of NP-completness of SAT following Cooks original paper

I am currently in the process of trying to understand the original proof of NP-completeness of SAT given in the seminal paper by Cook [COOK71] and have struggled with a few of the details of the proof ...
Thomas Tappeiner's user avatar
0 votes
2 answers
53 views

Finding a 2SAT instance that has a specific solution set

Is there a 2SAT instance of variables $(a,b,c,d,e,f,g)$ that has exactly the solution set $S=\{ (1,0,0,0,0,0,0),(0,1,0,0,0,0,0),(0,0,1,0,0,0,0),(1,1,0,1,0,0,0),(1,0,1,0,1,0,0),(0,1,1,0,0,1,0),(1,1,1,1,...
DrownedSuccess's user avatar
1 vote
1 answer
80 views

Is there an SMT/SAT algorithm for General Predicate Logic (FOL)?

I'm learning how to write my own theorem prover. After skimming Decision Procedures (Kroening & Strichman, 2016), I didn't find any SMT algorithms for solving quantified n-ary predicate formulas. ...
Vivek Joshy's user avatar
1 vote
1 answer
136 views

Variation of 3-SAT

I already know that SAT and 3-SAT are NP-complete. If in 3-SAT the Boolean expression should be divided to clauses,such that every clause contains at most (in the original problem it says exactly) ...
Hjm's user avatar
  • 47
1 vote
1 answer
101 views

How to reduce 3SAT to TwoOrMoreSAT?

I want to prove, that 2OrMoreSAT is NP-complete. It's defined as follows: A formula is considered strongly satisfiable if there exists a model such that two or more different literals in every clause ...
Rahjid Domal's user avatar
0 votes
1 answer
85 views

MAX-SAT approximation factor

I am stuck on an exercise that ask the approximation factor of a MAX-SAT approximated algorithm generalized from a MAX-3SAT algorithm MAX-3SAT: set every variable with a random value ($0$ or $1$ each ...
Marcus34's user avatar

1
2 3 4 5
14