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
0 votes
1 answer
40 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 ...
Björn Lindqvist's user avatar
0 votes
1 answer
36 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
17 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
54 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
42 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
17 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
  • 152k
1 vote
1 answer
52 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
0 votes
1 answer
26 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
48 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
  • 176
0 votes
1 answer
29 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
25 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,230
0 votes
0 answers
27 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
36 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
28 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
8 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
11 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
28 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
42 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
30 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
  • 176
0 votes
1 answer
21 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
  • 55
1 vote
1 answer
42 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
  • 55
1 vote
1 answer
18 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
44 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
34 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
48 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
  • 15
2 votes
0 answers
33 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
47 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
55 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. ...
daegontaven's user avatar
1 vote
1 answer
60 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
  • 37
1 vote
1 answer
69 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
56 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
3 votes
1 answer
69 views

Finding a minimal set of package versions in a dependency graph with constraints

Suppose you have a dependency graph of "packages" registered in the ecosystem of a given programming language. We can model each package as a tuple ...
tom's user avatar
  • 133
1 vote
1 answer
48 views

Question about a proof of the existence of unsatisfiable linear k-CNFs for any k

Today I am reading paper Unsatisfiable Linear k-CNFs Exist, for every k by Dominik Scheder, 2007. But I have some problem to understand the proof of Theorem $3.2$. I don't know how to understand the ...
Jxb's user avatar
  • 176
0 votes
1 answer
28 views

How to get the formal model using propositional logic

Input There are three chairs (1,2,3) in the same row. We need to find a seat for three guests (a,b,c). Constraints The first guest does not want to be seated next to the third one (neither left nor ...
yeahman14's user avatar
0 votes
1 answer
109 views

Why solving #2SAT in polynomial time implies P = NP?

The wikipedia article for #P states that if we have a polynomial-time algorithm for a #P-complete problem, P = NP is true. As #2SAT is #P-complete, this would mean that providing a polynomial-time ...
tonik's user avatar
  • 195
2 votes
1 answer
64 views

NP-hard $k$-SAT variant with exactly $\ell$ occurrences per variable

For the purpose of this post, let $k$-SAT be SAT with exactly $k$ literals per clause, as opposed to the more common meaning of at most $k$ literals per clause. With the purpose of proving some ...
J. Schmidt's user avatar
9 votes
2 answers
5k views

Is SAT an existential question?

Some sources state that an algorithm that solves the SAT problem not only needs to decide whether a given existentially-quantified formula is satisfiable or not, but, additionally, in the case where ...
tonik's user avatar
  • 195
1 vote
1 answer
40 views

Possible to solve a combinatorial game with integer programming?

I recently had the idea that it would be neat if it were possible to make a SAT solver play combinatorial games. To start, I'm trying a relatively simple case of solving single-stack Misère Nim ...
Exalted Toast's user avatar
1 vote
0 answers
90 views

CNF – satisfy at most a fixed number of clauses

I'm working on this task: Prove that the following problem can be solved in time $2^{k} \cdot \Vert \varphi \Vert^{\mathcal{O}(1)}$: given a boolean formula $\Vert \varphi \Vert$ in CNF, decide ...
dawmd's user avatar
  • 65
0 votes
1 answer
53 views

Logical Consequence - Equivalent Assertions

I have the following slide in my notes and I'm having trouble understanding how the three assertions are equivalent. I understand to a degree how the 2nd and 3rd assertions are equivalent, but the ...
A. Boy's user avatar
  • 1
0 votes
1 answer
67 views

Running time of SAT and other EXPTIME algorithms

I need to propose an algorithm for a NP-hard problem. I use dynamic programming which leads to a running time $O(2^s\cdot n^2), s\leq n.$ The algorithm aims to finding a path in a graph $G(V, E)$ (in ...
user153448's user avatar
1 vote
1 answer
43 views

Is ANF-SAT P or NP?

Given a finite set of equations in ANF, for example: $$ \begin{cases} (x_1 \land x_2) \oplus (x_1 \land x_3 \land x_4) \oplus 1 = 0 \\ x_3 \oplus (x_2 \land x_3 \land x_4) = 0 \\ (x_1 \land x_4) \...
Omid's user avatar
  • 13
2 votes
1 answer
1k views

Why can't 3-SAT be solved efficiently if you convert all clauses (x ∨ y ∨ z) into (u ∨ z) by introducing a variable?

Let $a_i$, $b_i$, etc., be a literal, i.e., a variable or the negation of a variable. 3-SAT concerns formulas in CNF form: $(a_1 \vee a_2 \vee a_3) \wedge \dots \wedge (b_1 \vee b_2 \vee b_3)$ (3-CNF)....
D Left Adjoint to U's user avatar
0 votes
0 answers
25 views

Given an instance of a HORN-SAT problem with at most 3 literals per clause, what context-free grammar is equivalent to deciding the problem?

Given an instance of a HORN-SAT problem with at most 3 literals per clause, what context-free grammar is equivalent to deciding the problem? For example, here are some HORN clauses: ...
Jesus is Lord's user avatar
-1 votes
1 answer
159 views

How to prove that P = NP?

So if someone proves with an algorithm that SAT can be solved in deterministic polynomial time, then P = NP and that's it?
just_learning's user avatar
1 vote
1 answer
66 views

Simple Skolemization Question

Is it correct that, under a certain signature S, two First Order Logic formulae F and G are equisatisfiable if (F is satisfiable under S iff G is satisfiable under S)? But in Skolemization I’m ...
Abhishek Manikandan's user avatar
2 votes
0 answers
30 views

Reductions from 3-SAT that won't work directly from SAT

Our prof talked about why it's good to know that 3-SAT is NP-complete because it's easier to craft reductions from it than from plain SAT. However, all the examples we've seen (reduction to ...
No one's user avatar
  • 21
0 votes
0 answers
95 views

Polynomial Reduction from 3SAT

Given an undirected graph $G=(V,E)$ where $V$ is a set of vertices, and $E$ is a set of edges and given a set $D$ where $D \subseteq V $ and $ \forall v \in V \setminus D \: \mid \: \exists w \in D : ...
Emily's user avatar
  • 1
0 votes
0 answers
46 views

Could we know what's the total number of unsatisfiable 3SAT formulas for a given n variables?

given some $n$ variables I would be interested to know what is the count of all 3SAT formulas under $n$ that are unsatisfiable. An example of all 3SAT forumlas under $n=3$ is the following: $$ ( x \...
matan Pleblist's user avatar
1 vote
1 answer
46 views

Reducing a mixed Boolean expression containing XOR of conjunctions

I know that XOR-SAT can be solved in polynomial time using arithmetic in $F_2$ and Gaussian elimination. I have a set of formula that is of the form $$ G_i := \oplus_{j=0}^{i} \left ( a_j \land b_{i-j}...
vvg's user avatar
  • 135

1
2 3 4 5
13