Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
1
vote
1answer
17 views
Reducing 3SAT to MAX-3SAT
I have the following problem:
Consider the MAX-3-SAT problem: given a Boolean function in
Conjunctive Normal Form (CNF) determine the maximum number of clauses
that can be satisfied. Prove that ...
0
votes
1answer
23 views
n-DNF boolean formula k satisfiability
Given an n variable boolean DNF formula and a number k, does this formula has satisfying input combination greater than k?. (0<=k<=2^n).
Where input is infinite number of n tuples where ...
1
vote
0answers
24 views
Is the solution to Independent Set or Vertex Cover from 3-SAT optimum?
There are plenty of resources online discussing 3-SAT reductions to Independent Set or Vertex Cover problem. I am unable to find a resource which states that a satisfiable assignment to 3-SAT results ...
1
vote
0answers
21 views
3-SAT wher each literal appears at most once [duplicate]
I'm currently following a course and we have to prove that a restricted version of the 3-SAT decision problem where each literal appears at most once is solveable in polynomial time.
I think such a ...
1
vote
1answer
35 views
Why not do these checks on the number of clauses in 3-SAT?
I've been writing a 3-SAT solver for fun and comparing its performance against the solver pycosat. My solver vastly outperforms pycosat in two special cases, where I solve by doing simple, obvious ...
1
vote
1answer
28 views
Why is Max SAT in P if SAT in P?
It holds that if SAT could be solved in poly time, one can also find in poly time the assignment that satisfies most clauses of the original formula.
Does anyone have any idea how to show this?
Let's ...
2
votes
1answer
119 views
Directed HAM Cycles with Additional Constraints to SAT
The $n$ dimensional hypercube $Q_n$ is a graph that has a vertex $v_s$ for each string $s \in \{0, 1\}^n$ and an edge between two vertices $v_s$ and $v_t$ if and only if the Hamming distance between $...
3
votes
1answer
462 views
In SAT, do we require an assignment for arbitrary variables?
I am reading about the Satisfiability Problem, in page (5) the author gives the following example :
$(P \lor Q \lor R) \wedge
(\bar{P} \lor Q \lor \bar{R}) \wedge
(P \lor \bar{Q} \lor S) \wedge
(\bar{...
0
votes
1answer
16 views
Sat instance size and definition of TIME(f(n))
Sat usually is defined as the language of a 'reasonable' encoding of satisfable Cnf formulas over n variables.
Question: a Cnf formula over n variable with m clauses has a size (as a function of n) ...
4
votes
0answers
82 views
Maximum-minimum-satisfiability [closed]
In MAX-SAT, we are given a formula and want to maximize the number of satisfied clauses. I.e., given a formula $\phi = c_1 \cap \cdots \cap c_n$, where each $c_i$ is a disjunction, we want to find the ...
1
vote
0answers
20 views
Proof that MAX-2-SAT is NP-hard [duplicate]
According to Wikipedia, while the 2SAT problem is polynomial, its maximization variant MAX2SAT is NP-hard. But, they do not provide a reference for this claim. Is this obvious? If not, where can I ...
1
vote
1answer
20 views
NP-completeness and reduction of MAX-XOR-SAT and MAX-2-XOR-SAT
It is often stated that the MAX-XOR-SAT problem is NP-hard, and that likewise is the MAX-2-XOR-SAT problem. However, I cannot find a reduction from SAT to either of these problems, nor a proof of NP-...
2
votes
1answer
12 views
General structure of solutions to 3-SAT circuits
Certain special forms of the SAT problem have solution sets of a special form. For example, given any three solutions to a 2-SAT circuit, their bitwise median is also a solution. Likewise, given any ...
3
votes
1answer
13 views
Variance of MAXSAT clause satisfiability
For a given MAXSAT problem, it is trivially easy to compute the mean number of clauses satisfied for all assignments, or equivalently the expected number of clauses satisfied by a random assignment.
...
0
votes
1answer
76 views
2SAT Problem using Implication Graph
I was doing a practice question. As you can see below there is an Implication graph. To check whether the problem is satisfiable, I checked whether there were any 'bad loops'. To do so, for each ...
4
votes
2answers
120 views
Is there a way to convert a program into a Boolean formula?
Let's say I have a program P, in form of a binary code for x86 architecture.
I want to find a Boolean formula F (in form of CNF, or something like that), such ...
-1
votes
1answer
46 views
How many solutions are there for a XOR-SAT formula? [closed]
Does anyone know how many solutions there are for a XOR-SAT formula? And how do the variables in solutions distribute? For example, if (x0=1, x1=0, x2=1) is a solution for a XOR-SAT formula, how does ...
1
vote
1answer
14 views
what does it mean to extend an assignment?
For a constraint satisfaction problem, what does it mean for an assignment x to extend an assignment a?
Sorry if this is super trivial, I did not find an answer
e.g here: No Small Linear ...
0
votes
1answer
49 views
Given a NP Algorithm for SAT, do we expect to have Correct and Incorrect Solutions?
I am reading about Boolean Satisfiability Problem and Nondeterministic Algorithms, in the latter defination it says :
In computational complexity theory, nondeterministic algorithms are ones that, ...
0
votes
0answers
43 views
Number of X3SAT Instances?
Exactly 1 in 3SAT (X3SAT) is known to be NP-Complete. It remains NP-Complete even if we only consider instances that are monotone and linear. Monotone means all of the literals are positive. Linear ...
1
vote
0answers
32 views
What can be a Zero Knowledge Proof of a working SAT Algorithm?
Me and my colleague are exploring new ideas to solve SAT efficiently (i.e. in polynomial time) and it's the case that there is a candidate algorithm.
Unfortunately, neither of us can write scripts ...
3
votes
1answer
63 views
SAT for positive CNF clauses with exactly half of the variables being true
I am focusing here on positive even SAT problems, that is a CNF for which all literals are positive, and in which an even number n of variables occur. This is obviously trivial : just set all ...
2
votes
2answers
208 views
Why SAT Requires A Non-determinstic Algorithm?
I am getting started to understand the probelm of Satisfiability and i am reading (Computers and Intractability: A Guide to the Theory of NP-Completeness).
I do understand the difference between a ...
0
votes
1answer
90 views
Alternate reduction from 3SAT to 4SAT?
It seems that the standard reduction method you see online from 3SAT to 4SAT is that we let $\phi = (a \lor b \lor c)$ be a 3SAT clause, and so there is an assignment that satisfies $\phi$ iff $\phi' =...
0
votes
0answers
30 views
Proof of the Cook-Levin Theorem - snapshot transitions
I'm trying to understand the proof of the Cook-Levin thereom in Aurora and Barak's "Computational Complexity" text.
A snapshot $z_i$ of $M$’s execution on some input $y$ at a particular step $i$ is ...
1
vote
1answer
101 views
P=NP giving a deterministic algorithm for SAT
I'm trying to prove the following problem:
Prove that if $P=NP$ then there is a polynomial time algorithm for the following problem:
INPUT: A boolean formula $\phi$.
OUTPUT: A satisfying ...
2
votes
1answer
260 views
Proving special case of SAT is in P
Let SAT-100 be the following problem:
Input: Any boolean logic formula
Output: True if there exists a combination of exactly 100 input variables that satisfy the formula.
This is the description of ...
1
vote
1answer
31 views
Preserving a propositional formula
I know I must be getting stuck on notation. However, I'm having trouble following the logic in Example 1.2 in https://arxiv.org/pdf/cs/0611018.pdf. They define what preserving a propositional ...
1
vote
1answer
58 views
Is any sudoku solver an SAT solver?
I have recently created a sudoku solver using C#, which outputs the solution to a sudoku after a reasonable amount of time in many cases. I have used the basic sudoku SAT-reduction (i.e. x111 meaning ...
2
votes
1answer
54 views
When is a 1-in-3 SAT clause satisfied?
How does exactly 1 in 3 sat work given the variables Xi, Xy, Xz if one of the variables in the formula are negative.
We know that the results are if they are all positive given that:
R(Xi, Xy, Xz) =
...
1
vote
0answers
62 views
General Understanding of SMT Solving Across Multiple Theories
My first question was a little too simplified in that it turned out to be an integer linear programming problem solvable with the Simplex Method. However, what I think I am wondering about is how to ...
3
votes
1answer
96 views
How the Abstract DPLL Algorithm Works in SAT Solving
I have come across many definitions of the DPLL algorithm but haven't been able to follow them. The ones that are closest to making sense to me are the ones based on state-transition systems with ...
-2
votes
1answer
43 views
How a SMT / SAT Solver Generates Valuations for this Example
First, an example of a set of constraints which turned out not to be solvable (I don't think):
...
2
votes
2answers
88 views
Circuit satisfiability problem : SAT-C to SAT-2C
I have the following language : $L=\{\langle C_1,C_2\rangle \text{ | } C_1 \text{ and } C_2 \text{ are two circuits that calculate different function}\}$. We can call this language SAT-2C.
Prove that ...
0
votes
0answers
26 views
On $\Sigma_kSAT$ algorithms from $\Sigma_{k'}SAT$ where $k'<k$
Define $\Sigma_kSAT$ by 'Given a quantified boolean formula $φ=∃y_1∀y_2\dots Q_ky_k ϕ(y_1,\dots,y_k)$ where $ϕ(y_1,\dots,y_k)$ is boolean predicate with each $y_i$ a vector of variables, $Q_{2j−1}=∃$ ...
1
vote
2answers
258 views
What are known 3SAT to 2SAT reductions?
Is there a way to convert a 3SAT formula into a equisatisfiable 2SAT formula? Each method is of interest, even those that grow exponentially.
(So if, for example, my 3SAT formula has 16 variables and ...
0
votes
0answers
29 views
USAT, Arora Barak's book
Here on the page 354 Arora and Barak write below the shaded area
"but in fact $f(\phi)$ $\notin SAT$"
and not
"but in fact $f(\phi) \in SAT$"
While in the last line of the shaded area they write
$...
0
votes
0answers
37 views
Is my logic correct and is this a new reduction and algorithm from 3 SAT to clique?
Is my logic correct? If so, is this a new reduction and algorithm from 3 SAT to clique? I could only find one SAT to clique reduction; it wasn't this.
Definitions:
A clause group of a SAT instance ...
3
votes
1answer
38 views
Lower upper bound on # variables in k-SAT with m clauses
If I have an instance of $k$-SAT with $m$ clauses, then a trivial upper bound on the number of variables $n$ is given by $n \leq mk$. But we can only have $n = mk$ when no variable is repeated and ...
2
votes
1answer
282 views
Reduce Max-Cut to Max-2SAT
I would like to find a reduction from Max-Cut to Max-2Sat.
Could someone shed light on this problem, preferably spiced with some intuition?
Thanks,
Matan.
0
votes
1answer
28 views
Is there an algorithm to find out if a truthtable can be represented as 2-sat, and if so find its 2-cnf?
I know that not all truthtables have a corresponding 2-cnf representation, but is there a way to find out if a given truthtable has a 2-cnf representation, and if so to find what that is?
-1
votes
1answer
157 views
NP-completeness of vertex cover
Show that the following language is NP-complete
$$ L = \{ \langle G,k \rangle \mid \text{$G$ is a graph with a set $S$ of $k$ vertices hitting every edge of $G$}\}. $$
I know I should reduce the ...
-1
votes
1answer
594 views
To prove 4-SAT CNF is NP-complete [closed]
To answer the question below,
4-SAT: Given a formula in Conjunctive Normal Form, where each clause contains exactly 4 literals, does it have a satisfying truth assignment?
I was going to prove that ...
0
votes
0answers
47 views
$SAT$ and $BPP=P$ conjecture?
$BPP$ is the complexity class that accepts all languages for which there is Poly time TM with at least $1/3$ of their computation paths accept and rejects all languages for which there is Poly time TM ...
2
votes
1answer
49 views
Are there any techniques for checking whether a clause is subsumed by another clause when adding it to a cnf formula?
When doing variable elimination on a formula in cnf form, there is created a lot of new clauses. Is there any efficient way to check if these are subsumed by other, already existing clauses?
0
votes
1answer
55 views
Reducing INDSET and MAXCUT to 3SAT
Given a graph and an integer $k$ is there an independent set larger than $k$ is INDSET problem and is there a cut larger that $k$ is the MAXCUT problem. Is there standard way to convert to 3SAT from ...
1
vote
1answer
28 views
When using resolution variable elimination to simplify a cnf, does that change the truth values of the other variables?
When you use resolution variable elimination to preprocess/simplify a formula in cnf form the resulting formula is equisatisfiable.
What I wonder about is if I can use this technique to remove ...
-1
votes
1answer
49 views
Counting (enumerating) minimal solutions of a dual horn formula
Is there an efficient algorithm ("does not necessarily have to be a polynomial time algorithm") to compute all "minimal" solutions for a Dual Horn formula (conjunction of clauses where each clause ...
1
vote
1answer
165 views
3-SAT reduction to jobs scheduling problem (np-completeness)
In this paper with the title of "NP-Complete Scheduling Problem" by J. D. Ullman, I am trying to understand the reduction from 3-SAT problem to a scheduling problem in order to prove the later is also ...
1
vote
1answer
79 views
Counting solutions of a particular type in HORN SAT
I am interested in counting the number of solutions of a particular type (say #) in HORN SAT. I have 2 questions concerning the same.
Suppose we have a HORN SAT -: $(x_1) \land (x_2 \implies x_1)$, ...
