Applying GSAT to Non-Clausal Formulas
R. Sebastiani
TL;DR
This paper presents a modification of the GSAT algorithm enabling it to efficiently handle non-clausal formulas by using a linear-time scoring function based on CNF clause falsification.
Contribution
It introduces a novel scoring method that allows GSAT to be applied directly to non-clausal formulas without explicit CNF conversion.
Findings
The modified GSAT can be applied to non-clausal formulas efficiently.
The scoring function is computed in linear time.
The approach is compatible with most GSAT variants.
Abstract
In this paper we describe how to modify GSAT so that it can be applied to non-clausal formulas. The idea is to use a particular ``score'' function which gives the number of clauses of the CNF conversion of a formula which are false under a given truth assignment. Its value is computed in linear time, without constructing the CNF conversion itself. The proposed methodology applies to most of the variants of GSAT proposed so far.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMulti-Criteria Decision Making · Bayesian Modeling and Causal Inference