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
4
votes
3answers
292 views

Are there IP competitions?

Are there competitions for integer programming like there are for SAT and MAXSAT?
2
votes
1answer
167 views

Proof for NP-hardness of simultaneous minimization and maximization of a weighted subset

I am working on a problem defined as the following Given a set of $n$ elements called $R \subseteq \mathbb{N} \times \mathbb{N}$ and numbers $Z,G \in \mathbb{N}$, where $Z$ is a measure of our ...
-1
votes
0answers
20 views

2 SAT NL algorithm

How would you define the 2-SAT complement pseudo code? The information I gathered is, Let x be random variable chosen then we have to check if there exist a path between x to ~x and from ~x to x. If ...
-1
votes
1answer
34 views

Does 2SAT contained in SAT?

Is it true that $2 S A T \subseteq S A T ?$ and in general is $k S A T \subseteq S A T $ where k is any positive integer is true? Thanks.
0
votes
0answers
22 views

CNF encoding of additions

I have $m$ equations of the following form: $$x_1+x_2+\cdots+x_n=s,$$ where each variable is either 1 or 0, and the total number of variables is $m\approx3{,}000$. So I’m thinking of modeling each ...
3
votes
1answer
44 views

Complete resolution rule for 1-in-k SAT

In CNF SAT, each clause (A or B or C or...) must contain at least one true literal. The resolution rule applies to pair of clauses who have exactly one opposite literal. (A or B or C) and (!A or D ...
1
vote
3answers
155 views

Counting the number of satisfied models - given mathematical constraints

Question There are plenty of algorithms for solving the #SAT problem, with one being the DPLL algorithm and is implemented for all kinds of programming languages. As far as I've seen, they all take a ...
3
votes
1answer
32 views

Reference asking: phase transition in SAT

This is not a technical question, I hope this community has a room for such questions, but I will delete it in case this is inappropriate. It has been experimentally observed (e.g. here) that when ...
1
vote
1answer
41 views

What are the differences between symbolic execution and SAT solvers?

My understanding is that symbolic execution only deals with specific paths and bad patterns, while SAT solvers, or satisfiability modulo theories in general, provide a much more robust analysis of the ...
1
vote
1answer
37 views

When does Gaussian elimination solve exact 1-in-3 SAT?

Terms: A literal is a variable or its negation. A clause is a set of literals. An exact 3-in-1 clause is satisfied if an assignment of values to variables results in exactly 1 ...
0
votes
0answers
16 views

Translating running times of $3$-coloring to $k$-$SAT$ complexity

Suppose there is an $O(f(n))$ algorithm for $3$-coloring a graph on $n$ vertices what does it translate to in terms of time complexity for solving $k$-$SAT$ with $m$ clauses?
3
votes
1answer
85 views

Having trouble understanding a proof of Mahaney’s theorem

I am reading a blog post of Lance Fortnow, which includes a proof of Mahaney's theorem. I am not sure why $a’$ cannot be in between $w_i$ and $w_j$ in Case 1, and also why $a’$ cannot be in between $...
0
votes
1answer
27 views

Maximum number of positive literals in 2SAT

MAX 2SAT is NP complete. Instead of satisfying the maximum number of clauses, I have a fully satisfiable 2SAT formula and I want to have the maximum number of positive literals in the assignment (...
1
vote
1answer
57 views

P=NP when number of inputs that give 1 is bounded by polynomial

Suppose there exists some NP-complete problem such that the number of inputs that gives 1 as an output is bounded by a polynomial; that is, if the problem is $f \colon \{0, 1 \}^* \to \{0, 1\}$, then, ...
1
vote
2answers
88 views

Converting Mathematical Statements to SAT Formulas

Is it possible to write a mathematical statement (like Goldbach's conjecture, for example) as a nontrivial 3-SAT formula that is satisfiable iff that statement is true? iff it is false? iff it is ...
0
votes
0answers
18 views

the correctness of 2-satisfiability problem algorithm by using implication graph

I learned finding a solution of 2-sat problem algorithm below. The point are below (1) when constructing the implication graph (2) finding there is no occurrence of a variable x and its negation x' ...
1
vote
1answer
46 views

building a polynomial algorithm that solves SAT when given a polynomial TM that solves SAT on two formulas

Here's the question: Assume there exists a polynomial time machine $M$ that receives two formulas $\varphi_1,\varphi_2$ and satisfies the following: If $\varphi_1 \in \mathrm{SAT}$ and $\...
2
votes
0answers
25 views

Names of specific SAT variants

I enjoy reading research on satisfiability, but sometimes it's easier to find relevant information when you know the names of the variants. Example: All the clauses are width 3 and must have ...
1
vote
1answer
65 views

Turing reducibility of 2 versions of the satisfiability problem

I need help with this problem. There are 2 versions of the satisfiability problem: [1] decision version: determine whether an arbitrary formula f is satisfiable or not [2] search ...
1
vote
1answer
62 views

Reducibility of 2 boolean satisfiability problems

I beg some help with this problem. There are 2 boolean satisfiability problems. Problem $A$: Determining whether an arbitrary formula of size $n$ is $satisfiable$. Problem $B$: Determining ...
1
vote
0answers
52 views

CircuitSAT to 1-in-3SAT

This question follows Unique 3SAT to Unique 1-in-3SAT Consider an AND gate such that (A ∧ B) = C. It can be trivially expressed in 3SAT with 4 clauses and no extra variables. $$ (A ∨ B ∨ \overline{...
2
votes
2answers
148 views

Unique 3SAT to Unique 1-in-3SAT

Suppose I have a CNF formula with clauses of size 2 and 3. It has a unique satisfying assignment. It was made from a binary multiplication circuit where I multiplied two primes numbers A and B such ...
1
vote
1answer
26 views

Unique 1-in-3 SAT

Suppose I have a CNF formula with clauses of size 2 and 3. It has a unique satisfying assignment. I know the value of each bit of the unique assignment because it was made from a binary ...
0
votes
1answer
80 views

Prove or Disprove, 3SAT ≤p 2SAT, then P = NP

I know that 3SAT is in NP and 2SAT is in P. And 2SAT can reduce to 3SAT just says 3SAT is strictly harder than 2SAT, so I don't think this proves P = NP, but it doesn't seem to disprove it either.
10
votes
2answers
3k views

What is wrong with this simple proof of P=NP?

Exactly 1 in 3 SAT ($X3SAT$) is a variation of the Boolean Satisfiabilty problem. Given an instance of clauses where each clause has three literals, is there a set of literals such that each clause ...
2
votes
1answer
36 views

Programming in Propositional Logic article notation question

I was reading this article about propositional logic and transforming problems to SAT. The author often uses the following notation (taken from Dominating set section): I don't understand what $[v,i]$...
2
votes
1answer
65 views

MAX 2-SAT is polynomial time reducible to 2-SAT?

I know that 2-SAT is solvable in polynomial time and 2-SAT is NP-Hard. I have issue about this statement: MAX 2-SAT is polynomial-time reducible to 2-SAT. Can you explain to me how reduction looks ...
1
vote
1answer
66 views

Time complexities of state-of-the-art SAT solvers with respect to length of the formula

I am learning about DPLL and CDCL SAT solvers, and I know that they have time complexity exponential to the number of variables. If I am not mistaken, one of the reasons why most believe P does not ...
1
vote
1answer
72 views

Use 2SAT to show that an implication graphs must have a cycle if it's not satisfiable

Using 2SAT and implication graphs, how could I prove the following properties of implication graphs: Suppose there is a directed path between literals l1 and l2 in G_φ. Then there is also a directed ...
2
votes
1answer
31 views

Definition of 2-CNF (a.k.a Krom) formula

In my lecturer's notes, the following definition for a 2-CNF wff is given: A 2-CNF formula, or Krom formula is a CNF formula F such that every clause has at most two literals. However, there is ...
3
votes
1answer
59 views

Clarification on “clause learning” in DPLL algorithm

I am struggling to understand the idea of conflict-driven clause learning, in particular, I can not understand why the clause we 'learned' is a substantially new (i.e. the clause database does not ...
2
votes
0answers
21 views

Flip Output of SAT problem [duplicate]

Why cant I Just create a TM A that runs a NTM B with a formula to compute the SAT Problem and Just Flip its Output. So when the Input NTM B Returns true (formula is satisfyable) the TM A Return false.
2
votes
1answer
60 views

Special Monotone SAT problem: NP complete?

Say we have the set $X=\{ x_1, x_2, \dots \}$ of variables. Then we consider the following problem: Is the formula $$\bigwedge_{(a,b,c) \in A}(a \vee b \vee c) \wedge \bigwedge_{(a,b,c) \in B}(\neg a ...
3
votes
1answer
135 views

Polynomial-time linear-reduction from Directed Hamiltonian Path Problem to 3SAT

Is there a polynomial-time reduction from Directed Hamiltonian Path Problem to 3SAT which is linear in the number of vertices? That is, it reduces every directed graph $G$ with $n$ vertices to a ...
4
votes
2answers
255 views

An Exact Method for Solving Small Instances of XORSAT

I have a couple of small instances for XORSAT for which I am to design and implement an exact method. However, there are a few catches. It is guaranteed that there always exists and answer but I need ...
1
vote
0answers
83 views

Class of languages recognizable by n-bit formulas of size at most $T(n)$

A Boolean (combinatoiral) circuit is a labeled (with the labels: AND, OR, NOT, IN, OUT), directed, acyclic graph, that satisfies: fan-in=2 for the AND and OR nodes fan-n=1 for the NOT nodes fan-...
0
votes
0answers
64 views

Give me ideas for an undergraduate final year math project about Boolean Satisfiability and SAT solvers

Context I am a student starting an undergrad math project. I was instructed to read Donald Knuth's Fascicle 6: Satisfiability and come up with ideas for a project from this material. I have 13 weeks ...
1
vote
0answers
34 views

Are there any resources or forums online for helping me understand TAOCP?

Context I am doing an undergrad math project that involves exploring Donald Knuth's "TAOCP, Volume 4, fascicle 6: Satisfiability". I am having trouble parsing some of this material. Surely ...
2
votes
0answers
40 views

Boolean matrix / satisfiability problem [duplicate]

Let $M$ be an $m\times n$ matrix with all elements in $\{1,0\}$, $m >> n$. Let $\mathbf{v}_0, \ldots, \mathbf{v}_n$ be the columns of $M$. I want to find all sets of columns $S = \{\mathbf{v}_{...
2
votes
1answer
62 views

Encoding set of At-Most-One constraints as a MAX-SAT problem

Assume a set of variable $V$ = $\{v_1,...,v_m\}$. Given total $n$ at-most-one (AMO) constraints (at most one element in a given set is true) set [of the below form], over the variable set $V$, $$ ...
1
vote
1answer
85 views

Integer programming to MAX-SAT translation

Reading A Comparison of Methods for Solving MAX-SAT Problems, I can see that a MAX-SAT problem can be translated to an integer programming (IP) problem. Definition of MAX-SAT [Wikipedia]: The ...
4
votes
2answers
138 views

Is it feasible to solve this subset cover problem with SAT solver?

The problem is to find $\mathcal{S}$, a minimal collect of subsets of $\{1,\dots, 17\}$ such that the two conditions are satisfied: if $S \subseteq \mathcal{S}$ then $|S|=6$; for any $A \subseteq \{1,...
0
votes
0answers
35 views

CNF2 = { φ | φ is a satisfiable CNF-formula in which each variable appears at most 2 times}. Show CNF2 is in P

CNF2 = { φ | φ is a satisfiable CNF-formula in which each variable appears at most 2 times}. Show CNF2 is in P. I found this solution: We use the method of resolution to take the variables out ...
0
votes
0answers
214 views

CNFH = {⟨φ⟩| φ is a satisfiable cnf-formula where each clause contains any number of literals, but at most one negated literal} ∈ P

The problem derived from the book of Sipser and the question was already posted (link) with partial comments. Let CNFH = {⟨φ⟩| φ is a satisfiable cnf-formula where each clause contains any number ...
0
votes
0answers
67 views

Using induction prove that a K-SAT problem is NP-Complete

Using induction on k, how do I prove that the K-SAT problem is NP-complete? On wikipedia, it describes the Cook-Levin theorem to prove that K-SAT is NPC by reducting the K-SAT problem to a circuit-...
3
votes
1answer
36 views

CNF satisfiability with a bound on number of clauses

Consider the CNF-sat problem with n literals and k clauses. If k scales linearly in n, we get np-completeness (e.g., 3-sat where each literal appears at most 4 times). Do we still get np-completeness ...
4
votes
2answers
126 views

Are SAT problems with at most two false clauses NP-complete?

Is the problem of deciding whether a SAT instance, where at most two clauses are false (that is, any given variable assignment will either lead to all clauses being true, all but one, or all but two), ...
2
votes
1answer
28 views

Significance of quantifier ordering in quantified boolean formulas (kQBF vs. QBF)

I am studying solvers of quantified boolean formulas (QBF) as a generalization of SAT solving. The standard DIMACS format of SAT specification is extended to QDIMACS, which adds "a ..." and "e ..." ...
5
votes
2answers
255 views

checking '<' for two binary numbers in a cnf-formula

I want to check whether a arbitrary binary number is less or equal to another binary number in a cnf-formula. I can already construct a formula, which is not in cnf: Lets say n and m are two-digit ...
1
vote
1answer
46 views

Find a truth assignment of 2SAT that has the most number of true variables?

Given a 2SAT instance in CNF where each clause has at most two literals. Let $m$ be the number of clauses and $n$ be the number of variables et let $k$ be a positive number. Question: Is there a ...

1
2 3 4 5
10