A linear-time transformation of linear inequalities into conjunctive normal form

DOI10.1016/S0020-0190(98)00144-6zbMath1339.68244MaRDI QIDQ293409

Joost P. Warners

Publication date: 9 June 2016

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: http://www.sciencedirect.com/science/article/pii/S0020019098001446?np=y

zbMATH Keywords

combinatorial optimizationsatisfiabilityautomatic theorem proving

Mathematics Subject Classification ID

Linear programming (90C05) Combinatorial optimization (90C27)

Related Items

Algorithms for Solving Satisfiability Problems with Qualitative Preferences, What we can learn from conflicts in propositional satisfiability, Propositional SAT Solving, Improving the Normalization of Weight Rules in Answer Set Programs, Some computational aspects of DISTANCE SAT, Solving satisfiability problems with preferences, HySAT: An efficient proof engine for bounded model checking of hybrid systems, Boolean lexicographic optimization: algorithms \& applications, A Boolean satisfiability approach to the resource-constrained project scheduling problem, Learning from conflicts in propositional satisfiability, Probabilistic satisfiability: algorithms with the presence and absence of a phase transition, Towards Robust CNF Encodings of Cardinality Constraints, On preprocessing for weighted MaxSAT, Quantitative Logic Reasoning, Cardinality networks: a theoretical and empirical study, \(N\)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT, Encoding cardinality constraints using multiway merge selection networks, New Encodings of Pseudo-Boolean Constraints into CNF, Algorithms for Weighted Boolean Optimization, Bounds and fast approximation algorithms for binary quadratic optimzation problems with application to MAX 2SAT, On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving, Open-WBO-Inc: Approximation Strategies for Incomplete Weighted MaxSAT, Iterative and core-guided maxsat solving: a survey and assessment

Cites Work

• Unnamed Item
• Compact normal forms in propositional logic and integer programming formulations
• Some results and experiments in programming techniques for propositional logic
• Branch-and-cut solution of inference problems in propositional logic
• A potential reduction approach to the frequency assignment problem
• Local search algorithms for the radio link frequency assignment problem
• A nonlinear approach to a class of combinatorial optimization problems
• Convex Programming Methods for Global Optimization