# Questions tagged [conjunctive-normal-form]

A formula is in conjunctive normal form (CNF) if it is a conjunction of clauses, where a clause is a disjunction of literals.

189 questions
Filter by
Sorted by
Tagged with
13 views

33 views

### At most $k$ contiguous $\mbox{true}$ values in a Boolean array using SAT

Given an integer $k > 0$ and a Boolean array $A$ of length $n$, find a simplified and efficient CNF formula to ensure that there is not more than $k$ contiguous $\mbox{true}$ values in this array. ...
15 views

### Number of distinct unsatisfiable 3CNF formula consisting of n variables

I'm interested to know if anyone knows the number of unsatisfiable 3SAT formulae in CNF consisting of $n>3$ variables. Specially, formulae where no clause contains the same literal twice, either ...
24 views

### Converting First-Order Logic to CNF

I am having a lot of trouble using the rules of converting First-Order Logic to CNF. I have this statement: ∀x∃y : ([P(x, y) → Q(y, x)] ∧ [Q(y, x) → S(x, y)]) → ∃x∀y : [P(x, y) → S(x, y)] After ...
1 vote
66 views

### Is there a method to solve 3SAT problems using loss function?

Loss function seems to be used to solve optimization problems. I assumed that 3SAT problems can be treated as them. I would like to know whether there is a good loss function that is defined by ...
1 vote
63 views

### I'm studying boolean algebra in the discrete mathematics

problem Let $a_4a_3a_2a_1a_0$ be a 5- bits binary numbers (each $a_i=0$ or $1$). Write an expression in Boolean algebra that evaluates to $1$ when odd number of bits of the number is $1$ and $0$ ...
51 views

### Why doesn't Krom's method apply to solving the 3SAT in polynomial time?

In the paper "The Decision Problem for a Class of First-Order Formulas in Which all Disjunctions are Binary", Krom suggested a method to solve 2SAT problem. My understanding is this. Use ...
32 views

33 views

### How do I re-write this propositional formula in conjunctive normal form (CNF)?

I'm struggling with this problem -- though it would seem simple enough. I think it's the parentheses that are getting me confused here. I need to convert (p→(q⋁r))⋁(s↔t) to conjunctive normal form (...
1 vote
33 views

Can the following clause be converted to conjunctive normal form? If so how? $$(a \implies b) \implies (c \implies d)$$ I tried applying DeMorgans laws and am unable to get the result. $$(a \... 1 vote 0 answers 91 views ### Help with Resolution Refutation Problem I'm trying to convert Solve a Resolution Refutation problem. The problem states: Knowledge Base is ∀𝑥𝑦 𝐹(𝑥, 𝑦). Prove using resolution-refutation that ∀𝑥𝑦 𝐹(𝑦, 𝑥). Note: β = F(y, x) This ... 0 votes 1 answer 17 views ### expanding disjunctive pairs of conjunctives using distributive law I am having a bit of a brain malfunction. I am working through a functional programming class and I am trying to in parallel fake some knowledge of discrete mathematics. I am working through a simple ... 0 votes 1 answer 44 views ### Can clause normal form include true/false constants? As Wikipedia puts it, ... the only propositional connectives a formula in CNF can contain are and, or, and not. The not operator can only be used as part of a literal, which means that it can only ... 0 votes 1 answer 78 views ### How to get CNF of propositional formula form DNF of its complement? Explain how to read off a CNF for propositional formula directly from a DNF from its complement. I've managed to explain it in words, but can't write a rigorous proof of that. How to show this in ... 0 votes 0 answers 69 views ### Generalisation of DNF to CNF for DNF of m choose l clauses Given two values m and l, I can create corresponding DNF formula which is a disjunction of all m \choose l combinations, where each number corresponds to a variable. Each combination is, in ... 1 vote 1 answer 82 views ### The Explanation on how to form CNF I am currently reading Logic in Computer Science Modelling and Reasoning About Systems (by Michael Huth & Mark Ryan). They introduced a fairly easy way to form conjunctive normal form (CNF) of an ... 0 votes 1 answer 42 views ### HORN algorithm - clarity needed I have been spending some time studying the HORN algorithm, but my textbook, as well as most posts online, are quite vague around the steps taken. These are the steps from my textbook: My questions: ... 0 votes 1 answer 99 views ### How to introduce conjunctions into a conditional statements so as to get the CNF and DNF? I have the following conditional statement: ((p → q) → p) → p Knowing that CNF is a conjunction of disjunctions (and that DNF is a disjunction of conjunctions), we will obviously have to introduce ... 0 votes 1 answer 42 views ### Converting propositional logic formula to CNF I have been trying to do this all day but I am not getting anywhere with it, could anyone help me? My formula is r → (p ↔ ¬q) And I want to convert it into CNF ... 0 votes 0 answers 70 views ### Dominant set of a Graph - Convert to Conjunctive Normal Form I am supposed to convert this problem to a Satisfiability Problem in Conjunctive Normal Form, but I have no idea how. The Problem: Determine, if there exists any dominant set for a Graph G ... 0 votes 1 answer 242 views ### Explain into disjunctive normal form Can anyone tell me how to Express the following formula into disjunctive normal form ⌐ (p V q) ↔ (p ^ q). I have done few steps but I need your help. 0 votes 1 answer 43 views ### Converting 3-variable truth table to 3CNF I have a truth table for length 3 binary strings, say 110 and 001 map to 1 and everything else to 0. Is there an an algorithm to represent this table as a 3CNF which is satisfied only by ... 0 votes 1 answer 29 views ### How to prove that a given disjunctive or conjuctive normal form is minimal? what is the argument that a given canonical normalform cannot be reduced any further? For example have a look at this dnf(f) = (\neg a \wedge b \wedge c) \vee (a \wedge \neg b \wedge c) \vee(a \... 0 votes 1 answer 46 views ### DNF to CNF of a simple expression I have a formula like this:$$\bigvee_{\substack{i \in [1,...,m] \\ j \in [1,...,m]}} x_{i} \wedge x_{j}$$What is the equivalent formula in CNF (conjunctive normal form)? 0 votes 1 answer 89 views ### Is the following boolean expression a tautology? I have the following boolean Expression: ... 0 votes 1 answer 65 views ### CNF formula for manipulating words I am trying to create CNF formula for manipulation of a word. word is a sequence of letters from a \Sigma alphabet. A word is encoded by variables like x_{i,a} which means that the letter a is ... 0 votes 1 answer 35 views ### CNF for modilisation of a word Imagine that we are interested in problem of words. A word is a sequence of letters from a \Sigma alphabet. For encoding a word in SAT we are using variable like x_{i,a} which means that in ... 1 vote 1 answer 93 views ### Converting a 4cnf clause into one with not all equal literals Given a 3cnf clause$$(a \lor b \lor c)$$we can construct an equivalent conjunction$$(a\lor b\lor d) \land (\lnot d \lor c \lor \bot)$$such that the second clause has a valid truth assignment if ... 1 vote 1 answer 93 views ### Is it possible to get from a propositional formula a CNF with clause (¬A ∨ ¬B ∨ ¬C), if formula doesn't have negations in it? If i have a propositional formula consisting of conjunctions, disjunctions and implications and no negations of three literals A, B, C, is it possible to get a CNF from that formula which include ... 1 vote 1 answer 259 views ### Apply resolution algorithm to check SAT for CNF I have a CNF:$$(\neg p \lor \neg q \lor r) \land (\neg p \lor \neg r) \land p \land q$$I need to check SAT for it using resolution algorithm, but i don't know how. I know how to check it with truth ... 0 votes 2 answers 48 views ### Can I rewrite propositional formula in this way? I have a propositional formula:$$(\neg p \lor \neg q \lor r)$$Can i rewrite it in this way?:$$(\neg p \lor \neg q \lor r) = (\neg p \lor (q \land \neg r))= (\neg p \lor q) \land (\neg p \lor \neg r)... 91 views

### Find conjunctive normal form of propositional formula

I need to find conjunctive normal form (CNF) of this propositional formula: $$\lnot((p \implies (q \implies r)) \implies ((p \implies \lnot r) \implies (p \implies \lnot q)))$$ How could i do that? I ...
502 views

### Ways to write CNF for an implication with disjunction?

I have the following statement before it's converted to CNF: p → (s ∨ q). When I initially convert this to a CNF, I get the following: ¬p ∨ (s ∨ q). I'm wondering if I could use laws of associativity ...
52 views

### How to convert $(A \vee B) \wedge (C \vee D)$ to CNF?

Wikipedia states that all propositional logic statements can be transformed into CNF. However, I'm not so sure how we can further simplify $(A \vee B) \wedge (C \vee D)$? Or if this is CNF, why is it ...
1 vote
Why do we introduce a negative when trying to simplify? (circled in orange) If x approaches -$\infty$ for both, the negative sign should cancel out..? Khan acad's working: Edit, removed my workings ...