Skip to content

Commit

Permalink
feat: add sharpSAT frontend
Browse files Browse the repository at this point in the history
  • Loading branch information
piotr.malkowski committed Feb 17, 2025
1 parent 30a7f12 commit f333e87
Showing 1 changed file with 50 additions and 0 deletions.
50 changes: 50 additions & 0 deletions src/pages/solve/SharpSAT.tsx
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
import { Divider, Heading, Spacer, Text } from "@chakra-ui/react";
import type { NextPage } from "next";
import { useState } from "react";
import { Layout } from "../../components/layout/Layout";
import { SAT_language } from "../../components/solvers/SAT/prism-SAT";
import { SolverConfiguration } from "../../components/solvers/SolverConfiguration";
import { TextInputMask } from "../../components/solvers/TextInputMask";
import { LogicalExpressionValidator } from "../../converter/dimacs/LogicalExpressionValidator";

const SharpSAT: NextPage = () => {
const logicalExpressionValidator = new LogicalExpressionValidator();

const [logicalExpressionString, setLogicalExpressionString] = useState("");

return (
<Layout>
<Heading as="h1">sharpSAT Solver</Heading>
<Text color="text" align="justify">
For a given Boolean formula, this algorithm counts the number of satisfying assignments.
You can enter any Boolean formula with any number of variables and combine them using Boolean operators
(i.e., &quot;and&quot;, &quot;or&quot; and &quot;not&quot;).
</Text>

<Spacer />

<TextInputMask
textPlaceholder='Try "a and (not a or not b)"'
text={logicalExpressionString}
setText={setLogicalExpressionString}
problemTypeId="sharpsat"
grammar={{
grammar: SAT_language,
language: "SAT_language",
}}
validate={(text) =>
logicalExpressionValidator.validateLogicalExpression(text)
}
/>

<Divider />

<SolverConfiguration
problemTypeId="sharpsat"
problemInput={logicalExpressionString}
/>
</Layout>
);
};

export default SharpSAT;

0 comments on commit f333e87

Please sign in to comment.