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
54 views
Counting models satisfying a boolean formula
I'm trying to implement the #2-SAT algorithm from the paper "Counting Satisfying Assignments in 2-SAT and 3-SAT" (Dahllöf, Jonsson and Wahlström, Theor. Comput. Sci. 332(1–3):265–...
-2
votes
0answers
26 views
Please help me with exercise 6.3.3 of László Lovász Computational Complexity lecture notes
Let us call a Boolean formula with n variables simple if it is
either unsatisiable or has at least 2^n / n^2 satisfying assignments. Give a probabilistic polynomial algorithm to decide the ...
1
vote
1answer
28 views
Can problems of class P be transformed into SAT formula?
I know that NP problems can be transformed into SAT (due to this fact, SAT is considered to be a NP Complete problem). I am not sure if P problems can too be transformed into SAT.
0
votes
1answer
19 views
Fine-grained complexity of 3-CNF formula evaluation
It's well known that 3-SAT is in NP, which means that one can evaluate a 3-CNF formula in polynomial time. However, I was wondering what the tightest upper bound is for formula verification, expressed ...
2
votes
2answers
29 views
Calculating the number of assignments satisfying a general propositional formula
I know, for a disjunctive clause of the form $x_1 \vee ... \vee x_i$, the number of assignments satisfying it is simply $2^i - 1$, but what about for a general formula? Is the number of satisfying ...
1
vote
1answer
14 views
For a given k-DNF formula, what is the size of the formula for the purpose of complexity?
I am currently in the process of proving some complexity bounds about k-DNF. However I am confused what the $n$ in the time complexity would refer to in this case (that is that I don't know how the "...
0
votes
0answers
21 views
Can I use the Quine-McCluskey to simplify a CNF which is not a product of maxterms?
As I understand it the Quine-McCluskey method allows you to start with a set of maxterms (or minterms), and combine them pairwise in a systematic way into a smaller set of clauses with a smaller set ...
2
votes
1answer
38 views
Refutation in first order logic
Consider the following statement
In FOL, we can reduce entailment checking to satisfiability checking:
$S \models S' \iff S \land \neg S'$ is satisfiable (This proof
strategy is called ...
1
vote
1answer
31 views
Why Cook-Levin thorem's proof can mean SAT's NP-Hardness
I'm studying about Cook-Levin theorem but there is a problem I faced. Cook-Levin theorem shows that any NPTM can be encoded as a boolean formula. About given language $A$, instance $w$, and NPTM $M$ ...
3
votes
0answers
15 views
relationship between SAT and Min-ones SAT
If SAT can be decided in polynomial time, is it clear that Min-ones SAT can be decided in polynomial time? The idea I had was to take a poly decider of SAT and try it on a formula OR'd with all ...
0
votes
1answer
40 views
Seeking nontrivial small SAT/UNSAT instances
I need SAT instances, involving 9 to 20 variables. They need to be hard to solve for humans. Both SAT and UNSAT instances are needed.
I tried random-SAT generators on the web, but the results were ...
1
vote
0answers
186 views
Could you show the intractibility of SAT by showing that the number of variables contributing to an arbitrary unsatisfied clause is not constant? [closed]
Preface: This is not an attempted proof at P vs NP
Starting with some CNF Boolean expression ϕ, by the rules of logical disjunction, a clause is only unsatisfied if each of the literals in it are ...
1
vote
1answer
20 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
27 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
32 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
23 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
42 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
30 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
120 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
21 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
88 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
27 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
16 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
14 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
109 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
125 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
70 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
15 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
52 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
44 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
37 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
96 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
233 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
155 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
33 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
102 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
272 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
33 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
81 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
72 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
64 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
144 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
54 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
93 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
29 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
315 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
30 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
39 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 ...
