A novel approach of solving the CNF-SAT problem
In this paper, we discussed CNF-SAT problem (NP-Complete problem) and analysis two solutions that can solve the problem, the PL-Resolution algorithm and the WalkSAT algorithm. PL-Resolution is a sound and complete algorithm that can be used to determine satisfiability and unsatisfiability with certainty. WalkSAT can determine satisfiability if it finds a model, but it cannot guarantee to find a model even there exists one. However, WalkSAT is much faster than PL-Resolution, which makes WalkSAT more practical; and we have analysis the performance between these two algorithms, and the performance of WalkSAT is acceptable if the problem is not so hard.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving
As a seemingly self-explanatory task, problem-solving has been a significant component of science and engineering. However, a general yet concrete formulation of problem-solving itself is missing. With the recent develop…
Automated Theorem ProvingArguments for the Effectiveness of Human Problem Solving
The question of how humans solve problem has been addressed extensively. However, the direct study of the effectiveness of this process seems to be overlooked. In this paper, we address the issue of the effectiveness of …
Problem-solving Recognition in Scientific Text
As far back as Aristotle, problems and solutions have been recognised as a core pattern of thought, and in particular of the scientific method. In this work, we present the novel task of problem-solving recognition in sc…
Solving the QAP by Two-Stage Graph Pointer Networks and Reinforcement Learning
Quadratic Assignment Problem (QAP) is a practical combinatorial optimization problems that has been studied for several years. Since it is NP-hard, solving large problem instances of QAP is challenging. Although heuristi…
Combinatorial OptimizationDeep LearningDeep Reinforcement LearningTraveling Salesman ProblemAn Augmented Benchmark Dataset for Geometric Question Answering through Dual Parallel Text Encoding
Automatic math problem solving has attracted much attention of NLP researchers recently. However, most of the works focus on the solving of Math Word Problems (MWPs). In this paper, we study on the Geometric Problem Solv…
Data AugmentationMathQuestion Answering